「(λx.M(xx))(λx.M(xx))→ M(λx.M(xx)(λx.M(xx)))」

「(λx.M(xx))(λx.M(xx))→ M(λx.M(xx)(λx.M(xx)))」で詰まった。

と書いたけど、普通に書いたら問題なかった件を書いておく。

左辺の(λx.M(xx))(λx.M(xx))について、判りやすさのために、Nを以下のように定義する。

N = M

で、左側の(λx.M(xx))を書きかえる。ラムダの文字xはyと書き変えても問題がない。*1

(λx.M(xx)) = (λy.N(yy))

で、元の左辺を書き変えてみる。

(λx.M(xx))(λx.M(xx)) = (λy.N(yy))(λx.M(xx))

これはつまり、(λy.N(yy))という関数に対して、パラメータ(λx.M(xx))を与えているという式になる。で、λyについて解くと、y = λx.M(xx)となって、

(λx.M(xx))(λx.M(xx)) = (λy.N(yy))(λx.M(xx))
                       = N((λx.M(xx))(λx.M(xx)))
　　　　　　　　　　　　　　↑一つ目のy ↑
　　　　　　　　　　　　　　　　として　↑二つ目のyとして

で、M = Nなので、

(λx.M(xx))(λx.M(xx)) = (λy.N(yy))(λx.M(xx))
                       = N((λx.M(xx))(λx.M(xx)))
                       = M((λx.M(xx))(λx.M(xx)))

はい、できた。超丁寧に解くと、こんな感じかな。

関数とそれに対するパラメータを意識して読むと、かなり単純なことがわかりました。

それにしても括弧が多すぎ。慣れるまでは、ノートに手書きで括弧を書き分けながら解いていくのがお勧めかも。

*1:ruby等でのクロージャの文字を変えるのと同じ意味。（でよいよね？）