INFINITE TREES IN NORMAL FORM AND RECURSIVE EQUATIONS HAVING A UNIQUE SOLUTION

A system of recursive equations is C-univocal if it has a unique solution modulo the equivalence associated with a class C of interpretations. This concept yields simplified proofs of equivalence of recursive program schemes and correctness criteria for the validity of certain program transformations, provided one has syntactic easily testable conditions for C-univocality. Such conditions are given for equational classes of interpretations. They rest upon another concept: the normal form of an infinite tree with respect to a tree rewriting system. This concept yields a simplified construction of the Herbrand interpretation of certain equational classes of interpretations. © 1979 Springer-Verlag New York Inc.