×

Axiomatizing permutation equivalence. (English) Zbl 0884.68070

Two important notions have been introduced in order to equip rewriting systems with a semantics through equivalences between derivations. The first one, permutation equivalence, generalizes the well-known Church-Rosser theorem and proceeds by a thorough manipulation of residuals. The second one, due to Meseguer, exploits the algebraic structure of terms, extended to derivations, on which categorical axioms are provided.
The paper proves the equivalence of the two approaches in the case of term rewriting systems (t.r.s.). In order to show the failure of this result in general, the case of \(\lambda\)-calculus with explicit substitutions is studied, where the non-equivalence comes from critical pairs that Meseguer’s axioms cannot handle. Then the authors succeed in proving the equivalence in Klop’s orthogonal combinatory reduction systems (o.C.R.S.). Using a technique of ‘flattening’ of an o.C.R.S. to a term rewriting system.

MSC:

68Q42 Grammars and rewriting systems
03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Boudol, Fundamenta Informaticae 11 pp 433– (1988)
[2] Boudol, Algebraic Methods in Semantics pp 169– (1985)
[3] Aczel, A general Church-Rosser theorem (1978)
[4] DOI: 10.1016/0304-3975(93)90240-T · Zbl 0783.68089
[5] DOI: 10.1016/0890-5401(90)90013-8 · Zbl 0711.68077
[6] Meseguer, Algebraic Methods in Semantics (1985)
[7] DOI: 10.1016/0304-3975(92)90087-V · Zbl 0756.68075
[8] DOI: 10.1016/0304-3975(90)90118-2 · Zbl 0716.03022
[9] Lévy, To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism pp 159– (1980)
[10] Laneve, Fundamenta Informaticae 20 pp 333– (1994)
[11] DOI: 10.1016/0304-3975(93)90091-7 · Zbl 0796.03024
[12] Laneve, Springer-Verlag Lecture Notes in Computer Science 632 pp 350– (1992)
[13] Curry, Combinatory Logic (1974)
[14] DOI: 10.1016/0304-3975(92)90182-F · Zbl 0758.68043
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.