Reductions in Higher-Order Rewriting and Their Equivalence

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 {\em equivalence of reductions} in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to {\em 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 ($\beta$-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 \emph{rewrites} that supports nested composition. We then define {\em two} notions of equivalence on rewrites, namely {\em permutation equivalence} and {\em projection equivalence}, and show that they coincide.