论文标题
降低高阶重写及其等效性
Reductions in Higher-Order Rewriting and Their Equivalence
论文作者
论文摘要
证明术语是句法表达式，代表术语重写中的计算。他们是由Meseguer引入的，并由Van Oostrom和De Vrijer剥削，以研究（左）一阶术语重写系统的减少等效性。我们研究了将证明术语概念扩展到高阶重写的问题，该概念通过允许使用Binders和高阶替换来概括一阶设置。在以前设计的高阶重写证明术语（例如Bruggink的）的作品中，已经指出，挑战在于核对证明术语和高阶替代的组成（\ b {eta} - 等效性）。这导致Bruggink拒绝“嵌套”组成，而不是最外面的层面。在本文中，我们提出了一个高阶证明项的概念，我们将支持嵌套成分的重写。然后，我们在重写上定义了两个等效的概念，即置换等效性和投影等效性，并表明它们是重合的。我们还提出了一个标准化程序，该程序计算重写的置换等效类别的规范代表。
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink's, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (\b{eta}-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide. We also propose a standardization procedure, that computes a canonical representative of the permutation equivalence class of a rewrite.
