Lambda微积分β还原

Question

我有以下蓝氏微积分：

( x ( λyz.xz ) ( λxy.zyx )) (( λyx.xyz ) ( λy.xz ))

我已经减少了：

alpha => ( x ( λyz.xz ) ( λxy.zyx )) (( λyx1.x1yz )) ( λy.xz ))
beta  => ( x ( λyz.xz ) ( λxy.zyx )) ( λx1.x1 ( λy.xz ) z )

我的问题是:为什么以下的削减是错误的？在我看来，这句话似乎很简单：

beta1 => ( x ( λyz.xz ) ( λxy.zyx )) ( λx1.x1 ( xz ))
beta2 => ( x ( λy.x ( λxy.zyx ))) ( λx1.x1 ( xz ))

Answer 1

为了避免混淆，我建议再重命名一点。因此，在“作用域”中似乎有x和z (它们在术语中不受任何λ的约束)，确定是否引用它们是一个好主意。

我会像这样改写你的任期：

(x (λy1,z1. x z1) (λx2,y2. z y2 x2)) ((λy3,x3. x3 y3 z) (λy4. x z))

我在重命名方面做了相当多的工作(当然，这是不必要的，但就像这样，我们确定哪个是哪个)。

这个术语β-减少到

(x (λy1,z1. x z1) (λx2,y2. z y2 x2)) ((λx3. x3 (λy4. x z) z))

然后

(x (λy1,z1. x z1) (λx2,y2. z y2 x2)) ((λx3. x3 (λy4. x z) z))

这确实是阿尔法-相当于你写的东西。那么，您要做的就是将(λy4. x z)应用于z。您不应该这样阅读x3 (λy4. x z) z，它也可以用更多的括号(如这个(x3 (λy4. x z)) z )来编写。不知何故，这个词被卡住了，因为它的头是一个变量。

没有什么可以做的，因为这个术语也涉及到一个不能减少的应用程序。也许您还可以通过eta还原将(λy1,z1. x z1)重写为(λy1. x)。

因此，您不能获得(x (λyz.xz) (λxy.zyx)) (λx1.x1 (x z))，而且出于同样的原因，您不能将其简化为(x (λy.x (λxy.zyx))) (λx1.x1 (x z))，因为您的括号错误。

从左到右读取f x y，取f并将其应用于x，然后将结果应用于y。

Answer 2

我会把这个答案保留得很简单。

若要减少到beta1或beta2，请注意在"x1 (λy.xz ) z“中有"x1 ( (λy.xz )z ) "，因此可以减少.，即将最后两个表达式(λy.xz )和z放在一起，这是错误的。

这不是它的工作方式。在减少lambda表达式时，您应该维护左结合性，即总是将最左边的表达式分组为“( x1 (λy.xz ) ) z”，而不是"x1 ( (λy.xz )z)E 213，这是错误的。

如果有像E1 E2 E3 E4这样的表达式，

您应该将其分组为(( (E1 E2) E3 ) E4 ))

因此，对于beta2，不能将x1 (λy.xz )z还原为"x1 ( xz )“。同样的逻辑也适用于beta1。

我希望这对你有意义。