λのおわりに

English version

先日，広告でこんなものを見た．この広告は「投資の専門家に: 一番簡単なことから始めよう」というもので，多分，1+1 = 2 というのが一番簡単だと言うのであろう．私は 1 + 1 が 2 であることを機械に教えるにはどうすれば良いかということを 8ヶ月かかって説明してきた．(ところでこの広告は煙草の広告である)




人間ならば，確かにこれは簡単かもしれない．しかし，機械にそれを教えるとなると，1+1 とは何かということを追求する必要がある．1+1 の前に，数とは何かということを考え，それをチャーチ数で表現した．パラノイアかもしれないが，あたりまえのことというものは，簡単だからあたりまえなのではなく，単にいつも身近にあるからあたりまえなだけだと思う．簡単なことではない．家族や恋人と一緒に時間をすごすことをあたりまえに感じてしまっている人もいるかもしれない．しかし，それは単にそうすることに慣れているからであって，簡単だからではないと思う．時々，あたりまえのことをふりかえって見ることも大切だと思う．

これでλ計算のためのヒッチハイカーズガイドというテーマのブログはとりあえず幕とする．

Wikipedia にはλ計算でチャーチ数を SUCC や PLUS に適用するとそれが正しいとわかる．と書いてあるが，私には一週間もわからなかった．友人らの助けを借りてやっとわかったので，どうやるのかということを書いておこうと考えて始めたのがこの短編である．

ここではλ計算とは何か，どうしてそういうものを考えたのか，そして具体的に簡単なものを適用する方法を述べてきた．この短編が私と同じ所でつまづいている人の助けになれば幸いである．

しかし，λ計算はまだまだ奥が深い．これでは入門の扉を開いたという程度である。私には combinator がまだ理解できていない．いつかわかったらそれについて書いてみたい．書くことによって学ぶことができるのは良かった．あるいは教えることは学ぶことであるとつくづくおもった．本当に興味のあるものでないと続けるのは難しいということも学んだことであった．

この小文は λ計算を informal な方法ではあるが，感じをつかむことを重点に置いて書いた．ここでは λ式を構成的に示すこともしなかったし，α-conversion, β-conversion, η-conversion などの基礎的な変換方法も詳しくは述べなかった．さらに詳しく知りたい人はWikipedia が良い入門となることと思う．

謝辞

この blog を書くきっかけをつくってくれた内田さん，計算の具体例を理解する手助けをして下さった Hoedicke さんと Rehders さん，そして今回書くことができなかったが，実装のヒントを与えてくれた前田さんに感謝します．他にも助言や感想を下さった皆さまにお礼を申し上げます．また，この blog を読んで欲しかったが，残念ながら永遠に不可能になってしまった楯岡さんにこの blog を捧げます．

Sub

English version

それぞれの具体例は実際にやってみたいと思わないとあまり面白くないかもしれない．計算がどのように進むのかは確かめないと式の羅列でしかないからだ．

PRED を使って引き算を定義する．

SUB := λ m n. n PRED m

SUB 3 2 = (λ m n. n PRED m) (λ f x. f (f (f x))) (λ f x. f (f x))
= (λ n. n PRED (λ f x. f (f (f x)))) (λ f x. f (f x))

= (λ f x. f (f x)) PRED (λ f x. f (f (f x)))

= (λ x. PRED (PRED x)) (λ f x. f (f (f x)))

PRED が二番目の引数分(= 2)コピーされた．これがトリックである．引く数が10 ならば，PRED が 10 個コピーされる．

= PRED (PRED (λ f x. f (f (f x))))

つまり，これは，PRED (PRED 3) であるので，

= PRED 2

= 1

つまり 3 - 2 は 1 である．引き算も可能だった．

PRED

English version

引き算をしたいのだが，これまでに作った Church数では負の数がない．これはfの数で数を示していたためだ．簡単のためにここでは負の数を考えないことにするが，より詳しいことは Wikipedia を参照して欲しい．

まず，準備として PRED (predecessor) を考える．これは一つ前の数の意味である．しかしここでは 0 の前は考えないものとする．


PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)


PRED 2 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. f (f x))

= (λ f x. (λ f x. f (f x)) (λ g h. h (g f)) (λ u. x) (λ u. u))

= (λ f x. (λ x. (λ g h. h (g f)) ((λ g h. h (g f)) x)) (λ u. x) (λ u. u))


= (λ f x. (λ x. (λ g h. h (g f)) (λ h. h (x f))) (λ u. x) (λ u. u))

= (λ f x. (λ g h. h (g f)) (λ h. h ( (λ u. x) f)) (λ u. u))

= (λ f x. (λ h. h ((λ h. h ( (λ u. x) f)) f)) (λ u. u))

ここで一つ f が消える．

= (λ f x. (λ h. h ((λ h. h x) f)) (λ u. u))

= (λ f x. (λ h. h ((f x))) (λ u. u))

= (λ f x. ((λ u. u) ((f x))) )

= (λ f x. (f x))

= (λ f x. f x)

= 1


ちなみに 0 を入れてみるとどうなるだろうか．


PRED 0 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. x)
= (λ f x. (λ f x. x) (λ g h. h (g f)) (λ u. x) (λ u. u))

= (λ f x. (λ x. x) (λ u. x) (λ u. u))

= (λ f x. (λ u. x) (λ u. u))

= (λ f x. x)

0 になってしまった．これは良い性質とも言える．PRED は入力が 0 の時は 0 を返し，それ以外は一つ前の数を返す函数である．

ここで面白いと思うのはチャーチ数そのものがプログラムの一部を成している所である．もちろんここでのチャーチ数は函数であるから自然と言えば自然である．


λ n . n (λ g h. h (g f)) は 0 を入れると，

(λ n . n (λ g h. h (g f))) (λ f x . x)
= (λ f x . x) (λ g h. h (g f))
= (λ x . x)

0 が出力される．PRED では他の項があるので，これ以上は詮索しないが，0 が出力されると，最初の項が無視されることに注意しよう．これはチャーチ数の 0 では f が bind されていないからである．