高階ことりちゃんと学ぶSKIコンビネータ

ねぇ、この前ね、λ式はみんなこんな感じの関数“S”と“K”だけで表現できるって聞いたんだけど、本当?

SKIコンビネータだね。できるよ。

それってどうやってやるの? ほんとにSとKだけで全部できるの?

そう、できる。方法はいくつかあるけど、わかりやすいものとしては「λリフティング」と「α-消去」を使う方法がある。

なんか難しそう?

少しずつやっていけば大丈夫。順に説明していこう。

まず、「λリフティング」をすると、λ式をコンビネータの定義の集まりに変換できる。

ええと、つまりどういうこと?

例えば、λ式で関数を定義する場合、

こんな形になるよね。

うん。

それを、

こういう風に、複数のコンビネータの定義に変換する。右辺からλの記号が無くなるようにするんだ。

λを無くしちゃうんだ。

そう。この次の「α-消去」はλが無い式を対象にしているのでλを消しておく必要があるんだ。

じゃあこの例を見ながら説明しよう。

λリフティングのために、内側にあるλから順に消していく。まず最初は一番内側にある“λv. ((x x) v”だ。まずはコンビネータの名前を決める。名前はなんでも良いけど他と被らない名前にする。ここでは“M”にしよう。

さて、では“M ... = ...”と置いて、左側の...の部分を決めよう。

変換中の部分には変数が2つ使われているね。

えっと、つまり?

“x”と“v”。この2つはパラメータである“v”とそれ以外である“x”に分けられる。パラメータの方は「束縛変数」と言い、それ以外は「自由変数」という。

「そくばくへんすう」と、「じゆうへんすう」。

そう。それでMのパラメータは「自由変数」全てと「束縛変数」とする。

つまりこういう形になる。

順番はなんでもいいの?

順番は自由変数が先で束縛変数が後になるようにする。話が前後するけどこのあと変換中の部分をM xという式で置き変えるのでxが先じゃないといけないんだ。自由変数同士の順番は変えても良い。

さて、変換後の式の右辺なんだけどこっちは簡単で、変換中の部分の.の後ろそのままでいい。

つまり?

こうなる。

これで完成?

最後に変換前の式“Y = ...”の中で変換中の部分“λv. (x x) v”が使われていた所を“M x”で置き換える。

“M x”の後に“v”は付けなくていいの?

うん。自由変数だけを並べればいい。これで式“λv. (x x) v”のλリフティングが完了した。

ええと、まとめると、

でいいの?

うん。じゃあ次は“λf. (λx. f (M x))”でやってみよう。

まず名前を付ける。“L”とすると、こんな風になるのかな?

うん。

次に、変数は……、“f”と“x”で、“f”が自由変数、“x”が束縛変数?

合ってる。

それで右辺は.の後ろそのままだったから、じゃあこんな感じ?

うん。問題無い。

最後に変換前の式を書き換えて、こうかな?

うん。完璧。

わぁい

最後にYにも同じことをする。この場合は自由変数が無いので、次のようになる。

これでλリフティングはおしまいだ。次は「α-消去」を見てみよう。

さて、λリフティングによって、一般のλ計算の式からλを含まないような式に変換できた。ここからさらにSとKの組み合わせに変換していこう。

その前に、SとKだけだと長くてわかりづらくなってしまうので、Iというコンビネータを導入しよう。

Iはこのように、引数をそのまま返すコンビネータだ。

そのまま返すんだったら無くてもいいんじゃないの?

例えば、こんな風なコンビネータWを作りたいとする。

このとき、コンビネータWはこんな風にSとIを使って表せる。

ええと、そうなの?

式を変形すると同じになるよ。

うーん……、うん、たしかにそうだね。

それで、IはSとKで表わせるんだっけ?

そう。こんな感じで表せる。

これでIになるの?

S K Kにxを与えるとこんな風になってxが戻ってくる。

……これって、2つ目のKは使われてないの?

そう。だからS K SでもS K (K K)でもなんでもいい。S K Kと定義することが多いけどね。

さて、ではλを含まないような式について、S, K, Iだけで表してみよう。

例えば、こういうコンビネータTがあったとする。

ここから変数を1つずつ消していって、最後にはSとKとIだけにする。

これでちゃんと元のままなの?

例えば、yだけを消した式にyを与えると元の式になる。xの方も同様だ。

それで、消し方だけど、後ろの変数から先に消していく。

こんな風に式を立てて、□がわかったらyを両辺から消す。

つまり、変数yを含む式から変数yを消去するためには、□ yが元の式と同じになるような□を求めればよい。

変数yの消去を「y-消去」と言う。変数xであれば「x-消去」。まとめて「α-消去」と言う。

「あるふぁしょうきょ」。

うん。その具体的な方法なんだけど、今回もやはり式の内側から処理していく。

まず最初に最初の“y”の部分について考える。

y = □ yと置くと、□はなにになるかな?

……うーんと、これってもしかしてさっきのI?

そう。だからTは次のように変形できる。

次に、右側の“x”の部分について考える。

この場合は□はどうなるかな?

うーんと、……yからxを作るのって、できるの?

□の部分は1つのコンビネータとは限らなくて、複雑な式でもいい。その中にxが含まれていてもいいよ。

yはいらないけどどうするの?

要らないものを捨てたいときにはKを使うといい。

Kを使う……。つまり、K x y = xだから、□はK x?

そう。だからTはさらに次のように変形できる。

さて、今までのをまとめると、次のようになる。

ここで、2つ目の規則はさらに一般化して次のように書ける。

ここでXはただの変数だけでなく、複雑な式でいい。この一般化はしなくてもいいけど、した方が消去後の式が小さくなる。

さて、λ計算の式はλと変数と関数適用でできていた。λは最初のλリフティングで消えていて、変数の場合は今見た規則でα-消去できる。あとは関数適用の場合だ。

こういう風におくと、□はなにになるだろうか。

うーんと、いままでS使ってなかったからS使う?

そう。

じゃあ、S f g y = (f y) (g y)だったから……、□はS I (K x)でいいのかな?

そう。完璧。

えへへ。

するとTは次のように変形できる。

これでyを消去できた。関数適用のy-消去は一般的には次のような規則になる。

これでひととおりα-消去ができるようになった。

ええと、まとめるとこうかな?

そう。さらに最適化として次の規則を加えてもよい。

元々y-消去した形になってるからだね。

これでλ計算の全ての式がSとKだけで表せるようになった。

2つだけで表わせるなんてなんか不思議だね。

実は1つだけでも表せる。

えっ、ほんと?

うん。だけど今日は長くなったからまたこんどね。