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

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

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

形式系

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

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

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

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

対角線論法

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

論理式の不動点

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

1変数論理式 $A(x)$ に対して、操作 $\theta : B \mapsto A (\lceil B \rceil)$ の不動点を見つけたい。ゲーデル数 $n$ を持つ1変数論理式を $B_n$ とおき、表の縦と横に並べる。表の中で行 $B_r$ と列 $B_c$ が出会うところには、 $B_r(\lceil B_c \rceil) = B_r(c)$ を埋める。対角線の各要素に対して $\theta$ を適用し、 $A(\lceil B_n(n) \rceil)$ を得る。ここである行 $B_k(n)$ が存在し、 $B_k(n) \leftrightarrow A(\lceil B_n(n) \rceil)$ が成立するはずである。このとき行 k と対角線の交わるところに注目すると $B_k(k) = A(\lceil B_k(k) \rceil)$ であり、 $B_k(k)$ は $\theta$ の不動点になっている。

	$B_1$	$B_2$	…	$B_k$
$B_1$	$A(B_1(\lceil B_1 \rceil))$
$B_2$	︙	$A(B_2(\lceil B_2 \rceil))$
︙	︙	︙	⋱
$B_k$	$B_k(\lceil B_1 \rceil)$	$B_k(\lceil B_2 \rceil)$	…	$B_k(\lceil B_k \rceil) \leftrightarrow A(\lceil B_k(\lceil B_k \rceil) \rceil)$

ラムダ式の不動点

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

	$T_1$	$T_2$	…	$T_k$
$T_1$	$M (T_1 T_1)$
$T_2$	︙	$M (T_2 T_2)$
︙	︙	︙	⋱
$T_k$	$T_k T_1$	$T_k T_2$	…	$T_k T_k =_\beta M(T_k T_k)$

構成的証明

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

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

感想

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

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

作者: 照井一成
出版社/メーカー: 青土社
発売日: 2015/02/24
メディア: 単行本
この商品を含むブログ (8件) を見る

その他の資料

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

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

詩と創作・思索のひろば

ドキドキギュンギュンダイアリーです!!!