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

Question

来自我最近读的一本书：

第一：

????????.(????????.????????.????)(????)((????????.????)????) 最外层的 lambda 绑定？？？在这一点上是不可约的，因为它没有适用的论据。剩下的就是一次一层地进入这些术语，直到我们找到可简化的东西。

下一步：

????????.(????????.????)((????????.????)????) 我们可以应用 lambda 绑定 ????论据????。我们一直在寻找可以应用的条款。我们可以应用的下一件事是 lambda 绑定 ????到 lambda 项 ((????????.????)????)。

我不明白。在第一部分，它说 ???????? 没有适用的参数，我大概可以理解，但是在下一部分，我认为 z 可以绑定到 ((????????.????)????) 因为如您所见，@987654327 @，???????? 的主体显然有一个可以绑定的z 参数。但本书只是忽略了头部????????，直接将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

关键是 n 从未在抽象中使用。 n 仍然绑定到 ((λp.p)z)，但它会立即被丢弃。

λz.(λm.λn.m)(z)((λp.p)z) = λz.(λn.z)((λp.p)z)  Replacing m with z
                         = λz.z                Replacing n with ((λp.p)z)

Answer 3

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。所以，我们仍然拥有z lambda，正如书中所说，这是不可逆转的。我们只是没有别的东西！

---

...我不确定这是否真的是您的问题。如果是这样：为什么我们不首先看看我们是否可以减少((\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 )