可编程策略到项重写系统的忠实（元）编码
编程语言
2019-03-14 v2
摘要
重写是计算机科学和数理逻辑中广泛使用的形式体系。当将重写用作编程或建模范式时，重写规则描述了人们想要执行的转换，而重写策略用于控制其应用。这些策略的操作语义已被普遍接受，且分析特定策略终止性的方法也已被研究。本文提出了一种通用编码，将 Maude、Stratego 和 Tom 等基于重写的语言中使用的经典控制和遍历策略编码为普通项重写系统。该编码被证明是可靠且完备的，作为直接推论，用于项重写系统的成熟终止方法可应用于分析策略控制的项重写系统的终止性。我们表明，将策略编码为项重写系统可轻松适配以处理多类签名，并使用项的元级表示来减小编码规模。在 Tom 中的相应实现生成了与 AProVE 和 TTT2 等终止工具语法兼容的项重写系统，这些工具在（反）证明生成的项重写系统的终止性方面非常有效。该方法也可被视为通用策略编译器，可集成到提供模式匹配原语的语言中；Tom 中的实验表明，应用我们的编码可获得与原生 Tom 策略相当的性能。
引用
@article{arxiv.1705.08632,
title = {Faithful (meta-)encodings of programmable strategies into term rewriting systems},
author = {Horatiu Cirstea and Serguei Lenglet and Pierre-Etienne Moreau},
journal= {arXiv preprint arXiv:1705.08632},
year = {2019}
}