基于术语重写的评估如何工作？

Question

纯编程语言是apparently based on term rewriting，而不是传统上作为外观相似语言基础的 lambda 演算。

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

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

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

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

Answer 1

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

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

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

-- 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)

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

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