lambda - 使用 beta 归约找到范式

Question

给定以下表达式：

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

我想使用 beta 减少找到它的正常形式。

我的计算：

((λx.λx.xx) (λx.xzx)) (λy.yy) ->
((λx.xzx)(λx.xzx)) (λy.yy) -> ((λx.xzx)z(λx.xzx)) (λy.yy) ->
(zzz (λx.xzx)) (λy.yy) -> ?

但是我该如何从这里继续：

(zzz (λx.xzx)) (λy.yy) -> ?

谢谢

Answer 1

用来\表示λ：

((\x.\x.xx) (\x.xzx)) (\y.yy) =
= ((*\x*.\x.xx) *(\x.xzx)*) (\y.yy) =
= (\x.( (\x.xzx) (\x.xzx) )) (\y.yy) =
= (\x.( (*\x*.xzx) *(\x.xzx)* )) (\y.yy) =
= (\x.( (\x.xzx) z (\x.xzx) )) (\y.yy) =
= (\x.( ( (\x.xzx) z) (\x.xzx) )) (\y.yy) =
= (\x.( ( (*\x*.xzx) *z*) (\x.xzx) )) (\y.yy) =
= (\x.( ( (zzz) (\x.xzx) ) (\y.yy) =
= (*\x*.( ( (zzz) *(\x.xzx)* ) (\y.yy) =
= (zzz) (\x.( (\y.yy) z (\y.yy) )) =
= (zzz) (\x.( ((\y.yy) z) (\y.yy) )) =
= (zzz) (\x.( ((*\y*.yy) *z*) (\y.yy) )) =
= (zzz) (\x.( (zz) (\y.yy) )) =
= (zzz) (\x.(zz)(\y.yy))

并且这里没有其他可用的应用程序 - 至少，只要您没有z.

另请注意，x最终展开式中有一个定义，您可能在计算过程中已将其隐藏。

所有变量 ( λx . λx . xx) 在表达式中都有共同点：

((*λx*.*λx*.xx) (λx.xzx)) (λy.yy)

是他们的名字。尽管如此，它们是不同的变量。