Four equivalent equivalences of reductions

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^ole in our development is played by the notion of a proof term.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Vincent van Oostrom, Roel C. de Vrijer
• Keywords: Co-initial Reductions, ENTCS 2002, First-order Left-linear Term, Term Rewriting Systems