贝塔减少拉姆达演算
问题描述:
我试图减少以下使用测试版还原:贝塔减少拉姆达演算
(λx.x x) (λx. λy.x x)
我陷入第一次换人后,因为它似乎是给(λx. λy.x x)(λx. λy.x x)
这将在怎样的一个循环的结束。我究竟做错了什么?
答
这里的评价
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表达式不具有头标准形式。它永远不会达到正常形式。
答
你没有做错什么。
表达 (λ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)
感谢您的好解释 –