COMPARING CURRIED AND UNCURRIED REWRITING

Currying is a transformation of term rewrite systems which may contain symbols of arbitrary arity into systems which contain only nullary sy mbols, together with a single binary symbol called application. We sho w that for all term rewrite systems (whether orthogonal or not) the fo llowing properties are preserved by this transformation: strong normal ization, weak normalization, weak Church-Rosser, completeness, semi-co mpleteness, and the non-convertibility of distinct normal forms. Under the condition of left-linearity we show preservation of the propertie s NF (if a term is reducible to a normal form, then its reducts are al l reducible to the same normal form) and UN--> (a term is reducible to at most one normal form). We exhibit counterexamples to the preservat ion of NF and UN--> for non-left-linear systems. The results extend to partial currying (where some subset of the symbols are curried), and imply some modularity properties for unions of applicative systems. (C ) 1996 Academic Press Limited