贝塔减少拉姆达演算

Question

我试图减少以下使用测试版还原：

(λx.x x) (λx. λy.x x)

我陷入第一次换人后，因为它似乎是给(λx. λy.x x)(λx. λy.x x)这将在怎样的一个循环的结束。我究竟做错了什么？

Answer 1

这里的评价

beta reduction 1 
(λx.xx) (λx.λy.x x)    →β x [x := (λx.λy.x x)] 
(λx.(λx.λy.x x)(λx.λy.x x)) 

beta reduction 2 
(λx.λy.xx) (λx.λy.x x)   →β x [x := (λx.λy.x x)] 
(λx.λy.(λx.λy.x x)(λx.λy.x x)) 

result 
λy.(λx.λy.x x) (λx.λy.x x)

现在，我们已经达到了弱头范式的说明 - 即我们有一个lambda λy不带任何参数应用它来。

要得到主管范式，我们可以尝试减少拉姆达下...​​

reduction 1 
λy.(λx.λy.xx) (λx.λy.x x)  →β x [x := (λx.λy.x x)] 
λy.(λx.λy.(λx.λy.x x)(λx.λy.x x)) 

reduction 2 ... 
λy.λy.(λx.λy.x x) (λx.λy.x x) 

好了，我们马上就可以看到，这种模式将会重演。每次我们尝试在lambda下进行缩小时，结果都会被包装在另一个λy中。因此，这个特定的lambda表达式没有头标准形式 - 即这个表达式的评估（当应用于参数时）将永远不会终止;因此，这个特定的lambda表达式不具有头标准形式。它永远不会达到正常形式。

Answer 2

你没有做错什么。

表达 (λx.x x) (λx. λy.x x)的β-减少在一个步骤中(λx. λy.x x)(λx. λy.x x)，其中β-内减少到λy.(λx. λy.x x)(λx. λy.x x)再到λy.λy.(λx. λy.x x)(λx. λy.x x)。
在每一步中，每个新表达式都与以前相同，但包含在新的抽象中。

在Lambda微积分中，缩减过程可能不会终止。换句话说，程序可能不会终止（就像任何图灵完全编程语言一样）。

的另一个例子是长期Ω = (λx.x x)(λx.x x)