ラムダ計算を理解したようです
ラムダ計算に魅了されたあやぴーが、ラムダ計算でプログラミングしてみる。
今回の目標は「1+2=3」をラムダ計算で計算することです。
準備:ラムダ計算とは？
「函数の函数による函数のための計算」とか言ってると、「ぽい」のかもしれないです。
1930年頃にアロンゾ・チャーチさんが考案した、すっごい単純なプログラミング言語だと思っていればとりあえずいいと思います。(本気で知りたい人は自分で調べましょー)
ラムダ計算ではリダクションと呼ばれる式の変形によって計算します。
チャーチの数詞
「1+2=3」を計算するには、まず「数」が必要なのでチャーチの数詞を使います。
一般的にチャーチ数と言われる定義は、函数によって「数」を表すものです。
0 = identity 1 = f 2 = f f 3 = f f f …
それを実際の函数の式に表すとこんな感じ。
0 = λf.λx.x 1 = λf.λx.f x 2 = λf.λx.f (f x) 3 = λf.λx.f (f (f x)) …
チャーチ数における「後続数」
足し算はm,nの2つの数があるとき、「ある数nのm個あとの後続数」だと表現できそうです。
そうするとチャーチ数で、ある数nの「後続数」を返却する函数が必要そうだと気付きます。
例えばλf.λx.xの後続数はλf.λx.f xです。λf.λx.f xの後続数はλf.λx.f (f x)です。
なんだか、ある数nを引数に渡して、fがひとつ増えればいいような気がしてきます。
ということで、SUCC*1という名前の函数を書いてみます。
SUCC = λn.λf.λx.f n
これに1に相当するλf.λx.f xを入れてλf.λx.f (f x)が返れば成功です。
(SUCC λf.λx.(f x)) (λn.λf.λx.(f n) λf.λx.(f x)) ;;束縛変数が重複したのでλf.λx.f x=>λa.λb.a bとα変換してます λf.λx.(f (λa.λb.a b))
あれ…コレ以上どうしようもなくなりました。でももう少しな気がします。
ここでα変換したλa.λb.a bを数ではなく、ひとつの函数*2として捉えると、どうやったら(f x)になるのかが見えてきます。
(λa.λb.(a b) f x) ;;=> (f x)
ということはSUCCの定義を書きなおして、以下のように書けます。
SUCC = λn.λf.λx.f (n f x)
もう1度試してみます。
(SUCC λf.λx.(f x)) (λn.λf.λx.(f (n f x)) λf.λx.(f x)) λf.λx.(f (λa.λb.(a b) f x)) λf.λx.f (f x)
これで良さそうですね。
「1+2=3」をやってみる
さっき僕は
足し算はm,nの2つの数があるとき、「ある数nのm個あとの後続数」だと表現できそうです。
と書きました。
すると足し算する函数PLUSはこう書けそうです。
PLUS = λm.λn.m SUCC n
実際にやってみます。
((PLUS λf.λx.(f x)) λf.λx.(f (f x))) ((λm.λn.(m SUCC n) λf.λx.(f x)) λf.λx.(f (f x))) ;;α変換してλf.λx.(f x)=>λa.λb.(a b) ((λn.(λa.λb.(a b) SUCC n)) λf.λx.(f (f x))) ((λn.(λb.(SUCC b) n)) λf.λx.(f (f x))) (λn.(SUCC n) λf.λx.(f (f x))) (SUCC λf.λx.(f (f x))) λf.λx.f (f (f x))
はい。ということで、「1+2=3」ができました！
ラムダ計算素敵ですね！
おまけ
Schemeだとこう書けます。
(define zero (lambda (f) (lambda (x) x))) (define one (lambda (f) (lambda (x) (f x)))) (define two (lambda (f) (lambda (x) (f (f x))))) (define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x)))))) (define plus (lambda (m) (lambda (n) ((m succ) n)))) ((plus one) two)
