Four equivalent equivalences of reductions |
| |
Authors: | Vincent van Oostrom Roel de Vrijer |
| |
Affiliation: | aDepartment of Philosophy, Universiteit Utrecht, Utrecht, The Netherlands bDepartment of Theoretical Computer Science, Vrije Universiteit, Amsterdam, The Netherlands |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|