我正在阅读有关 lambda 演算的内容。从此处http://www.toves.org/books/lambda/第 2.1 节的末尾开始:
(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1 ⇒ (λx.λy.x × y) 3 ((λz.x + z) 2) where x = 1
⇒ (λy.x × y) ((λz.x + z) 2) where x = 3
⇒ x × y where x = 3 and y = (λz.x + z) 2
⇒ x × y where x = 3 and y = x + z and z = 2
⇒ x × y where x = 3 and y = 5 and z = 2
⇒ 15
它说
事实上,尽管如此,y 应该达到 3 而不是 5,因为第一次 beta-reduction 应该将 1 插入到表达式中 x 的位置。出于这个原因,惰性参数必须在每次归约时保留当前变量上下文,在这种情况下记住表达式 λy.x × y 内的 x = 3 但在表达式外保持 x = 1 的事实。
但是我对 beta 减少期间的操作顺序感到困惑。不幸的是,这里的解释是模棱两可的。它们可能意味着 x 应该在 (λx.λy.x × y) 内为 1,然后 y = 3 因为这是要传入的下一个参数,并且 x 已经设置(感觉不对),或者我们走下面的路线:
我们是否同意 (λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1
与 (λx.(λt.λy.t × y) 3 ((λz. x + z) 2)) 1
x 是一个界限吗?不应该是1吗?
这意味着当我们减少它时: (λt.λy.t × y) 3 ((λz.1 + z) 2)) x = 1 (λy.3 × y) ((λz.1 + z) 2)) x = 1, t = 3 3 × ((λz.1 + z) 2)) x = 1, t = 3, y = ((λz.1 + z) 2)) 3 × ((λz.1 + z) 2)) x = 1, t = 3, y = ((λz.1 + z) 2)), z = 2 3 × (1 + 2) x = 1, t = 3, y = ((λz.1 + z) 2)), z = 2 3 x 3 = 9
那是对的吗?还是我错误地减少了它?