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

Question

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

1) λx.(λy.y)x 是一个卡住的术语或者应该计算为 λx.x?

2) λx.(λy.y)(λz.z),这个呢?

3)实现中如何控制求值顺序？

我很困惑，谁能解释一下这些值，stuck term，评估顺序，如何控制？

提前致谢！

Answer 1

1) λx.(λy.y)x is a stuck term or should be evaluated to λ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), what about this one?

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

我们有：

• 一个抽象，λx. (λy.y)(λz.z)，具有：
  • 申请，申请
    • 抽象λy.y到
    • 抽象λz.z.

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

3) how to control the order of evaluation in implementation?

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

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

将其简化为 I

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

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