7. 归约策略¶
7.1. 应用序（Applicative Order）¶
表达式 \((\lambda x.m \; (\lambda x.(x \; x) \; \lambda x.(x \; x)))\) 中有多少个 \(\beta\) 可归约式？你应该能找到两个。根据你先归约哪一个，你最终得到的"答案"可能是 \(m\)，也可能是与你开始时间完全相同的那个表达式，也就是说，\(\beta\)-归约意义上的无限循环。
我们已经看到，对 \(\lambda\) 演算中表达式的求值本质上是 \(\beta\)-归约，它可以简单地用替换来定义： \((\lambda p.b \; a) \equiv subst(a,p,b)\)
但还有一个额外的因素需要考虑：前面那个 \(\beta\) 可归约式中的 \(a\) 和 \(b\) 本身可能包含 \(\beta\) 可归约式。我们需要递归地归约它们，这就提出了以下问题：
我们应该先归约哪个可归约式，顶层的可归约式，还是嵌套在内部的可归约式？
先归约哪一个有关系吗？这两种策略的后果是什么？
不同的归约策略会得到不同的结果吗？
部分回答上面第二个和第三个问题的关键是 丘奇-罗瑟定理（Church-Rosser Theorem） ，我们只陈述而不证明。根据丘奇-罗瑟定理， 如果两种不同的归约策略都得到了某个答案，那么它们将得到相同的答案。
因此，第二个和第三个问题的答案是否定的，但要加上这样的告诫：任何能得到答案的归约策略都会给出相同的答案。这里的关键是这个策略到底会不会得到答案，而丘奇-罗瑟定理既不保证停机，也不保证在答案存在时一定能找到答案。当某个策略得到的答案不能再进一步归约时，我们就说这个表达式处于 beta 范式中 （或 \(\beta\)-范式）。
JavaScript 在其替换计算模型中使用策略称为 应用序归约（applicative order reduction） 。采用这种策略，要求值形如 f(arg1, arg2, arg3, ...) 的表达式，我们：
从左到右对每个子表达式求值（如果 f 需要求值的话，也包括它）。（怎样才会需要求值呢？）
把最左边的结果——它应该是一个函数——应用于其余已经求值的子表达式。
应用序策略的特点是从左到右进行，先求值最内层的子表达式。也就是说，只有当每个子表达式都被归约、并且除了最顶层的应用之外不再存在任何可归约式时，我们才执行一次应用。考虑：
\((\lambda x.((x \; y) \; (y \; x)) \; (\lambda w.(w \; w) \; z))\)
应用序求值会先归约 \((\lambda w.(w \; w) \; z)\)，得到 \((z \; z)\)。然后这个结果会被替换到 \(((x \; y) \; (y \; x))\) 中的 \(x\)，得到 \((((z \; z) \; y) \; (y \; (z \; z)))\) 作为最终答案。
尽管应用序归约在上面的问题中经过两步就找到了答案，但当它用于本节考虑的第一个例子时，即
\((\lambda x.m \; (\lambda x.(x \; x) \; \lambda x.(x \; x)))\)
我们会陷入前面提到的无限循环。
7.2. 标准序（Normal Order）¶
标准序归约（normal order reduction） 先归约最左边的 \(\beta\) 可归约式，然后再归约它内部的子表达式以及它后面的子表达式。应用序是先求值子表达式、然后再应用函数，而标准序求值则是先应用函数、然后再求值子表达式。换句话说，标准序归约总是寻找最左边最外层的归约，而应用序总是寻找最左边最内层的归约。
因为标准序归约推迟了对函数实参的求值，所以当用于曾经让应用序无限循环的那个例子 \((\lambda\)x.m (\(\lambda x.(x \; x) \; \lambda x.(x \; x)))\) 时，它能正确地得到 \(m\)。
现在，把它用于 \((\lambda x.((x \; y) \; (y \; x)) \; (\lambda w.(w \; w) \; z))\) 时，标准序会把 \((\lambda w.(w \; w) \; z)\) 替换为 \(((x \; y) \; (y \; x))\) 中的两次 \(x\) 出现。然后它在得到最终答案 \((((z \; z) \; y) \; (y \; (z \; z)))\) 之前，必须 两次 对 \((\lambda w.(w \; w) \; z)\) 求值。
如果你仍然不能确定应用序与标准序之间的确切区别，可以使用下面的可视化工具，在各种随机的 \(\lambda\) 表达式上观察它们各自经历的步骤。一旦你有信心总是能预测可视化的下一步，就可以去做下面给出的练习了。
7.3. Beta 归约顺序（1）¶
下面的问题关注 \(\lambda\) 表达式在使用我们讨论过的两种求值策略进行求值时，其第一步（即 \(\beta\)-归约）。要获得这个随机练习的学分，你必须连续三次答对。
7.4. Beta 归约顺序（2）¶
在下面的问题中，你必须用我们讨论过的两种求值策略研究一个 \(\lambda\) 表达式的完整求值过程。要获得这个随机练习的学分，你必须连续三次答对。
7.5. 应用序熟练度练习¶
在下面的问题中，你必须对一个随机选择的 \(\lambda\) 表达式进行完整的求值，也就是说，执行尽可能多的 \(\beta\)-归约，直到达到 \(\beta\) 范式。对于这个问题，你必须使用 应用序 归约策略。要获得这道题的学分，你只需要正确解决一个问题实例。然而，每个问题实例包含多个步骤，你必须全部正确完成（本例中，每一步都是一次 \(\beta\)-归约）。请仔细阅读并遵循操作说明。注意，存在正确答案（称为 参考答案 ）。不过，如果你查看了它，你将无法获得当前问题实例的学分。要获得另一次机会，请点击 重置 按钮开始一个新的问题实例。
7.6. 标准序熟练度练习¶
在下面的问题中，你必须对一个随机选择的 \(\lambda\) 表达式进行完整的求值，也就是说，执行尽可能多的 \(\beta\)-归约，直到达到 \(\beta\) 范式。对于这个问题，你必须使用 标准序 归约策略。要获得这道题的学分，你只需要正确解决一个问题实例。然而，每个问题实例包含多个步骤，你必须全部正确完成（本例中，每一步都是一次 \(\beta\)-归约）。请仔细阅读并遵循操作说明。注意，存在正确答案（称为 参考答案 ）。不过，如果你查看了它，你将无法获得当前问题实例的学分。要获得另一次机会，请点击 重置 按钮开始一个新的问题实例。
