查找使用的β減少

Question

考慮下面的表達式範式：

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

我想用公測減少查找其正常形態。

我的計算：

((λ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) 

他們的名字。儘管如此，它們仍然是不同的變量。