tree-manipulating systems and church-rosser theorems
We define a general class of tree-manipulating systems that includes many of the special cases from logic, linguistics, and automata theory. Systems possessing what we call the Church-Rosser property are appropriate for evaluation or translation processes: the end result of a complete sequence of applications of the rules does not depend on the order in which the rules were applied. We sketch the theoretical and practical advantages of such flexibility. We derive general sufficient conditions for the Church-Rosser property and apply them to some important tree-manipulating systems. Applications include tree transducers, the McCarthy formalism for recursive computation, and the classical Church-Rosser Theorem for the full lambda-calculus.
tree tree systems class evaluation translation process completeness sequence applications rules order practical flexibility recursion value values definition parallel programming mean lambda calculus trees algorithm nondeterminism