Lambda演算β减少具体步骤和原因

Question

从我最近阅读的一本书:

第一:

.(..)()((.)) 在这一点上,最外层的lambda绑定是不可简化的,因为它没有适用的参数.剩下的就是一次一层地进入术语,直到我们找到可以减少的东西.

下一个:

.(.)((.)) 我们可以将lambda绑定应用于参数.我们一直在寻找可以申请的条款.我们可以应用的下一件事是lambda绑定到lambda术语((.)).

我不明白.在第一部分,它说 has no argument to apply to, that I can probably understand, but then at the Next section I think the z可以被束缚,((.))因为正如你所看到的,.(.)身体 clearly has a z论点可以是界.但是,这本书恰恰忽略了头 and directly bound n到((.)).我的意思.是没有n争论,为什么它会受到约束？

有人可以向我解释一下吗？

Answer 1

使用正常的订单评估,您可以获得两次beta减少的答案

// beta reduction 1
?z.(?m.?n.m)(z)((?p.p)z) ?? (?n.m) [m := z]
?z.(?m.?n.z)(z)((?p.p)z)

// beta reduction 2
?z.(?n.z)((?p.p)z)       ?? z      [n := ((?p.p)z)]
?z.(?n.z)((?p.p)z)

// result
?z.z

第二次减少可能看起来很棘手,因为它n是必然的,((?p.p)z)但表达式只是z,因此n被抛弃了.

使用应用订单评估,需要一个额外的步骤

// beta reduction 1
?z.(?m.?n.m)(z)((?p.p)z) ?? p      [p := z]
?z.(?m.?n.m)(z)((?p.z)z)

// beta reduction 2
?z.(?m.?n.m)(z)(z)       ?? (?n.m) [m := z]
?z.(?m.?n.z)(z)(z)

// beta reduction 3
?z.(?n.z)(z)             ?? z      [n := z]
?z.(?n.z)(z)

// result
?z.z

在这种情况下,无论我们使用正态订单评估还是应用订单评估,结果都是相同的.不同的评估策略有时会评估不同的结果.

重要的一点是,我们上面所做的减少步骤在应用之前 不会发生?z(取决于实施).在您提供的示例代码中,?z从未应用过,因此?z在这种情况下,简化术语仅适用于练习.

我们所做的就是展示lambda 等价(在两种不同的评估策略下)

?z.(?m.?n.m)(z)((?p.p)z) <=> ?z.z

Answer 2

Lambda表示法有点奇怪。IMO Haskell语法更清晰：

\z -> (\m -> \n -> m) z ((\p -> p) z)

或者，甚至更明确

\z -> (
        (
           ( \m -> (\n -> m) )
           z
        )
        ( (\p -> p) z )
      )

第一步减少是

\z -> (
        (
           (\n -> z)
        )
        ( (\p -> p) z )
      )

要么

\z -> (
        (\n -> z)
        ( (\p -> p) z )
      )

那么你的确可以绑定((\p -> p) z)-不z，而是n！（实际上根本没有使用。）

\z -> (
        (z)
      )

或简单地说\z -> z。因此，我们仍然有那个zlambda，正如书中所说的那样，这是难以置信的。我们别无其他！

...我不确定这是否真的是你的问题。如果是这样：我为什么不首先要看看是否可以减少((\p -> p) z)，那么答案是，lambda演算本身根本没有定义这一点（它只是定义了可以应用的转换，而不是定义的顺序）应该这样做。^{实际上我不确定，如果我错了，请更正我}）。如果使用严格的语言（例如Scheme），您确实会先减少((\p -> p) z)；Haskell不会这样做，因为没有必要。无论哪种方式，都没有关系，因为结果还是被丢弃了。

   ( \z -> (\n -> z) ((\p -> p) z) )
?  ( \z -> (\n -> z) z )
?  ( \z -> (\n -> z) foo )
?  ( \z -> z )