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.

翻译：证明项是表示项重写中计算的语法表达式，由Meseguer引入，并由van Oostrom和de Vrijer用于研究（左线性）一阶项重写系统中归约的等价性。我们研究了将证明项概念扩展到高阶重写的问题，该问题通过允许带有绑定子和高阶替换的项来推广一阶框架。在先前为高阶重写设计证明项的工作（如Bruggink的研究）中，已经注意到挑战在于协调证明项的复合与高阶替换（β-等价）之间的关系。这导致Bruggink拒绝了除最外层以外的"嵌套"复合。在本文中，我们提出了一种称为rewrites的高阶证明项概念，支持嵌套复合。随后，我们定义了rewrites上的两种等价概念，即置换等价和投影等价，并证明它们是一致的。我们还提出了一种标准化过程，能够计算rewrite的置换等价类的典范代表。