Comparing curried and uncurried rewriting
Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, Vries, F.-J. (Fer-Jan) de · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1993
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 leftlinearity 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.