Reductions in Higher-Order Rewriting and Their Equivalence

Pablo Barenbaum, Eduardo Bonelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publication31st EACSL Annual Conference on Computer Science Logic, CSL 2023
EditorsBartek Klin, Elaine Pimentel
ISBN (Electronic)9783959772648
DOIs
StatePublished - 1 Feb 2023
Event31st EACSL Annual Conference on Computer Science Logic, CSL 2023 - Warsaw, Poland
Duration: 13 Feb 202316 Feb 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume252
ISSN (Print)1868-8969

Conference

Conference31st EACSL Annual Conference on Computer Science Logic, CSL 2023
Country/TerritoryPoland
CityWarsaw
Period13/02/2316/02/23

Keywords

  • Equivalence of Computations
  • Higher-Order Rewriting
  • Proof terms
  • Term Rewriting

Fingerprint

Dive into the research topics of 'Reductions in Higher-Order Rewriting and Their Equivalence'. Together they form a unique fingerprint.

Cite this