| Transfinite Reductions in Orthogonal Term Rewriting Systems (1995) | |||||||||||||||||
Abstract | |||||||||||||||||
| We define the notion of transfinite term rewriting: rewriting in which terms may be infinitely large and rewrite sequences may be of any ordinal length. For orthogonal rewrite systems, some fundamental properties known in the finite case are extended to the transfinite case. Among these are the Parallel Moves lemma and the Unique Normal Form property. The transfinite Church-Rosser property (CR 1 ) fails in general, even for orthogonal systems, including such well-known systems as Combinatory Logic. Syntactic characterisations are given of some classes of orthogonal TRSs which do satisfy CR 1 . We also prove a weakening of CR 1 for all orthogonal systems, in which the property is only required to hold up to a certain equivalence relation on terms. Finally, we extend the theory of needed reduction from the finite to the transfinite case. The reduction strategy of needed reduction is normalising in the finite case, but not in the transfinite case. To obtain a normalising strategy, i... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||