Comparing Curried and Uncurried Rewriting
Comparing Curried and Uncurried Rewriting
复制标题
比较柯里化和非柯里化重写
DOI：
10.1006/jsco.1996.0002
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
F. D. Vries
中科院分区：
文献类型：
--
作者：
R. Kennaway;J. Klop;R. Sleep;F. D. Vries
抽象咖喱是术语改写系统的转换，可能包含任意arity的符号，其中仅包含无效符号，以及一个称为应用的单个二进制符号。通过这种转变来保留：强大的归一化，弱化，教会较弱，完整性，半完整性以及不同正常形式的非转换性。在左线性的条件下，我们显示了属性NF的保存（如果术语降低为正常形式，则其降低均减少到相同的正常形式）和un→（最多降低了一个术语为正常形式形式）。我们对非左线性系统的NF和UN→UN的准备。结果扩展到部分咖喱（其中符号的某些子集被咖喱），这意味着适用系统的工会的某些模块化属性。
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.