Yコンビネータ（不動点演算子）の導出法

MinCamlのページからリンクされているのにプログラミング言語の話題が（あまり）ないのはイマイチなので、突発プチ・チュートリアル開始。

純粋なλ計算で再帰関数を表すのに使う

λf.(λg.f(g g)) (λg.f(g g))

というλ式があります（これだと型があったりcall-by-valueな言語は駄目ですが、とりあえず型なし＆call-by-nameとして）。どこからこんな式が出てくるのか、恥ずかしながら、ついこの間まで導き方を知らなかったのですが、ふとしたことから気づいたので書いておきます。

let rec g = F(g) in g

という再帰関数があったとします。ただし、F(g)というのはgが含まれる何らかの式です。これを

let g = (gを含まない式) in g

のように、gの定義の右辺にg自身が出現しない形で書きたいわけです。もちろん、素朴に

let g = F(g) in g

などとしても、F(g)の中に含まれるgが定義されないので駄目です。そこで、「まだ定義されていないけど、これから定義する」自分自身gを「後から受け取る」ように

let g' = λg.F(g g) in (g' g')

とします。g'というのが、「gを受け取り、それを使ってgの定義を返す」ような関数です。ここでg'の定義をインライン展開すれば

(λg.F(g g)) (λg.F(g g))

となります。これを使うと、はじめの再帰関数

let rec g = F(g) in g

は

(λg.F(g g)) (λg.F(g g))

と表せます。以上の議論は任意のFについて成立するので、Fをλ抽象して

λf.(λg.f(g g)) (λg.f(g g))

というλ式が導出できます。

…って、まだわかりにくいですね。特にλg.F(g g)のあたりが…