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)のあたりが…