Comparing curried and uncurried rewriting

Abstract

Currying is a transformation of term rewrite systems which may contain symbols of arbitrary arity into systems which contain only nullary symbols, together with a single binary symbol called application. We show that for all term rewrite systems (whether orthogonal or not) the following properties are preserved by this transformation: strong normalization, weak normalization, weak Church-Rosser, completeness, semi-completeness, and the non-convertibility of distinct normal forms. Under the condition of left-linearity we show preservation of the properties NF (if a term is reducible to a normal form, then its reducts are all reducible to the same normal form) and UN→ (a term is reducible to at most one normal form). We exhibit counterexamples to the preservation 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. © 1996 Academic Press Limited.