Entries

照井一成『コンピュータは数学者になれるのか?』

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-
数学基礎論についての実に素晴らしい一冊。このような本が読めることはとても幸運だ。数学基礎論や計算機科学は極めて面白い問題がたくさんあるのだが、入り口のハードルが高いこともあってなかなか平易な本はない。第一線の研究者がこのレベルの分かりやすい本を出すのは素晴らしい。

タイトルからはいま流行りの人工知能の話に見えるが、そうではない。人工知能は実際的にどのように知能を作っていくかという話。この本は知能と呼べるものは理論的にどのようなものか、そしてそれが理論的にどこまで実現可能かという話だ。知能に対する理論的限界の話といえば、ゲーデルの不完全性定理やP=NPの話がある。これらを解説した本は多い。だが、著者が正しく言うよう、これらの定理の否定的で悲観的な解説が多い。実際には肯定的な研究が数多くあるのだ(p.8)。

本書は数学基礎論や計算機科学における、理論的限界を巡る肯定的な研究を数多く扱っていく。例えば、タルスキの真理定義不可能性に対して、裏定理としてΣn真理述語の定義可能性を取り上げる。定義可能性は極限においてのみ崩れる。こうした理論的限界と紙一重の結果、肯定的な結果に目を向けることが重要だ(p.95-97)。また、ゲーデルの不完全性定理に対しては、ゲンツェンの証明論的順序数の分析が対置される。「できない」結果ではなく、「ではどこまでならできるのか」が重要なのだ(p.137f)。ゲンツェンが明らかにしたのは、無矛盾性証明がどこまでできないかである(p.187f)。ここで明らかになった、証明図の代数構造こそ、新たな地平を拓くものだった(p.191-194)。ゲンツェンの試みと結果は、本書を通じて大きく取り上げられる。ゲーデルを取り上げてゲンツェンを取り上げない、巷の不完全性定理の解説は明らかに不十分なのだ。

後半は計算量の理論の話。ここでも単純にP=NP問題を取り上げるのではなく、PとNPの間に様々な階梯が存在することを明らかにしていく。例えばP=NPに対して、タルスキの真理定義の有界論理バージョンが対置される(p240-242)。そしてその後は、証明の自動化に話が移っていく。構成的プログラミングの話から、coq派論理主義・形式主義・直観主義の究極の融合形態としての構成計算へ(p.286-289)。古典論理に対するカリー=ハワード対応で重要な、継続とCPS変換についての解説は非常によく書けている(p.305-308)。

この本が提示する知的興奮を味わえる人は少ないのかもしれない。一読しただけでは味わいきれない深い本だ。またしばらくして読みなおそう。
スポンサーサイト
この記事にトラックバックする(FC2ブログユーザー)
http://exphenomenologist.blog100.fc2.com/tb.php/750-66459cb9

トラックバック

コメント

コメントの投稿

コメントの投稿
管理者にだけ表示を許可する