コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-
- 青土社 (2015年2月24日発売)
本棚登録 : 153人
感想 : 13件
- Amazon.co.jp ・本 (357ページ)
- / ISBN・EAN: 9784791768516
感想・レビュー・書評
-
数学基礎論についての実に素晴らしい一冊。このような本が読めることはとても幸運だ。数学基礎論や計算機科学は極めて面白い問題がたくさんあるのだが、入り口のハードルが高いこともあってなかなか平易な本はない。第一線の研究者がこのレベルの分かりやすい本を出すのは素晴らしい。
タイトルからはいま流行りの人工知能の話に見えるが、そうではない。人工知能は実際的にどのように知能を作っていくかという話。この本は知能と呼べるものは理論的にどのようなものか、そしてそれが理論的にどこまで実現可能かという話だ。知能に対する理論的限界の話といえば、ゲーデルの不完全性定理やP=NPの話がある。これらを解説した本は多い。だが、著者が正しく言うよう、これらの定理の否定的で悲観的な解説が多い。実際には肯定的な研究が数多くあるのだ(p.8)。
本書は数学基礎論や計算機科学における、理論的限界を巡る肯定的な研究を数多く扱っていく。例えば、タルスキの真理定義不可能性に対して、裏定理としてΣｎ真理述語の定義可能性を取り上げる。定義可能性は極限においてのみ崩れる。こうした理論的限界と紙一重の結果、肯定的な結果に目を向けることが重要だ(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)。
この本が提示する知的興奮を味わえる人は少ないのかもしれない。一読しただけでは味わいきれない深い本だ。またしばらくして読みなおそう。
1
詳細をみるコメント0件をすべて表示 -
【書誌情報】
『コンピュータは数学者になれるのか？ 数学基礎論から証明とプログラムの理論へ』
著者：照井 一成(1971-)
定価：3,080円（本体2,800円）
発売日：2015年2月
ISBN：978-4-7917-6851-6
ヒルベルト、ゲーデル、チューリング、ゲンツェンら天才たちの挑戦は、 いまコンピュータ科学を経由して、世界に大転換をもたらしつつある。 「不完全性定理」「P対NP問題」などの論争の歴史を最新アップデートし、 「人工知能」の未来にまで架橋する数理論理学の決定版！
「［……］証明たちは、やがてプログラムとなり、計算理論の根底と結びついた。 20世紀初頭に繰り広げられた数学基礎論争の相克は、 この強固な基盤のもと、コンピュータ科学において新たな生を授かったといえる。 この大きな力が人工数学者の誕生に向けた突破口とならないだろうか。 そんな可能性を模索しているのが現状である」（本文より）。
[http://www.seidosha.co.jp/book/index.php?id=2117]
【簡易目次】
１ 数学者を作ろう（数学者とは何か；人工言語を画定する ほか）
２ 対角線上に追い詰めろ（対角線論法とは何か；言語の限界 ほか）
３ 計算よ停まれ！（数列の生成と停止；全員整列！ ほか）
４ ＮＰの壁（しらみつぶしと数学知性；Ｐ・ＮＰとは何か ほか）
５ 活き活きした証明（ラムダ計算；証明はプログラムである ほか）
６ 対角線方向にむかう未来
0
-
貸し出し状況等、詳細情報の確認は下記URLへ
http://libsrv02.iamas.ac.jp/jhkweb_JPN/service/open_search_ex.asp?ISBN=9784791768516
0
-
この分野、やっぱりおもしろい！
証明を端折ったストーリー展開と数学的厳密さのバランスが絶妙。学生の頃に感じたワクワク感を思い出しながら読めた。
0
-
やや本格的な数学基礎論の本である。
手に取って少し読んでみるとわかるが、大学の教養程度の数学的知識があると読みやすい。
小学校で算数、中学生から数学という学問を学ぶ。
算数の授業では四則演算という「数」の基礎を勉強する。小学生足し算を勉強すると自然数がわかる。
次に引き算をすると、ある数に同じ数を引くと何もないという「０」を学ぶ。ある数にある数よりも大きい数をひくと負の数が出てくる。
掛け算は足し算の延長であることがわかるが、割り算となるとそうはいかない。
自然数や負の数、０でない数を導入する必要がある。有理数である。
そして二次方程式を勉強すると、２乗して２になる数という未知の数が出てくる。これを無理数と呼ぶ。
先の有理数と併せてこの体系を実数と呼ぶ。
これで打ち止めかと思ったら、二乗して負になる数を考える。虚数である。
実数と併せて、この体系を複素数と呼ぶ。
大学ではさらに複雑な数をいくつも学ぶことになるが、そもそもこれらの数はどのように導入してきたか？
ある定義を与えて、それを演繹的に演算することで定理を証明していく。
たとえば、1+2+3＋・・・・+n=n(n+1)/2となることを証明しよう。
高校までの知識で解くことができるだろうか？
高校までの知識とは、というところで議論がわかれるかもしれれないが、大半の人は「数学的帰納法」を使えばよい。と答えるかもしれない。
たしかに、数学的帰納法によって
１）n=1のとき成り立つ
２）n=kのとき成り立つと仮定し、n=k+1を計算すると、
1+2+・・+k+(k+1)
=k(k+1)/2+(k+1)=(k+1)(k+2)/2
となり、確かにn=k+1のときも命題は成り立つので、すべての自然数に対して、命題は成立する。 （証明終）
なるほど、確かに上記の議論は正しいし、期末テストで上記を解答すればマルをもられるだろう。
しかし、数学的帰納法は数学的に正しいことを前提としていえるが、これはどこから来たのか？
教科書ではドミノ倒しのイラストがのっており、なんとなくイメージはつくが、全然証明になっていない。
このように証明とは何か、数とは何かという数学の基礎の基礎は実は学ぶ機会が少ない。
これは特に意識しなくとも、数学が確固たる基盤の上で展開されているため、いちいち気にしなくとも問題ないという、過去の数学者の血と汗（と涙）の結晶であるためである。
本書はその基礎そのものについてスポットをあてる。
まず気になるのは出発点はどこか。ということであろうか。
昔、子供のときに○○は何で出来ているの？ゲームをしたことはないだろうか？
これを繰り返していくと、それ以上還元できないところが出てくる。普通の人なら、何で出来ているかゲームは原子（または素粒子？）でゲーム終了ではないだろうか。しかし、あくなき好奇心を持つ子供は、じゃあ素粒子は何で出来ているの？と聞いてくるが、これについては苦笑いで沈黙するしかない。
だってこの先は誰も知らないのだから。。。
数学も同じである。遡っていくとこれ以上、証明できない命題が出てくる。これを公理と呼ぶ。
公理は、これ自体証明する必要がないため、勝手に考えていい。例えば、１＝２を公理として採用しても良い。が、あまり良い数学体系にならない。
ということで、あまりに勝手に公理を取ると体系がめちゃくちゃになるが、少なすぎると、そこから生まれる体系が芳醇にならない。
つまり、必要最低限で互いに独立な公理系が最高にHappyだ。
ある公理を数個持ってきて、それが互いに独立であることは（難しいけれど）判断することができる。
なぜならば、公理A,B,CをとってきてAとBからCが証明できれば、Cは公理系として選ぶ必要はない。この場合、公理A,Bで十分ということになる。
問題は、公理A,Bの二つで十分かということである。
これは大変難しく、歴史的な問題である。
20世紀初頭に数学者の間でこれについて議論がおこった。
Hilbertは、互いに矛盾がなく、独立な公理系を選ぶことができるという考えのもと、Hilbert問題という問題を提起した。
が、これはGedelによって否定的に解決された。
つまり、どんな公理系を選ぼうとしても、その公理系で決定不可能な命題が存在するというのだ。
（決定不可能とは、その命題が真か偽か証明できないということ）
これは数学の限界を与える定理と呼んでもいいのかもしれない。
しかし、悲観してもしょうがないので、どの程度無矛盾なのか、どうやれば無矛盾をいい方向に持っていくことができるかという前向きな議論が重要である。
この点、本書に詳しく議論されている点である。
0
-
150926 中央図書館
論理規則を確認して証明図を一つ一つ確認するのは普通の読者には難しい。しかし数学の難題に対して自動証明の手法が挑戦している状況は、この本を手に取らなければ想像もしなかったところ。終章に引かれているケプラー予想の証明確認の経緯が象徴的。
0
