Transfinite reductions in orthogonal term rewriting systems (extended abstract)
Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, F. J. de Veries · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1990
We establish some fundamental facts for infinitary orthogonal term rewriting systems (OTRSs): for strongly convergent reductions we prove the Transfinite Parallel Moves Lemma and the Compressing Lemma.Strongness is necessary as shown by counterexamples.Normal forms (which we allow to be infinite) are unique, in contrast to co-normal forms.Fair reductions result in co-normal forms if they are converging, and in normal forms in case of strong convergence.Rather surprisingly the infinite Church-Rosser Property fails for both converging reductions and strongly converging reductions in OTRSs.Extending the notions head normal form and B0hm tree from Lambda Calculus we prove the infinite Church-Rosser Property for non-unifiable OTRSs.The top-terminating OTRSs of Dershowitz c.s. are examples of non-unifiable OTRSs.