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. |
Year | DOI | Venue |
---|---|---|
1996 | 10.1006/jsco.1996.0002 | J. Symb. Comput. |
DocType | Volume | Issue |
Journal | 21 | 1 |
ISSN | Citations | PageRank |
Journal of Symbolic Computation | 26 | 1.45 |
References | Authors | |
9 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Richard Kennaway | 1 | 435 | 47.65 |
Jan Willem Klop | 2 | 1498 | 161.90 |
Ronan Sleep | 3 | 180 | 13.38 |
Fer-Jan de Vries | 4 | 244 | 21.67 |