あっ！野生の型がタイプしてる！！ｶﾀｶﾀｶﾀｶﾀ...
前提知識無しでも読めるし、ラムダ式を知ってるなら楽に読めると思いますが、SKIコンビネータを理解してしまう恐れがあるので、覚悟しておいてください！（覚悟しなくても大丈夫です）
ラムダ式
ラムダ式はオートマトンなどの計算モデルの一つ。無名関数の表現としてよく使われる。"λ"(ギリシャ文字ラムダ)の後ろに引数を書いて、"."の後に関数の内容を書く。関数は左結合で、引数を取る変数を束縛変数、それ以外を自由変数と呼ぶ。束縛変数に値を代入する操作を関数適用という。
-- 束縛変数がx
λx. x + 2
-- 関数適用
(λx. x + 2) 3 = 3 + 2 = 5
-- 束縛変数がx,y 自由変数がC
-- 引数は繋げることができる
λx. (λy. x + y + C) = λx y. x + y + C
-- 関数適用
(λx y. x + y + C) 2 3 = 2 + 3 + C
= 5 + C
-- 左結合である
f x y = (f x) y
ラムダ計算
ラムダ計算は以下の3種類の簡約、変換によりラムダ式を評価、適用することを言います。
α-変換 : 束縛変数の名前は重要ではない
β-簡約 : 関数適用
η-変換 : 2つの関数に対し、任意の引数をとったものが等しいならば、それらの関数は等しい
-- 具体例
-- α-変換
λx. x = λy. y
-- β-簡約
(λx. f x) y = f y
-- η-変換
f = λx. f x
ラムダ計算はチューリング完全である。そのことを体感する為にラムダ式で自然数、真偽値、データ構造を作って遊びます。これらをChurch数といいます。
自然数はペアノ算術と同様に定義できます。
-- 自然数 関数で適用される回数と対応させている
0 := λf x. x
1 := λf x. f x
2 := λf x. f(f x)
3 := λf x. f(f(f x))
...
練習問題
次の関数をラムダ式と自然数を用いて実装してみよう！
★
Succ:ある数の次の自然数を返す関数を見つけ出しなさい。
解答例
一番前にfを付け足してあげる。
Succ := λa f x. f(a f x)
-- 具体例
Succ 2 = (λa f x. f(a f x)) 2
= λf x. f(2 f x)
= λf x. f(f(f x))
= 3
★★
Add:2つの自然数の和を返す関数を見つけ出しなさい。
解答例
そのまま後ろに繋げるようにしてあげる。
Add := λa b f x. a f (b f x)
-- 具体例
Add 2 3 = (λa b f x. a f(b f x)) 2 3
= λf x. 2 f (f(f(f x)))
= λf x. f(f (f(f(f x))))
= 5
★★★
Mul 2つの自然数の積を返す関数を見つけ出しなさい。
解答例
Mul := λa b f x. a (b f) x
-- 具体例
Mul 2 3 = (λa b f x. a (b f) x) 2 3
= λf x. 2 (3 f) x
= λf x. (λf' x'. f'(f' x')) (λx''. f(f(f x''))) x
= λf x. f(f(f(f(f(f x)))))
= 6
★★★★
Pow 2つの自然数e, aをとって$e^a$を返す関数を見つけ出しなさい。
解答例
Pow := λe a. a e
-- 具体例
Pow 2 3 = (λe a. a e) 2 3
= 3 2
= λx. 2(2(2 x))
= λx. λf'y. f'(f' y) 2(2 x)
= λx y. 2(2 x)(2(2 x) y)
= λx y. λz. 2 x(2 x z) (2(2 x) y)
= λx y. 2 x (2 x (2(2 x) y))
= λx y. 2 x (2 x (2 x (2 x y)))
= λx y. 2 x (2 x (2 x (x(x y))))
= λx y. 2 x (2 x (x(x(x(x y)))))
= λx y. 2 x (x(x(x(x(x(x y))))))
= λx y. x(x(x(x(x(x(x(x y)))))))
= 8
★★★★★
Pred 一つ前の自然数を返す関数を見つけ出しなさい。
解答例
Pred := λn f x. n (λg h. h(g f)) (λu.x) (λu.u)
-- 具体例
Pred 3 = (λn f x. n (λg h. h(g f)) (λu.x) (λu.u)) 3
= λf x. 3 (λg h. h(g f)) (λu.x) (λu.u)
= λf x. (λg h. h(g f)) ((λg h. h(g f)) ((λg h. h(g f)) (λu.x))) (λu.u)
= λf x. (λg h. h(g f)) ((λg h. h(g f)) (λh. h x)) (λu.u)
= λf x. (λg h. h(g f)) (λh. h(f x)) (λu.u)
= λf x. (λh. h(f(f x))) (λu.u)
= λf x. f(f x)
= 2
真偽値やデータ構造もラムダ式で表現できる。
-- bool (False = 0)
True := λx y. x
False := λx y. y
-- Not
Not := λp. p False True
-- And
And := λp q. p q False
-- Or
Or := λp q. p True q
-- If
If := λp x y. p x y
-- IsZero
IsZero := λn. n (λx. False) True
-- list
Cons := λs b f. f s b
Car := λx y. x = True
Cdr := λx y. y = False
-- 具体例
Cons (Cons a b) c Car Car = Car (Cons a b) c Car
= (Cons a b) Car
= a
さて、条件分岐も使えるようになったし、今度は繰り返し処理でもやってみましょう。
繰り返し処理は再帰呼び出しで実現でき、再帰は不動点コンビネータを使うことで簡単に実装できます。不動点コンビネータには様々な関数があり、よく使われる不動点コンビネータはYコンビネータで、次のように定義されます。
-- 不動点コンビネータ
Fix f := f (Fix f)
= f (f (Fix f))
= f (f (f (Fix f)))
= ...
-- Yコンビネータ
Y := (λf. (λx. f(x x)) (λx. f(x x)))
Y g := (λf. (λx. f(x x)) (λx. f(x x))) g
= (λx. g(x x)) (λx. g(x x))
= g ((λx. g(x x)) (λx. g(x x)))
= g (Y g)
階乗をラムダ式で表現してみよう！
\begin{align}
Fac(0) &= 1\\
Fac(n) &= n \times Fac(n-1)
\end{align}
階乗の定義は上の通りであるから
-- ラムダ式ver.
G = λf x. If (IsZero x) 1 (Mul x (f (f (Pred x))))
(λf x.f f x) G
(λf x.f f x) G 3 = G G 3
= If (IsZero 3) 1 (Mul 3 (G (G (Pred 3))))
= Mul 3 (G G 2)
= Mul 3 (Mul 2 (G G 1))
= Mul 3 (Mul 2 (Mul 1 (G G 0)))
= Mul 3 (Mul 2 (Mul 1 (If (IsZero 0) 1 (Mul 0 (G (G (Pred 0)))))))
= Mul 3 (Mul 2 (Mul 1 1))
= 6
-- 不動点コンビネータver.
G' = λf x. If (IsZero x) 1 (Mul x (f (Pred x)))
Y G'
Y G' 3 = G'(Y G') 3
= If (IsZero 3) 1 (Mul 3 (Y G' (Pred 3)))
= Mul 3 (Y G' 2)
= Mul 3 (G' (Y G') 2)
= Mul 3 (Mul 2 (Y G' 1))
= Mul 3 (Mul 2 (Mul 1 (Y G' 0)))
= Mul 3 (Mul 2 (Mul 1 (If (IsZero 0) 1 (Mul 0 (Y G' (Pred 0))))))
= Mul 3 (Mul 2 (Mul 1 1))
= 6
どうでしょう、ラムダ式で様々なプログラムが書ける気になってきましたよね！
SKIコンビネータ
コンビネータとは高階関数のことである。先に述べたYコンビネータや次のようなものがある。
Ω x := x x
B x y z := x (y z)
C x y z := x z y
K x y := x
W x y := x y y
SKIコンビネータはSコンビネータ、Kコンビネータ、Iコンビネータから構成されるコンビネータの集合である。定義は次の通りである。
S := λf g x. f x(g x)
K := λx y. x
I := λx. x
S f g x = f x(g x)
K x y = x
I x = x
-- これも左結合なので演算順序は次のようになる
S f g x = ((S f) g) x
K x y = (K x) y
I x = I x
変数を使わずして、この3種類のコンビネータで関数を表します。
ん〜KはまだしもIなんて必要かな...？次の例を見てみよう。
S(K(SI))K x y = (K(SI)x)(K x)y
= SI(K x)y
= (I y)((K x)y)
= y x
なるほど。変数を使わない制約が効いてるわけだ。
練習問題
それぞれのコンビネータがSKIコンビネータでちゃんと表せられているか確認してみよう！
Ω x := x x
B x y z := x (y z)
C x y z := x z y
W x y := x y y
Ω := SII
B := S (K S) K
C := S(S(K(S(K S)K))S)(K K)
W := S S(S K)
Ωの解答
Ω x = SII x
= I x(I x)
= x x
Bの解答
B x y z = S (K S) K x y z
= K S x (K x) y z
= S (K x) y z
= K x z (y z)
= x (y z)
Cの解答
C x y z = S(S(K(S(K S)K))S)(K K) x y z
= (S(K(S(K S)K))S x)(K K x) y z
= (K(S(K S)K) x)(S x)K y z
= (S(K S)K (S x))K y z
= (K S (S x))(K (S x))K y z
= S(K (S x))K y z
= (K (S x) y)(K y) z
= S x (K y) z
= x z y
Wの解答
W x y = S S(S K) x y
= (S x)(S K x) y
= (x y)(S K x y)
= x y (K y) x y
= x y y y
Church数もSKIコンビネータで表せられる。自然数は後のお楽しみとして、真偽値とデータ構造を紹介する。
-- bool
True = K
False = K I
Not = S(SI(K(KI)))(KK)
And = SS(K(K(KI)))
Or = SI(KK)
If = I
-- list
Cons = S(S(KS)(S(KK)(S(KS))(S(K(SI))K))))(KK)
Car = SI(KK)
Cdr = SI(K(KI))
ラムダ式とSKIコンビネータの相互変換
SKIコンビネータからラムダ式への変換は定義より自明であるが逆はどうであろうか？
予感はしているだろうが、驚くべきことに任意のラムダ式はSKIコンビネータで表す事ができる。
ラムダ式からSKIコンビネータへの変換はいくつか方法がある。ここでは次の2つを紹介する。
- Abstraction Elimination
- λリフティング/α-消去
Abstraction Elimination
次の規則を用いて簡約化していく。これら全て、η-変換より同値である事が確かめられる。
-- Abstraction Elimination
1. T[x] => x
2. T[(E₁ E₂)] => (T[E₁] T[E₂])
3. T[λx.E] => (K T[E]) -- Eがxに依存しないとき
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]]
6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
7. T[λx.(E x)] => T[E] -- Eがxに依存しないとき
定義をみれば分かる通り、任意のラムダ式をSKIコンビネータに表せられる事が分かる。
次のラムダ式をSKIコンビネータに変換してみる。気持ちとしては、最初5を使い、基本6を使って、1,3,4,7で簡約を終了させていく。
-- 順序交換 Wiki(コンビネータ論理)より
T[λx.λy.(y x)] = T[λx.T[λy.(y x)]] -- by 5
= T[λx.(S T[λy.y] T[λy.x])] -- by 6
= T[λx.(S I T[λy.x])] -- by 4
= T[λx.(S I (K x))] -- by 3 and 1
= (S T[λx.(S I)] T[λx.(K x)]) -- by 6
= (S (K (S I)) T[λx.(K x)]) -- by 3
= S (K (S I)) K -- by 7
また、次のような簡約規則を使うことで簡約できることがある。
-- SKIコンビネータ簡約規則 (η-変換により容易に示せる)
-- Xは任意のコンビネータが入るとする。
I I = I
S K X = I
S B (K I) = I
S K (K I) = I
K K I = K
S K S K = K
K K (S K) = K
S (K X) I = X
S (K S) K = B
S X X = S (K(SII)) X
自然数やYコンビネータについてもAbstraction Eliminationを行ってみる。
-- 自然数
T[0] = T[λf x. x]
= K T[x. x]
= K I
T[1] = T[λf x. f x]
= T[λf. T[λx. f x]]
= T[λf. f]
= I
T[2] = T[λf x. f(f x)]
= T[λf. T[λx. f(f x)]]
= T[λf. (S T[λx. f] T[λx. f x])]
= T[λf. (S (K f) f)]
= S (S T[λf. S] T[λf. K f]) T[λf. f]
= S (S (K S) K) I
= S B I
T[3] = T[λf x. f(f(f x))]
= T[λf. T[λx. f(f(f x))]]
= T[λf. S T[λx. f] (S T[λx. f] T[λx. f x])]
= T[λf. S (K f) (S (K f) f)]
= S (S T[λf. S] T[λf. K f]) (S (S T[λf. S] T[λf. K f]) T[λf. f]))
= S (S (K S) K) (S (S (K S) K) I)
= S B (S B I)
-- Yコンビネータ
T[Y] := T[λf. (λx. f(x x)) (λx. f(x x))]
= T[λf. T[(λx. f(x x)) (λx. f(x x))]]
= T[λf. T[λx. f(x x)] T[λx. f(x x)]]
= T[λf. (S T[λx. f] (S T[λx. x] T[λx. x])) (S T[λx. f] (S T[λx. x] T[λx. x]))]
= T[λf. (S (K f) (SII)) (S (K f) (SII))]
= S T[λf. (S (K f) (SII))] T[λf. (S (K f) (SII))]
= S (K(SII)) T[λf. (S (K f) (SII))]
= S (K(SII)) (S (S T[λx. S] T[λx. K f]) T[λx. SII]))
= S (K(SII)) (S (S (K S) K) (K(SII)))
-- 確認
Y := S(K(SII))(S(S(KS)K)(K(SII)))
Y f = S (K(SII)) (S(S(KS)K)(K(SII))) f
= K (SII) f (S(S(KS)K)(K(SII) f)
= SII (S(S(KS)K)(K(SII)) f)
= S (S(KS)K) (K(SII)) f (S(S(KS)K)(K(SII)) f)
= S(KS)K f (K(SII)f) (S(S(KS)K)(K(SII)) f)
= K S f (K f) (K(SII)f) (S(S(KS)K)(K(SII)) f)
= S (K f) (K(SII)f) (S(S(KS)K)(K(SII)) f)
= K f (S(S(KS)K)(K(SII)) f) (K(SII)f (S(S(KS)K)(K(SII)) f))
= f (K(SII) f (S(S(KS)K)(K(SII)) f))
= f (S (K(SII)) (S(S(KS)K)(K(SII))) f)
= f (Y f)
つまりこのようになる。
-- 順序交換
λx.λy.(y x) = S (K (S I)) K
-- 自然数 B=S(KS)K
0 = KI
1 = I
2 = SBI
3 = SB(SBI)
4 = SB(SB(SBI))
...
-- Yコンビネータ
Y = S(K(SII)(S(S(KS)K)(K(SII)))
練習問題
SuccをAbstraction EliminationでSKIコンビネータに変換してみよう！
Succ := λa f x. f(a f x)
解答例
自然数の形をみてもらえれば分かる通り、SuccはSBと予想できます。実際にそうなったかな...？
T[Succ] = T[λa f x. f(a f x)]
= T[λa. T[λf. T[λx. f(a f x)]]]
= T[λa. T[λf. S T[λx. f] T[λx. (a f) x]]]
= T[λa. T[λf. S (K f) (a f)]]
= T[λa. S (S T[λf. S] T[λf. K f]) T[λf. a f]]
= T[λa. S (S (K S) K) a]
= S (S (K S) K)
= SB
また自然数の演算は次のようになる。
Add = S(KS)(S(K(S(KS)))(S(KK)))
Mul = S(KS)K
Pow = S(K(SI))K
-- 具体例 これである程度の自然数についてはかなり簡約ができる。
256 = Pow 4 4 = S(K(SI))K(SB(SB(SBI)))(SB(SB(SBI)))
λリフティング/α-消去
λリフティングとはコンビネータを使い、自由変数を引数に引き込んでいく操作、α-消去とは作ったコンビネータをSKIコンビネータに変換しつつ変数を消去する操作である。パズル感覚で楽しい方法である。
-- Zコンビネータ(Yコンビネータをη-変換したコンビネータ)のλリフティング
Z := λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
= λf. (λx. f (M x)) (λx. f (M x)) -- M x y = (x x) y
= λf. (L f x) (L f x) -- L f x = f (M x)
--結果
Z f x = (L f x) (L f x)
L f x = f (M x)
M x y = (x x) y
-- α-消去 コンビネータの最後の引数の変数を一番右に1つだけ持ってくるようにしたい
-- Mのα-消去
M x y = (x x) y
M x = (x x) -- y-消去
= SII x
M = SII -- x-消去
-- Lのα-消去 たのしい
L f x = f (M x)
= S (K f) M x
L f = S (K f) M
= (S (K S) K f) M
= S (S (K S) K) (K M) f
L = S (S (K S) K) (K M)
= S (S (K S) K) (K (SII))
-- Zのα-消去
Z f x = (L f x) (L f x)
= S (L f) (L f) x
Z f = S (L f) (L f)
= S (K S) L f (L f)
= S (S (K S) L) L f
Z = S (S (K S) L) L
= S (S (K S) (S (S (K S) K) (K (SII)) )) (S (S (K S) K) (K (SII)))
ラムダ式の世界をもっと探ってみよう
どうでしょう、SKIYAKIを計算したくなってきましたか？もっとラムダ式と戯れたいと思ったのなら、SKIコンビネータを元に作られた言語、Lazy Kを触ってみましょう！
Lazy Kの処理系
C++で実装されたThe Lazy K Programming Languageのコンパイラが下の方に載せられている。付属のSchemeファイルも良くて、Schemeをunlambda/iota/jotのマクロとしてみれるものがアツい。
Lazy K
4種類の書き方が存在します。Yコンビネータを例にしています.
- SKIコンビネータ計算
S(K(SII))(S(S(KS)K)(K(SII)))
- unlambda記法
関数適用についてf(x)を`fxと書くことで字数が短縮された。
``s`k``sii``s``s`ksk`k``sii
次のように関数ι(ギリシャ文字イオタ)を定義するとiotaと関数適用のみを使ってチューリング完全となる。
\begin{align}
ι &:= λf. (f S) K\\
I &= ιι\\
K &= ι(ι(ιι))\\
S &= ι(ι(ι(ιι)))
\end{align}
関数ιをiと書き、関数適用を*と書く。
***i*i*i*ii**i*i*ii***i*i*i*ii*ii*ii***i*i*i*ii***i*i*i*ii**i*i*ii*i*i*i*ii*i*i*ii**i*i*ii***i*i*i*ii*ii*ii
0と1でチューリング完全となる言語。iotaではsyntax errorがあるが、jotでは任意のコードが実行できるのが魅力。
\begin{align}
[] &= I\\
[F0] &= [F]SK\\
[F1] &= λx.λy.[F](xy) = S(K[F])\\
S &= [11111000]\\
K &= [11100]\\
I &= []
\end{align}
11111111100000
参考文献
だいたいWikiを読みめばいい感じ。
Wiki
ラムダ計算 / Lambda calculus
コンビネータ論理 / Combinatory logic
不動点コンビネータ / Fixed-point combinator
SKIコンビネータ / SKI combinator calculus
Church encoding
Church数を改良した51b数について
高機能なラムダ計算処理系
Lazy K処理系
Lazy K入門