减少这个 lambda 表达式

Question

我正在尝试减少 beta 值，但我对如何减少这个问题感到困惑：

(λx((λy.x)(λx.x))x)y

最外层的λx显然会被y代替，但我还要继续减少((λy.x)(λx.x))吗？我在这里错过了什么？

Answer 1

I’m trying to practice beta reduction but I’m stuck on how to reduce this problem:

(λx((λy.x)(λx.x))x)y

要执行第一个 β 归约，您必须查看受外部 λx 约束的变量 x，它们是

(λx((λy.x)(λx.x))x)y
        ^        ^  

请注意，在内部 λx.x 中隐藏了外部 lambda，因为它使用相同的变量名。所以这里的绑定 x 绑定到这个内部 lambda，而不是外部 lambda。

另一个问题是，如果您用 y 替换 λy.x 中的 x，那么 y 会被外层 lambda 捕获。这不可能发生，因此您需要对 λy.x 执行 α 转换（重命名）以避免被捕获。

所以首先是 α-转换，然后是 β-还原

  (λx((λy.x)(λx.x))x)y
→ (λx((λz.x)(λx.x))x)y
→    ((λz.y)(λx.x))y

如果您想继续，那么 λz.y returns y 对于任何输入，

  ((λz.y)(λx.x))y
→ yy

---

注意λ演算没有设置归约策略，它只是建立项之间的等价关系。所以你可以选择另一个减单。例如，您可以先 β-reduce 内部 β-redex (λy.x)(λx.x)。

  (λx((λy.x)(λx.x))x)y
→ (λx(xx)y
→ yy

这样可以避免 α 转换。