次の式が与えられます：
((λ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) -> ?
ありがとう
を使用\してλ:
((\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)
は彼らの名前です。それにもかかわらず、それらは異なる変数です。