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

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

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

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

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

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

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

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

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

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

圧縮したまま検索

「情報処理」に載った岡野原さんの記事「圧縮したまま検索」を読んだ。簡潔データ構造の解説だけあって、文章も簡潔で難解。LOUDSの部分で振り落とされてしまった。でも面白かったので、いつか自分で実装できればと妄想している。とりあえずライブラリの名前だけ決めた。


簡単に内容の紹介すると、まず、前半ではRank/Seleect辞書を導入して、これを用いてLOUDS、ウェーブレット木、圧縮全文検索とデータ構造を導入していく。後半はこれらを実装したライブラリの紹介をしている。

で、LOUDSで分からなくなったわけだけど、何処が分からなくなったかというと$\mathbf{parent}$を求める計算のところ。$\mathbf{parent}(b) = \mathbf{select}_0(B, p)$とあるのだが…なんか違わないか。$\mathbf{parent}(b) = \mathbf{select}_1(B, \mathbf{rank_1}(B, \mathbf{select}_0(B, p)) + 1)$くらいじゃないだろうか。勘違いしているのかもしれないけど。LOUDSの解説は情報系修士にもわかるLOUDS - アスペ日記にもあるけど、こちらは定式化が微妙に違うみたいな気がする。

モナドとは何か－私の見方

（プログラミング言語の）モナドについてはいろんな人がいろいろなことを言っていて、チュートリアルも沢山ある。ただ、どうも自分が見聞きした範囲では、そういったものは両極端にわかれているように思う。一つは正確だが難解なもの。去年秋の函数型言語プログラミングの集いでのtanakhさんの講演は多分これで、あまりに難解で笑ってしまった。（悪いという意味じゃないくて、分かっている人には含蓄のある講演だったと思う。）一方で、分かりやすい説明もあって、モナドは「計算」を表すものだ、というアナロジーが使われたりする。これはプログラマにはとっつきやすい説明だけど、よく考えると何を言っているか分からない。「計算」ってなんだ？というわけで（周回遅れかもしれないけど）私なりの理解を書く意味もあるかなと思う。ちなみに分かっている人のために書いておくと、Kleisli圏を使った説明になる。


さて、何か圏$\mathcal C$を考えよう。適当なプログラミング言語の型と関数の成す圏を考えれば良い。すると、関数$f : A \rightarrow B$が$A$から$B$への射となる。ただ、実際プログラミングしていると、この関数の戻り値を拡張したくなることがままある。例えば、関数$f$を$B$の値を返すだけではなくて、エラーも返すように書き換えたくなることがある。つまり $f : A \rightarrow B + E$ ($E$はエラーの型で+は直和）を$A$ から$B$ への射と見たい。もっと一般的に、何か型構築子$M$ について、$f: A \rightarrow M B$を$A$から$B$への射と見たい。

というわけで、オブジェクトが型$A, B,\ldots$でオブジェクト$A, B$間の射が元の圏$\mathcal C$の$A, MB$間の射であるような圏$\mathcal C^M$を新たに考える。これが圏になるためには、恒等射$\eta_A : A \rightarrow MA$と射の合成$\circ^M$があって、任意の$f : A \rightarrow MB, g : B \rightarrow MC, h : C \rightarrow MD$について、次が成り立たなければならない。

1. $\eta_A \circ^M f = f \circ^M \eta_B = f$
2. $(f \circ^M g) \circ^M h = f \circ^M (g \circ^M h)$

さて、$M$がモナドである時、上記のような$\eta$と$\circ^M$を導こう。$\eta$は通常のモナドのreturnそのものである。$ｆ \circ^M g$は>>=から$f \circ (\lambda x. x >>= g)$ (ここで$\circ$は元の圏の合成）と定義できる。モナド則の左恒等則は

return a >>= f　≡ f a

だった。よって左辺を変形して

$$ \eta_A a >>= f = fa $$

よって更に左辺を変形して

$$ (\lambda x. x >>= f) (\eta_A a) = fa$$

よって

$$ \eta_A \circ  (\lambda x. x >>= f) = f$$

よって

$$ \eta_A \circ^M f = f$$.   よって上の1の最初の等式が導かれた。次に右恒等則を考える。

m >>= return　≡ m

これを使って次のような式変形を行う。

$$\begin{align*} f \circ^M \eta_B &= f \circ (\lambda x. x >>= \eta_B) \\ &= f \circ (\lambda x. x >>= \text{return}) \\ &= f \circ (\lambda x. x) \\ &= f \end{align*}$$

よって$\eta$の恒等則が言えた。次に$\circ^M$の結合則だが

$$\begin{align*} f \circ^M (g \circ^M h) (a) &= f \circ (\lambda x. x >>= (g \circ^M h)) (a) \\ &= f(a) >>= (g \circ^M h) \\ &= f(a) >>= (g \circ (\lambda x. x >>= h)) \\ &= f(a) >>= \lambda y. g(y) >>= h \\ &= (f(a) >>= g) >>= h \\ &= (f \circ^M g) \circ^M h (a)  \end{align*}$$

となって結合則が導かれた。よって$\mathcal C^M$が圏をなすことが分かった。(実はいろいろごまかしているけど)

まとめると

1. モナドというのは型AからMBへの関数を型AからBへの「関数」と思う仕掛けである
2. 正確にいうと、型をオブジェクト、型AからMBへの関数をオブジェクトAからBへの射とする圏$\mathcal C^M$がモナドMから構成できる
3. モナド則から、$\mathcal C^M$の恒等則、結合則が導ける

となる。

87クロッカーズ

byflowでのsoutaroさんの紹介を見て、買ってみた。面白いけど、「のだめ」のゴミの部屋でショパンを弾くというイメージが強烈だったのに比べると、普通な感じ。面白くなるかどうかは、今後の展開次第な気がする。パラテクとか87とか何処から来てるんでしょうね。

ところで、私はあまりハードには興味が持てなくて、それは何故かというとハードウェアをいろいろ知っても、パーツメーカーの掌で踊っているような感じがするからなんだけど、まあソフトもOSや言語の掌で踊っているといえば言える。（私の場合、ソフトと言ってもプラットフォーム依存の部分はやはりあまり興味がなくて、アルゴリズムとか言語設計そのものとかに興味が有るわけだけど。）その辺、漫画を読んでハードを触る面白さが何かしら分かればいいかもしれない。でも自分のPCに液体窒素は使わないと思うけどね。