Four equivalent equivalences of reductions

V. van Oostrom, R.C. de Vrijer

Research output: Contribution to JournalArticleAcademicpeer-review


Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a different order. We present four characterisations of such a notion of equivalence, based on permutation, standardisation, labelling and projection, respectively. We prove that the characterisations all yield the same notion of equivalence, for the class of first-order left-linear term rewriting systems. A crucial rôle in our development is played by the notion of a proof term. ©2002 Published by Elsevier Science B. V.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2002

Bibliographical note

Proceedings title: Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002)
Publisher: Elsevier


Dive into the research topics of 'Four equivalent equivalences of reductions'. Together they form a unique fingerprint.

Cite this