λ計算について

質問

λ項fixを
fix≡(λxy.(y(xxy)))(λxy.(y(xxy)))
で定義したとき、任意のMについて、複数回（0回、1回も含む）のβ簡約を施すと
、
(fix M)はM(fix M)になるらしいんですが、どういう過程を経てこの結果が出てく
るのかわからないので教えてください。

fixをよく見ると、二つの(λxy.(y(xxy)))を演算させたものになっていますよね
。だから
A=(λxy.(y(xxy))) とでも置いて、何かを施せばいいのではないかと思いますが
、よくわかりません。
回答よろしくお願いいたします。

回答No.1

Tacosan · ベストアンサー

「(fix M) が M(fix M) になる」ということなんだから, fix だけを眺めていてもしょうがないよね.
(fix M) に対して λ計算の手続を粛々と実行すればいい.

お礼

ありがとうございます。
わからないところがあったらまた質問します。