ワニと卵のパズルは作者から公開の快諾をもらった。でも訳語とかの不備はあくまでもわたしの責任で、もう少し調整したいとは思っている(責任といえば、「責任」というのも小学校5年生の漢字だそうだ。別の単語にかえた方がいいかなー)。
さて、今回はこの「ワニのラムダ計算」から、ひとつのことを説明したい。
まんなかくらいにある「食事のルール」と「色のルール」は読んだだろうか。これは、実はラムダ計算の基本中の基本なのだけれど、これをよく見てほしい。下の方にある略記法を使って書くと、最終結果までの過程はこう書ける。
M-----< G---< Y-< O-----< R---< Y M M O G R O-------------< Y-< G---< G---< O Y R---< R---< G R G R G---< G---< Y-< R---< R---< Y G R G R R-------< Y-< C---< R Y B---< C B C---< Y-< B---< Y C B B----< Y-< B Y B-< B
じっくり見ていけばわかるだろう。
ところで、「左上」という原則があったが、これをすこし変えるとどうなるだろうか。たとえば、「右上」にするのだ。一番上で、一番右のワニが食べる。こんな風になる。
M-----< R-----< O-----< Y-< R M M O Y O-----------------< R-----< R-----< O Y-< R Y-< R Y Y O-------------< R-----< Y-< O Y-< R Y Y O---------< R-----< O Y-< R Y O-----< Y-< O Y O-< O
(最初のステップは省略した)。また、「左下」はどうだろうか。
O-------------< Y-< G---< G---< O Y R---< R---< G R G R O-----------< Y-< R-------< O Y C---< R B---< C B O---------< Y-< R-----< O Y B---< R B O-----< Y-< B---< Y O B B-----< Y-< B Y B-< B
さらに「右下」。
M-----< G---< Y-< O-----< R---< Y M M O G R M-----< R-----< O-----< Y-< R M M O Y M-----< R-< O-----< R M M O O---------< R-< R-< O R R O-----< R-< O R O-< O
……とまあ、長々と書いてきたが、見てほしいのは最終形。これはみんな同じかたちをしている(色はちがうけど、色は好きなように変わっちゃうということに注意)。
ここでは一定のルールに則ったものだったが、途中でルールを変えたり、気紛れに好きなところから食事をしてもじつは変わらない。実際には、どんな風に、どんな順番にやっても必ず同じものに収束するということが知られている。これをチャーチ・ロッサー性、略してCR性という。
ただし条件がある。ある種のパターンをつくると無限ループを作れるのだ。そのような無限ループに陥ると、いつまでも「食事」がつづいて終わらない。正確にいうと、「それ以上、食事=展開ができないようなパターンとなるなら、そのパターンはおなじ」という主張である。
そもそも、このワニはラムダ計算に対応していて、ラムダ計算はテューリング機械に対応しているのだった。「収束する」というのは、いってみれば「計算が終了する」というのと対応する考え方だ。だから「あるプログラム(と入力)があれば、その計算結果はどういう経路をたどっても等しい」というのは、ある意味で当然のことだと言える。それをきちんと調べたのがCR性というものだ。ちなみに、テューリング等価ということは「収束するかどうか」ということを事前には調べられないということを意味する(停止性問題ね)。
さて「ワニの家族」はラムダ計算におけるラムダ抽象に対応していて、ラムダ抽象は関数に対応していると考えられる。っていうのはようするに、
R-< R
というのは、たとえば JavaScript なら、
function(R) { return R; }
に対応するとかいった風な感じだ(ワニが2つ重なるとちょっと話がややこしくなるけど)。
で、どの順番で食事ルールを適用していくか、っていうのはおおざっぱに言うと「引数をどの順番で計算していくか」という問題などに対応しているのだね。で、CR性から、次のことが言える。
「関数に渡された引数は、どの順序で計算されても(計算が終了するなら)結果は変わらない」
ほんとうかな？ 大部分の言語では、これは本当じゃない(そうならない理由はいくつかあるが)。でも、 Haskell ではこれが成立する。そして実は、 Haskell という言語における特徴的な部分は、この特徴を成立させるためだけに存在しているといっていい。ラムダ計算というモデルをある程度知っていると、 Haskell のプログラミングは(型つき)ラムダ計算をやってるような感覚で書けるようになる。それが、 Haskell の言語仕様の特徴的なところだし、面白いところだと思っている。
えーと話が逸れた。そういうわけでCR性でした。