| Comparing Curried and Uncurried Rewriting (1998) | |||||||||||||||
Abstract | |||||||||||||||
| this paper we show that strong normalization (SN), weak normalization (WN), the weak Church-Rosser property (WCR), the unique normal form property (UN), completeness, and semi-completeness are preserved by currying. For left-linear term rewrite systems we show that currying also preserves the normal form property (NF) and the UN # property. (All these properties are defined in Section 2.5.) Counterexamples demonstrate that NF and UN # are not always preserved for non-left-linear systems. We also explore connections between currying and modular properties. Kahrs, 1994 has recently shown that the Church-Rosser property (CR) is preserved by currying for all rewrite systems. This corrects an error in an earlier version of this paper, which proved preservation of CR for left-linear systems, but claimed a counterexample for non-left linear systems. We use two di#erent definitions of currying: Schonfinkel's original definition, and a di#erent definition which is not equivalent, but is technically easier to work with. For every term rewrite system, and for each of the properties mentioned above, we prove that the property is preserved for that system by one form of currying if and only if it is preserved by the other. In addition, we consider partial currying, in which the currying transformation is applied to only some of the symbols of the system. All our results for full currying also apply to partial currying. Finally, we consider the modularity of these properties with respect to unions of curried rewrite systems. 2. Preliminaries | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||