Lambda 演算 - 评估这些惰性参数

Question

我正在阅读 lambda 演算。从第 2.1 节的末尾开始 http://www.toves.org/books/lambda/:

(λ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

它说

In fact, though, y should attain the value 3 rather than 5 since the first beta-reduction should plug 1 into x's spot in the expression. For this reason, a lazy parameter must preserve the current variable context with each reduction, remembering in this case that x = 3 within the expression λy.x × y but maintaining the fact that x = 1 outside the expression.

但我对 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

对吗？还是我不正确地减少了它？

Answer 1

表达式中

(λ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 实现的，但这只是一个理论构造，存在一些实际缺陷。
因此，改为使用 call-by-need 等策略。

这本书只是想展示一种可能的、抽象的、实施上述评估策略的方法。

作为参考，此处使用表达式的正常顺序进行完整缩减。

(\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

Answer 2

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

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

(<b>λx.</b>(λx.λy.x × y) 3 ((λz.<b>x</b> + z) 2)) <b>1</b>   →β x + z [x := 1]
<del>(λx.</del>(λx.λy.x × y) 3 ((λz.1 + z) 2)<del>) 1</del>
(<b>λx.</b>λy.<b>x</b> × y) <b>3</b> ((λz.1 + z) 2)          →β x × y [x := 3]
(<del>λx.</del>λy.3 × y) <del>3</del> ((λz.1 + z) 2)
(<b>λy.</b>3 × <b>y</b>) <b>((λz.1 + z) 2)</b>               →β 3 × y [y := ((λz.1 + z) 2)]
<del>(λy.</del>3 × ((λz.1 + z) 2)<del>)</del> <del>((λz.1 + z) 2)</del>
3 × ((<b>λz.</b>1 + <b>z</b>) <b>2</b>)                      →β 1 + z [z := 2]
3 × (<del>(λz.</del>1 + 2<del>) 2</del>)
3 × (1 + 2)                             →β 1 + 2 [ 1 + 2 := 3 ]
3 × 3                                   →β 3 × 3 [ 3 × 3 := 9 ]
9

Lambda 演算 - 评估这些惰性参数

Lambda calculus - evaluating these lazy parameters

computer-science

lambda-calculus

computer-science-theory

书上说得很清楚，15是错误的结果