1

我正在阅读有关 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

那是对的吗？还是我错误地减少了它？

4

2 回答 2

2

在表达式中

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1

您正确地改写为

(λx.(λt.λy.t × y) 3 ((λz.x + z) 2)) 1

该x变量绑定到外部 lambda 抽象λx。
事实上，减少术语(λx.λy.x × y) 3不可能改变术语(λz.x + z)，因为它位于 redex 树的另一个分支中。

这本书清楚地指出，15 是错误的结果

给出的示例是一个反例，说明如果天真地实施惰性评估会发生什么。

惰性求值理论上是通过normal order实现的，但这只是一种理论结构，存在一些实际缺陷。
因此，使用了按需调用等策略。

这本书只是想展示一个可能的、抽象的、上述评估策略的实现。

作为参考，这里使用正常顺序的表达式完全还原。

(\x.(\x.\y.x * y) 3 ((\z.x + z) 2)) 1


          ()
         /  \
       \x    1
        | 
       ()
      /   \
    ()     ()
   /  \   /  \
 \x    3 \z   2
  |       |
 \y       +
  |      x z
  *
 x y



---------------------------------------

(\x.\y.x * y) 3 ((\z.1 + z) 2)


       ()
      /   \
    ()     ()
   /  \   /  \
 \x    3 \z   2
  |       |
 \y       +
  |      1 z
  *
 x y


---------------------------------------


\y.3 * y ((\z.1 + z) 2)


       ()
      /   \
    .'     ()
   /      /  \
 \y      \z   2
  |       |
  *       +
 3 y     1 z

---------------------------------------


3 * ((\z.1 + z) 2)


     *
   /  \
  3   ()
     /  \
    \z   2
     |
     +
    1 z


---------------------------------------


3 * (1 + 2)


     *
   /  \
  3   1 + 2

---------------------------------------

3 * 3

  *
 / \
3   3

---------------------------------------

9
于 2016-08-21T09:24:14.020 回答
2

@MargaretBloom 的树可视化很棒，是的，这本书只是展示了一个潜在的陷阱。

我将提供此作为查看减少的另一种方式。

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1   →β x + z [x := 1]
(λx.(λx.λy.x × y) 3 ((λz.1 + z) 2)) 1
(λx.λy.x × y) 3 ((λz.1 + z) 2)          →β x × y [x := 3]
(λx.λy.3 × y) 3 ((λz.1 + z) 2)
(λy.3 × y) ((λz.1 + z) 2)               →β 3 × y [y := ((λz.1 + z) 2)]
(λy.3 × ((λz.1 + z) 2)) ((λz.1 + z) 2)
3 × ((λz.1 + z) 2)                      →β 1 + z [z := 2]
3 × ((λz.1 + 2) 2)
3 × (1 + 2)                             →β 1 + 2 [ 1 + 2 := 3 ]
3 × 3                                   →β 3 × 3 [ 3 × 3 := 9 ]
9
于 2016-08-31T17:03:36.750 回答