如何控制按值调用中的评估顺序？

Question

我对按值调用 lambda 演算有一些疑问。

1) λx.(λy.y)x 是一个卡住项还是应该计算为 λx.x？

2) λx.(λy.y)(λz.z)，这个呢？

3) 执行中如何控制求值顺序？

我感到很困惑，谁能解释一下这些值，卡住的术语，评估的顺序，如何控制？

提前致谢！

Answer 1

1) λx.(λy.y)x 是一个卡住项还是应该计算为 λx.x？

从术语和子术语的角度进行思考会有所帮助。在这里，我们有：

• 抽象，λx. (λy.y)x，具有：
  • 一个应用程序 (λy.y)x，它适用
    • λy.y（一个抽象，用简单的术语y）到
    • x.

应用程序可以转换，因此我们得到：

• 一个抽象，λx. x，因为应用程序重写为 x。这也写成组合子I。

λx.(λy.y)x 不是一个卡住项：一个项被卡住如果它不能被转换。

2) λx.(λy.y)(λz.z)，这个呢？

理想情况下，您现在尝试自己做。

我们有：

• 一个抽象，λx. (λy.y)(λz.z)，具有：
  • 一个应用程序，适用
    • 抽象 λy.y 到
    • 抽象 λz.z.

我们可以使用 y=(λz.z) 对应用进行变换，得到：λx.(λz.z)，可以简写为 λxz.z 或 K*。

3) 执行中如何控制求值顺序？

你不能。 Lambda 演算没有定义它。它是一种计算模型，而不是一种编程语言。由于 lambda 演算是confluent，因此对术语的任何计算都将产生相同的范式如果它产生一个范式。也就是说，每一项最多只有一个范式，但可能存在无限的求值路径。

例如，术语 KIΩ 具有无限的归约路径，因为它归约为自身（通过将 Ω ≡ ωω ≡ (λz.zz)(λz.zz) 归约到自身），同时它也可以通过以下方式归约为 I应用 K ≡ λxy.x.

因此，基于 lambda 演算的语言中的技巧是选择一种求值策略，该策略将产生一个范式（如果存在）。最基本的策略是"leftmost outermost" 策略，也称为正常顺序评估，它总是选择可以应用的最左边的 λ 抽象。它是低效的，但保证产生一个范式（如果存在）。

在编程语言中，必须应用技巧来提高评估效率。最常见的是，这包括 strictness analysis 和 graph rewriting。