ぼくもYコンビネータがわかるようになるまではそうだったのだけど、Yコンビネータを使うとどのような処理ができるのかがよくわからなくて悩んでいる人が多いように思う。他の人のブログを見ても、名前をつけずに再帰ができるのがすばらしいとか書いてあったりするのだけど、それによってどういう処理ができるのかわからずにいた。
結論をいえばYコンビネータには、なにかの処理を便利にする能力はない。関数であらゆる計算ができるということが示せれば、あとは用なしだ。理論の礎としてうまってしまえばいい。
結局、Yコンビネータによってどのような処理ができるかというのは、ラムダ計算の要素のメリットをチューリングマシンの中に見出そうとしてるといえる。
ラムダ計算とチューリングマシンは、どちらも計算モデルという点では一致しているけど、全く違う。
無限であるか有限かの違いといってもいい。
チューリングマシンでは、データの量と処理に対して計算の時間が変わる。そのため、データの量によってどのくらい時間がかかるかということを検証するのに使われる。
一方、ラムダ計算では、計算が終わるか終わらないかのどちらかしかない。計算が終わるのだとしたら、式の存在に気付いた瞬間に計算は終わっている。ただ、計算が終わるということに気付くのは難しいかもしれない。
例えば、ぼくはラムダで引き算をやるときに、Yコンビネータを使ったループで、与えた一歩手前まで計算を繰り返すことによって数値を1減らしてた。
pred = Y(λg.λn.λm.eq m (succ n)(n)(g (succ n)) m)(0)
けど、このとき、たとえ与えた数の大きさに比例するステップが必要になろうとも、ラムダ計算ではそれを気にしない。
つまり、このpredが常に与えた数値よりも1小さい値を返すことが示せれば
pred 100^100^100
などとやっても、これを書いた瞬間に
pred 100^100^100 = 100^100^100 - 1
と示せるわけだ。predのラムダ式を一ステップずつ簡約していく必要はない。
同様にYコンビネータも、そのYが不動点演算子であることが示せれば、あとはその内容はどうでもいい。
このようなチューリングマシンとの性質の違いがあるので、ラムダ式を使って考えると計算が速く終わるようになるということはない。λ計算は、計算の時間には関与しない。
では、いったい、ラムダ計算になにができて、何の役にたつのか。
そのことを示すのに、チューリングマシンになにができないのかを考えてみる。
チューリングマシンでは、ヘッドの位置のデータを読む・書く・ヘッドを動かす・状態を変えるという操作だけを行う。そして、テープをよみとり、手続きを行っていく。ここで、テープに何が書いてあろうが、チューリングマシンは黙々と仕事をこなす。
チューリングマシンでは、テープに書いてあるデータが妥当であるかどうかという判断を行うことはできない。もちろん、チューリングマシンによってデータが妥当かどうかを判定する処理を行うことはできるけど、チューリングマシン自身にデータ検証能力があるわけではない。間違ったデータを読み取ったとしても、正常に検証処理を行いそのデータが間違いであるという結果を正常に出力する。
つまり、チューリングマシンには、プログラムの妥当性が判断できない。
一方、ラムダ計算では、たとえばλx.x+yを書いてしまうと、yという変数が浮いたまま残ってしまうことがわかるし、λf.(λx.x+3)(λx.x*2)というラムダ式では最初のカッコのxとあとのカッコのxは別モノであることが示せる。
上のpred関数にtrueをあらわすラムダ式 λx.λy.xを渡すと、なんだか意味のない結果を返してしまうので、型付ラムダ計算といって、if関数はtrueかfalseしか受け取らないとか、その変数に割り当てることができる値の集合を指定することで、意味のない結果を出さないことを保証することもできる。集合を型として扱うわけだ。これを発展させていくと、計算が型という観点において妥当かどうか判断することができる。
つまり、今プログラムを書くときに、「プログラムの書き方」といって「スコープはせまく」とか「型あり言語は実行時エラーがでにくい」とかいう話をしてるのは、その背景にはラムダ計算があるわけだ。
ラムダ計算を基礎としてプログラムを考えていくことで、確実に動くプログラムを書くということを考えれるようになる。このようなことから、並列計算でのプログラム記述などに関数型言語が使われるようになっている。
並列計算では、プログラムを動かして検証するということは非常に難しい。ラムダ計算など、検証能力を持った計算モデルで、動かさなくても検証を行えるようにするわけだ。
プログラムは、いかに手続きを実行するかという命令的な側面と、いかに手続きを記述するかという宣言的な側面がある。チューリングマシンは前者の基礎で、ラムダ計算は後者の基礎であるということになる。
Yコンビネータについて、これによってどのような処理ができるのかというのを考えても、よい答えが出ないのはそういうわけだと思う。
