15

纯编程语言显然是基于术语重写，而不是传统上作为外观相似语言基础的 lambda 演算。

...这有什么定性和实际的区别？事实上，它评估表达式的方式有什么不同？

链接页面提供了许多有用的术语重写示例，但它实际上并没有描述它与函数应用程序的不同之处，只是它具有相当灵活的模式匹配（并且出现在 Haskell 和 ML 中的模式匹配很好，但不是评估策略的基础）。值与定义的左侧匹配并替换到右侧 - 这不只是 beta 减少吗？

模式匹配和替换为输出表达式，表面上看起来有点像syntax-rules我（甚至是卑微的#define），但其主要特征显然是它发生在评估之前而不是评估期间，而 Pure 是完全动态的并且有在它的评估系统中没有明显的相位分离（事实上，Lisp 宏系统在其他方面总是对它们与函数应用程序没有什么不同而大吵大闹）。能够操作符号表达式值很酷，但也似乎是动态类型系统的产物，而不是评估策略的核心（很确定您可以重载 Scheme 中的运算符来处理符号值；事实上您甚至可以使用表达式模板在 C++ 中执行此操作）。

那么，当两者都发生替换时，术语重写（Pure 使用的）和传统函数应用程序（作为评估的基础模型）之间的机械/操作差异是什么？

4

1 回答 1

11

术语重写不必看起来像函数应用程序，但是像 Pure 这样的语言强调这种风格，因为 a) beta-reduction 很容易定义为重写规则，b) 函数式编程是一种易于理解的范例。

一个反例是黑板或元组空间范式，术语重写也非常适合。

beta-reduction 和 full-term-rewriting 之间的一个实际区别是，重写规则可以对表达式的定义进行操作，而不仅仅是它的值。这包括对可约表达式的模式匹配：

-- Functional style
map f nil = nil
map f (cons x xs) = cons (f x) (map f xs)

-- Compose f and g before mapping, to prevent traversing xs twice
result = map (compose f g) xs

-- Term-rewriting style: spot double-maps before they're reduced
map f (map g xs) = map (compose f g) xs
map f nil = nil
map f (cons x xs) = cons (f x) (map f xs)

-- All double maps are now automatically fused
result = map f (map g xs)

请注意，我们可以使用 LISP 宏（或 C++ 模板）来做到这一点，因为它们是一个术语重写系统，但这种风格模糊了 LISP 对宏和函数的清晰区分。

CPP 的 #define 不等效，因为它不安全或不卫生（语法上有效的程序在预处理后可能变得无效）。

我们还可以根据需要为现有函数定义临时子句，例如。

plus (times x y) (times x z) = times x (plus y z)

另一个实际考虑是，如果我们想要确定性的结果，重写规则必须是汇合的，即。无论我们应用规则的顺序如何，我们都会得到相同的结果。没有算法可以为我们检查这一点（通常无法确定），并且搜索空间太大，单个测试无法告诉我们太多信息。相反，我们必须通过一些正式或非正式的证明来说服自己，我们的系统是融合的；一种方法是遵循已知的融合系统。

例如，已知 beta-reduction 是合流的（通过Church-Rosser 定理），所以如果我们以 beta-reduction 的方式编写所有规则，那么我们可以确信我们的规则是合流的。当然，这正是函数式编程语言所做的！

于 2014-07-16T08:55:57.430 回答