纯编程语言是 apparently based on term rewriting ，而不是传统上作为相似语言的基础的 lambda 演算。
...这有什么质的、实际的区别？事实上，它评估表达式的方式有什么不同？
链接页面提供了很多有用的术语重写示例，但它实际上并没有描述它与函数应用程序的不同之处，只是它具有相当灵活的模式匹配(并且在 Haskell 和 ML 中出现的模式匹配很好，但不是评估策略的基础)。值与定义的左侧匹配并替换到右侧 - 这不只是 Beta 减少吗？
模式的匹配，以及对输出表达式的替换，表面上看起来有点像 syntax-rules对我来说(甚至是不起眼的 #define )，但它的主要特征显然是在评估之前而不是在评估期间发生，而 Pure 是完全动态的，其评估系统中没有明显的相分离(实际上不然Lisp 宏系统总是大声疾呼它们与函数应用程序的区别)。能够操作符号表达式值很酷，但也似乎是动态类型系统的产物，而不是评估策略的核心(非常确定您可以重载 Scheme 中的运算符来处理符号值；事实上you can even do it in C++ 带有表达式模板)。
那么，当两者都发生替换时，术语重写(如 Pure 所使用的)和传统函数应用程序(作为评估的基础模型)之间的机械/操作差异是什么？
最佳答案
术语重写不必看起来像函数应用程序，但像 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-reductions 的风格编写我们的所有规则，那么我们可以确信我们的规则是融合的。当然，这正是函数式编程语言所做的!
关于functional-programming - 基于术语重写的评估如何工作？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/24330902/