ソラリスの海はチューリングマシンの夢を見るか

今年はチューリングの生誕１００周年らしい。で、チューリングの一番の貢献というと、やはりチューリングマシンを定義したことだろう。皆さんも御存知の通り、現代の計算機科学では、チューリングが考えたチューリングマシンを使って、計算可能性を定義する。これをチャーチのテーゼというのだけど、これについて考えてみたい。

そもそもチャーチのテーゼはどういうステータスの言明なのだろうか。経験的に検証/反証可能な命題なのだろうか、それとも反証も検証も意味が無いような、計算概念の定義とみなすべきなんだろうか。

もし計算概念の定義と見れば、多分これは、位相空間で空間概念を定義するのと似ている。位相空間の場合、まず空間という概念について我々が持っている直観があって、これをできるだけ満たしていてかつ厳密な定義を与えた、ということなのだと思う。これをチューリングマシンに当てはめると、チューリングマシンが、有限的なルールで記述される記号操作、という直観を上手く定式化しているということだろう。いろいろな定義が提唱されたけど、結局皆チューリングマシンと同等になったというのも位相空間の場合と似ている。チューリングマシンは、記憶領域に1次元のテープを用いる所が少しアドホックな気がするけど、記憶領域をテープの代わりにRAMやスタックにしても計算可能な関数は変わらないし、量子計算とかにしても変わらない。

ただ、位相空間の場合、3次元であったり4次元であったりする現実の空間が何であるかについて議論しているわけではなくて、数学は数学で自分たちで定義した空間概念で一応やってみる。それで現実の空間が何であるかは物理の仕事、数学はそのための材料を提供しているに過ぎない、と思われる点がアナロジーとしては少し気持ち悪い。どうして気持ち悪いかというと、チャーチのテーゼの場合、それは計算機科学の出発点のようになっていて、それを検証するということはなされていない、というよりどうやって検証するのか、見当もつかない。

話をさらにややこしくするのが、計算可能な手続全体をどう定式化して良いかなかなかわかりにくいのと相反して、個別に計算手続きが与えられた時、それが実行可能な計算であることは直観的に分かるような気がすることだと思う。このことから、例えばAckerman関数は計算可能だと思えることからチャーチのテーゼを検証する、と言った具合にチャーチのテーゼに対する検証実験というのが考えられそうだ。ただ、私的にはこういうのを検証実験と呼ぶには抵抗があって、それってただ意見聞いてるだけな気がする。

では、チューリングマシン以外に何か計算概念の定式化はあり得るだろうか。

一つは弱める方に行くことで、例えば作業テープの長さが無限大というのは厳格有限主義の立場からするとちょっとまずい。で、これを入力の多項式時間とかに制限するとPSPACEになる。あるいは定数にしてしまうと有限状態機械になる。

逆に強める方に行くとどんなものがあるかというと、例えば極限計算可能性などがあると思う。これは、一回で答えに到達するのではなく、無限回繰り返し答えを出し、ある時点で正しい答えになっていればよい、というもの。ただし、どの時点で正しい答えになっているかは分からない。例えば、停止問題などは極限計算可能になる。また、ヒルベルトが基底定理を証明した時、このような意味での計算可能性を念頭に置いていた、と林晋先生に聞いたことがある。我々が学ぶヒルベルトの基底定理の証明はとても非構成的だけど、それは20世紀になってあまり構成可能性を気にしなくなってからの再構成であって、オリジナルはかなり構成的なのだそうだ。

さて、表題に出るソラリスの海について。ソラリスの海はどんな計算概念を持っているのだろうか。計算概念など持っていない、という気が私にはする。有限的な手続き、という発想がソラリスの海には似合わなさそう。