TY - GEN
T1 - Reductions in Higher-Order Rewriting and Their Equivalence
AU - Barenbaum, Pablo
AU - Bonelli, Eduardo
N1 - Publisher Copyright:
© Pablo Barenbaum and Eduardo Bonelli.
PY - 2023/2/1
Y1 - 2023/2/1
N2 - 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 (β-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.
AB - 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 (β-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.
KW - Equivalence of Computations
KW - Higher-Order Rewriting
KW - Proof terms
KW - Term Rewriting
UR - http://www.scopus.com/inward/record.url?scp=85148322755&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85148322755&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2023.8
DO - 10.4230/LIPIcs.CSL.2023.8
M3 - Conference contribution
AN - SCOPUS:85148322755
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 31st EACSL Annual Conference on Computer Science Logic, CSL 2023
A2 - Klin, Bartek
A2 - Pimentel, Elaine
T2 - 31st EACSL Annual Conference on Computer Science Logic, CSL 2023
Y2 - 13 February 2023 through 16 February 2023
ER -