人間と証明とプログラム: 『コンピュータは数学者になれるのか？』を読んだ

ウィッシュリストに入れていたのを知人に頂いた。数学基礎論とコンピュータ科学をつなぐ啓蒙書、という立ち位置の本なのだけど、自分はコンピュータ科学のバックグラウンドとしての数学基礎論、というとらえ方で読んでいった。専門的な概念とか簡単な証明とかはバンバン出てくるので基礎を抑えておかないと読むのには難儀しそう。以下、おもしろかった部分を整理がてらかいつまんで説明してみる。あまり丁寧ではないけど、間違っていたら教えてください。

書名にもある「数学者」とは真理を追い求める人のことで、ひいては与えられた命題に対する定理を証明するものである、と最初に位置づけられる。なので人間の証明能力をどのようにして・どこまで機械化できるのか、というところからこの本の話は始まる。

形式系

第1章は数学的な準備の章。まず、証明のための言語と推論規則からなる形式系を定める。自然数について語れるよう定義された形式系 が、本書の出発点となる仮想の数学者になる。形式系は拡大していくことができ、 に一部の文に対する数学的帰納法の能力を与えてより高度な 、さらにすべての文に解放して （ペアノ算術） ……と、能力や表現力を高めながら形式系を積み上げていくことができる。また、形式系の推論規則を組み合わせて論理式の証明図を書きあげられるとき、形式系は論理式を証明できる、という。

ゲーデルの不完全性定理とゲンツェンの無矛盾性証明

続く第2章から第5章まではそれぞれ、数学基礎論の否定的・肯定的結果、コンピュータ科学の否定的・肯定的結果の章になっている。数学基礎論の否定的結果といえば、無矛盾な形式系がそれ自身の無矛盾性を証明できない*1というゲーデルの（第二）不完全性定理。2章はこの結果に向かってほぼ一本道に突き進んでいく。ちなみに「はじめに」を読み直していたら、とあるメタ的な理由により、本書第1、2章は中高生程度の数学知識を持つ読者を対象にしています。とあって、はてどういうことだろう、と思ったことを思いだした。種明かしはちゃんとしてあった（忘れてたけど）。

というのが数学基礎論における「できない」だったわけだけど、逆に「できる」は何なのか、という話が第3章で続く。ここではゲンツェンの無矛盾性証明が紹介されている。ゲンツェンは にちょうど という順序数についての超限帰納法を加えると、 の無矛盾性を証明できることを示した。ゲーデルの結果に対し、具体的にどんな能力を与えたら無矛盾性を証明できるようになるのか？ を明らかにしているわけだ。

対角線論法

本書を貫く重要なワードのひとつが対角線論法。自然数の集合と実数の集合の濃度を分離するのに登場したあと、これが何度も、いろいろな場所で登場する。自己言及の匂いのあるとき対角線論法が現れるという感じか。実際強力な道具であることを見せつけられるが、後半第4章でこれまた有名な P 対 NP 問題が登場したときには力を発揮できない。 であることが知られている問題のクラスの関係において、 と は対角線論法によって分離できるが、肝心の と に関してはうまくいかない。対角線論法は量的な違いに対しては効くが、質的な違いに対しては有効でなく、それ以外にも P 対 NP 問題へのアタックはこれまでの数学基礎論の方法を応用してさまざまに試みられるが、どうも上手くいかない、という話で、これが面白い。

論理式の不動点

2.2 節で論理式の不動点を見つける過程でも対角線論法が使えるという話が出てきたけど、図式的にどういう対角線になるのか分からなかったので厳密さはともかく自分で書いてみた。

1変数論理式 に対して、操作 の不動点を見つけたい。ゲーデル数 を持つ1変数論理式を とおき、表の縦と横に並べる。表の中で行 と 列 が出会うところには、 を埋める。対角線の各要素に対して を適用し、 を得る。ここである行 が存在し、 が成立するはずである。このとき行 k と対角線の交わるところに注目すると であり、 は の不動点になっている。

			…
	︙
︙	︙	︙	⋱
			…

ラムダ式の不動点

同じように定理 5.1 のラムダ式の不動点も図式的に発見できる。ラムダ式 の不動点を発見したいのだとする。すべてのラムダ式に番号をふって（ゲーデル化とかでできると思う） とし、表の縦と横に並べる。表の中で行 と列 が出会うところは とおく。対角線の各要素に を適用し、 を得る。ここである行 が存在し、 が成立するはずである。このとき、この行と対角線が交わるところに注目すると であり、 が の不動点になっている。これは とβ同値。なるほど自分で書いてみるとこの謎の形の式も理解できるような気になる……。

			…
	︙
︙	︙	︙	⋱
			…

構成的証明

もう一つおもしろかったのが、構成的な証明と非構成的な証明の話。構成的な証明というのは具体的に証拠を提示する手続きになっていて、背理法はこの証拠を提示できないから構成的な証明には含まれない。これまで扱ってきたペアノ算術などは推論規則に背理法を許す古典論理にもとづいているが、これを除いた直観主義論理という論理体系もある。直観主義論理における証明は構成的であり、その証明図のひとつひとつのステップはラムダ項を構築したりバラしたりする操作とぴったり対応する。そしてこのことから、論理式を型と、その証明をプログラムと対応づけることのできるというカリー・ハワード対応が導かれる。

では構成的な証明だけがプログラムに対応するのか？ というとそんなことはなくて、面白いことに論理における背理法が（Scheme で言うところの）call/cc に対応することから、カリー・ハワード対応は古典論理にも拡張できる。また、古典論理における証明を直観主義論理における証明に翻訳する方法と、call/cc を含む関数型プログラムを CPS 変換によって純粋関数型プログラムに変換する方法とが対応する！ これは10年くらい前にウェブで見て面白かったやつ（Curry-Howard Isomorphism - d.y.d.）だなー。と思って調べてみたら本当に10年前だった。

感想

見知ったワードが幾つか出てくるけど、それぞれお話程度の理解しかなかったので、その関係も含めてもう一歩踏み込んだ数学的詳細を追うことができてよかった。面白かった大きなトピックを拾ってここには書いてみたけれど、本の中での議論はとうぜんもっと詳細だし他の話もいろいろ出てくるので、興味を持ったらちゃんと読むといいと思います。

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

その他の資料

• 直観主義論理への招待 著者による数学基礎論サマースクール講義資料
• 計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座) ラムダ計算について詳しく。領域理論の話もあったけどよく分かってなかった……
• 情報科学における論理 (情報数学セミナー) sequent 計算という自然演繹とはまた違った形式系を主にしている

*1:もちろん本ではもっとちゃんと述べてある

A Tour of Go のその先: 『みんなのGo言語【現場で使える実践テクニック】』

著者の一人であり、同僚でもある songmu さんに『みんなのGo言語』をいただきました。Go言語界隈の有名人がずらりと顔を並べていて豪華。拙作のツールも大きく取りあげていただいて、ありがたいです。

自分もGoという言語が好きで、趣味ではよく書いている（最近はおろそかだけど）んだけど、執筆陣はリアルワールドでGoを使いこなしている歴歴。オムニバス形式の各章がそれぞれの著者の背景を反映してバラエティに富んでおり、A Tour of Go、Effective Goを終えた人が、入門一歩先のGoをつまみ食いするのにとても良い本だと思った。

思ってみれば、Goは簡素な文法をもつようデザインされていて、要所を押さえた標準のツーリング等々を見ても、その使用者に与えられている道具というのが意図的に限られている言語だった。そしてそのことが、コードだとかプロジェクトの構成だとかの、書かれたものとしてのGo言語全体の複雑度を下げることに貢献しているのだけれど、一方でGoはさまざまの実用的な目的のために使われる言語でもあり、使用者はその乏しい表現力の中でいかに現実的な課題を解くのか、という問題に直面することにもなる。

そこでGoで本格的なプログラムを書くには、言語そのものへの知識に加えて、その周辺に醸成されているイディオム的な語彙を身につけることが他の言語に比較して重要になると思う。そういうものってのは常にドキュメントされているものではないわけで、Go的なやり方を知るためには例えば自分はGo公式のソースコードを読んできた（この本でも何人かの著者が紹介している）けれど、今回この本が登場したことで、より分かりやすい形での指南役が増えたのは喜ばしいことだと思う（あと『Go言語によるWebアプリケーション開発』の鵜飼さんによる巻末付録とかもいい）。

すでに語られているし、個別の内容にはあまり触れる必要はなさそうだけど……、songmu さんによる1章、fujiwara さんによる3章、suzu_v さんによる6章はGoを書く人なら全員読む価値があり、mattn さんによるマルチプラットフォーム、deeeet さんによるコマンドラインツール、lestrrat さんによる reflect パッケージはそれぞれ各論のすばらしい解説になっている。自分はLL的なバックグラウンドをもっているのだけれど、そういう観点から見たGoというのも各所で語られていてよかった。

今後Goの入門系の書籍であればウェブアプリケーションとか、並行処理に特化した話題も気になってくるところですね。読みたい〜。

みんなのGo言語【現場で使える実践テクニック】

会社は何のためにあるのか: 『ビジョナリー・カンパニー』を読んだ

ビジョナリー・カンパニー ― 時代を超える生存の原則

世界を見わたして長いこと生き残り、また業界で抜きん出ている会社（ビジョナリー・カンパニー）を取りあげて、それが他の会社と違っている点は何なのか分析した本。半世紀以上も経てば世界の状況は変わり、経営者以下みな代替わりしてゆくものだけど、それでも会社として生き残った、そしてこれからもそうであろうと思える理由というのは何なのかってのを見ていく。

それは経営者の資質だとか主力製品などでは決してない。それらに依存しているような会社は、たとえその時は栄華をものにできたとしても、やがて訪れる避けられない市場の変化や人物の不在という事態には耐えられない。必要なのはすぐれた人物や製品よりも、すぐれた組織づくりの方だ。会社が作り出す究極の作品は、その会社自身なのだとこの本ではいっている。

価値観と目的

では状況の変化に耐えながら会社が生き残る秘訣は何か。それは組織の基本理念をはっきりと定め、自覚することだ。すべての決定がそれに則っておこなわれ、それ以外のことが変わってもこれだけは変わらない、そんな理念を組織の背骨に据えなければいけない。

基本理念は基本的価値観と目的とで構成される。基本的価値観は時代を越えて不変の主義であり、短期的な利益や事情で曲がらない。目的は組織の存在理由になるもの。これは組織の内側に向けた価値観と、外向きの目的と分類できると思う。

基本的価値観を会社の中心に据え、それでも時間の経過に耐えるには進歩への意欲、変化を許す風土が必要だ。そしてそれらは仕組みとして定着させなければいけない。そうでなければ時代とともに失われてしまうからだ。

本を読むと各社がどんな行動を取ってきたのかという例がたくさん載っている。なるほどこの原則に即していると思う。もちろん盲目的に従えばよいというものではないけれど、大企業とよばれるような会社が今にいたるまでどんな決断をくだしてきたのかを知るだけでも面白い。

会社は何のためにあるのか

基本理念を達成することで会社が生き残り、そのプロセスがずっと続くのならば、人びとが集まって会社を動かすことの意味は、会社の考えるような、人間ひとりではとうてい実現できない大きな善を生み出して、価値観を維持していくことにある。そしてそのことに本当に意味があるのなら、その営みはずっと続いていくだろうし、会社で働くことも無駄ではないだろう。

……と思えたので、いい本だった。別に経営者のためだけに道を示してくれるのではなく、規模や時間的なスケールの違いはあれど、ある程度以上の人間が入れ代わりながら関わる組織（それこそ、社内のチームとか）であればこの精神を活かすことはできるはずだ。

Kindle 版もあった。

ビジョナリー・カンパニー　時代を超える生存の原則

おまけ。陳腐な表現だけど、組織は生物のようだと思ったのだった。

生命とは何か―物理的にみた生細胞 (岩波文庫)