Transfinite reductions in orthogonal term rewriting systems
Richard Kennaway, Jan Willem Klop, M. Ronan Sleep · 1990
Abstract: "First we establish some fundamental facts in the theory of infinitary orthogonal term rewriting systems (OTRSs): for strongly convergent reductions we prove the Infinitary Parallel Moves Lemma and the Compression Lemma. Strongness is necessary as shown by counterexamples. Normal forms (finite or infinite) are unique, in contrast to [omega]-normal forms. Strongly converging, fair reductions result in normal forms. Secondly we address the infinite Church-Rosser property, which in general OTRSs fails both for strongly converging reductions and for converging reductions