SKIコンビネータについて簡潔にまとまったサイトがみつからなかったので要点だけまとめました。1
ラムダ計算式とは
関数f(x)=x+2をラムダ計算では λx.x+2 と表す。λx.xならf(x)=x、つまり入力値をそのまま返す関数となる。
xy のように２つ並べられている時はxにyを引数として適用することを意味する。λx.((xy)z) は単に λx.xyzと書ける。各関数は左結合であり順序が明確な時はこのようにカッコを省略することができる。
λxy.x のように左辺に２つ並べたら、xとyの２つの引数をとる関数を意味する。この場合はyの値を無視してxをそのまま帰す関数f(x,y)=xとなる。
λx.xy にある２つの変数 x yのうち、パラメータとして使われる変数(この場合はx)を束縛変数(bound variable)、それ以外は自由変数(free variable)という。
λリフティング
ラムダ式の中のλを取り除きコンビネータで置き換える。例として下記の式の場合を考える。
Y = λf.(λx.f(λv.(xx)v))(λx.f(λv.(xx)v))
まず一番内側のカッコ内にあるλの箇所、λv.(xx)vを対象とする。コンビネータを仮にMと置く。Mのパラメータは自由変数を先に書き、後ろに束縛変数を書く。右辺は元の式のままでMxv=(xx)vとなる。
これを最初の式のλv.(xx)vと置き換える。この時、束縛変数は置く必要がない。2
Y = λf.(λx.f(Mx))(λx.f(Mx))
次に(λx.f(Mx))を置き換える。コンビネータ L と置いて Lfx = f(Mx)。これを元の式に適用する。xは束縛変数なので消去されて下記のようになる。
Y = λf.(Lf)(Lf)
最後にこの式のλをとる。Yには束縛変数fしかないのでYf = (Lf)(Lf)となる。以上をまとめると元のラムダ式をλリフティングした結果は下記のようになる。
Yf = (Lf)(Lf)
Lfx = f(Mx)
Mxv = (xx)v
SKIコンビネータ
S K I ３つのコンビネータを下記のように定義するとすべてのラムダ式をこれらだけで表すことができる。3
Sfgx = (fx)(gx)
Kxy = x
Ix = x
Iは入力値をそのまま返すだけのコンビネータ。Kは(x y)の２つのパラメータをとるがyを無視してxを返す。
α-消去
T x y = y xというコンビネータTがあるとする。これはパラメータ x y の適用順を逆にして y x を返す。これは下記のように変形できる。
Txy = yx ... Iy=yなので
= (Iy)x ... Kxy=xなので
= (Iy)(Kxy) ... Sfgxのf=I,g=Kx,x=yとおくと（Iy)(Kxy)は(fx)(gx)の形式なので
= SI(Kx)y
∴Tx = SI(Kx) ... y消去完了
Tx = SI(Kx) ... Kxy=xよりK(SI)x=(SI)となるので
= (K(SI)x)(Kx) ... Sfgxのf=K(SI),g=K,x=xとおいて
= S(K(SI))Kx
∴T = S(K(SI))K ... x消去完了
このようにしてパラメータを消去していくことをα-消去という4。これでTをSKIで表現することができた。
オンラインでSKIコンビネータを解釈してくれるサービスに投げると動作を確認できる。
http://ski.aditsu.net/
先程のS(K(SI))Kを入れるRunを押すと(x0->(x1->x1(x0)))となるのでたしかに引数を
x0,x1の順番に取得したのに｀x1,x0`の順番で合成していることがわかる。
参考サイト
- 高階ことりちゃんと学ぶSKIコンビネータ
- http://www.tatapa.org/~takuo/kotori_ski/index.html
- きっかけはここだったのですが、ラムダ書式の説明が足りないのとTxy = yxのy消去だけでx消去がなかったので自力で説いてみました。
- Wikipedia ラムダ計算 https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
- Wikipedia SKIコンビネータ計算 https://ja.wikipedia.org/wiki/SKI%E3%82%B3%E3%83%B3%E3%83%93%E3%83%8D%E3%83%BC%E3%82%BF%E8%A8%88%E7%AE%97