計算モデルと論理とゲーデルの不完全性定理

ゲーデルの不完全性定理は、数学を扱う数学、つまりメタ数学を考えるが、それだと理解が難しい。しかし、証明(数学)＝プログラムという悟りを開くと、プログラムを扱うプログラム、つまりメタプログラムを考えればよくなり、それならコンパイラ等でなじみがあるので理解が優しくなる。

話の流れは以下。
1. プログラムとは何か
2. 証明とは何か
3. 証明＝プログラム

　　　　　　　　　　　　 　 　 　 ,
　　　　　　　　　　　（　　 {、　{　　 ヽ.ｰ､､
　　　　 　 　 　 　 　 ＼､__ぃ._ゝ⌒ヾ iヾ）}､_
　　　　　　　　　　　　　 ﾝ_ｰ-_二ｰ-, 〉 {厶 _､ヽ　　　　　　　　　 　 　 _
　　 　 　 　 　 　 ヽ._＞'´ ／ /,ィ／　/　ハYﾍい　　　　　　 ,.　-- 〃⌒
　r−-､　　　　　　ィ´　 〃 ,ｲ/7'　 ,ｲイ/　小ヽ 丶、　,. ‐ '´ﾊ i 　 ″｀ヽ、
、ヽ、　　　　　／幺ィ　 {从{小込v' jｩ仏厶川ﾘ}　 YV,　　 小 Vj.　|丶 　 ヽ
　｀ ｰ-ミー--'_,辷三彡'´ | V'芯`　　　芬Yjﾙ/ﾊ.　／ 　 V√ヽ._!　l＼ ＼ '⌒ヽ
　　,. -‐ ｀￣　　　　_ファィ!　"´　　 　 ｀`ﾝ'´イﾊy′　 　 l{辷 { い. ト､ヽ._ヽ､ 　 ＼
y'´　　 _＿,,_ ＿__,,彡'´八ﾑ　　　_'__　､_幺イ厶/　　　　　|'心｀VヽﾍE､ヽY　い、　 ＼
′　　　/ ｜!　 　 r==ァ'ﾞ’_ﾍ、 ´_ｰ,Ｚ.彡-―-〈 　 ‐- 、　ド¨　　　 {tﾘj ハ> ｉ｀′　　 ヽ
.　　　 / 　 !ﾘ　　　　,.幺-‐=,.イ´'´　,. / ／　　 ヽ　　　 ＼l　__ '　　 ｀ﾞ ん}.ｉ_,｣　　　　　 ｀､
.　　　 i｀¨¨´　　 . '´ ／ィ＜{V/　　/,ｲ i′　,ハ　｀､ 　 ､ぃヽ｢⌒`j 　 厶ｲl｣ 　 　 、　　　ぃ            ―――証明と
ヽい　 l 　 　 ／　 /ﾚ′／〈.い、___,{.｛ 　 , -‐　＼ ＼ｰﾍ` ｀ ｀ヒ´_イy , ﾑ、　､ 　 ヽ.　　 }.}、
｀　　＼V　 /,　　 ,{ {　 '´_,ﾑ≧ｰ､-ﾍｰ}-/　 ,. -‐-､ヽﾉ　 ヽ　 ハ ｀バ´＾)＼`ｰ-）　 }ﾊ.　 ﾊ{
　,. 、 　 >'／　　 { い.ィ／ｩ￣｀ハ}ヽ＼.{　/　　　　_Ｖごヽ.._/ 　 }ー}｀丶乙ヽ　'7ノ^　}／
ヽ'＾＼ｰ '´_,,.　-‐＜ゝ`ｰ之,_　/／　　}ﾊﾍ{、i　 　 ヽ｀ﾏTハ_ _／;　 ヽ、 ﾊ､}ﾉ┐
,､-‐¬''" ,ｲ丁二了　{　　___彡' ／　ノノ　 ﾍ!　 　 　 ｀∨だ¬ /　 ∠_｀　}ﾍ ﾝ
　〉 -r‐／√　 　 l　ハ._乙 -‐'´／´/　　　 ﾑ　　　　　　ヾ＾ ｀ｉ′　＼ ｀ ー1´ヽ
-ｰ‐¬､Y'　 　 　 |/ 　 /了¨¨´　 , '　 -‐ ' ,.小、　　 　 　 丶　!　　　 丶.　　 　 i
　　／_,.　　　 　 ,?..._ {ｲ{　　　／　　　 ／ |′丶　　　　　　 ﾏi ､_　　　　 　 　 ﾄ､　　　　　,nyぃ/
　/´ /　 　 　 ∠-- .._｀丶､　ィ"¨¨　ーﾍ　〉|　　　＼　　　　　 ヽ 　 　 -‐　　 ヽｌ　`"¨¨´￣|ｉl}い} ,        プログラムは―――
　 　 { ,ｨ,ｲ厂¨＼.！　 ｀ヽ／　'´￣｀¨マ´/　|　　　　 i>､　　 , -　＼,　'"⌒丶.　ﾊ　 _＿,,..　｣ﾘ近'´
　　　∨い､　　　｀ ',　　　　　　　　 _,. -≧ｭ､',　 　 　 |ｴ＼　　 　 　 Y 　 　 　 　 |´　　　 ,ゝだﾝｩｰ
　　　　　　　　　　　i　　　　　　,.／'´ヽ ヾ 'r-ﾍ　　　　l-, -― 、　　　l.　　　 　 　 !　　　　｀ }} ｀＾｀
　　　　　　　　　 ､_r{ヽ　　　／/´　 ,.ィ　√ }ｰﾍ　　-‐'´__,. ､　 ヽ　　 |__,,..　_、　 ､ヽ
　　　　　　　 　 ｭ?ﾑ′ , '　 /。／ ／/　,'ﾑ斗ﾍ　　／　 　 ｀¨´　 　 l　　 　 ヽ　　 丶
　　　　　　　　　ゞｲ} ,ﾑ./ 　 ∧/−-／ ｧZ/!　ｉ._ぃ (._,,..　ﾍ下､　　 ｉ ｌ |ィT_i_､_　＼.　　',
　　　　　　　　　ｹ´|./ 〈　　∧/__ ,<./ / 7/､!´ ｢ i.ﾍ r‐ ､___｀ー--‐―_､i. l i!ﾍﾍヽ、＼　}
　　　　　　　　　°厶イ＼/∨¨７｀ヽ'´ ; / l i　 l　lﾍヾヽ._｀¨`ｰｧー ﾕ´l＝ｷミ､vﾍ_ぃ.　Ｙ　　　　　　　　　「「おなじだよ♪」」
　　　　　　　　　　 ,.ゝﾍ2__,ｲ'‐ / / ′!j_!　| !. -i¬ ﾍ.く｀ヽ｀¨´ー'´/ィｹ ｉ. l ｉ! l ﾏﾍ.ﾍ＼j
　　　　　　　　　r'´　　｀¨＾ﾀ_ / / ｉ ／l_j､｜ｉ_,,. l-‐!__Vドヽ｀ー‐z_'.イ√丁| ｉ! ﾄ､i_,.Vﾍヾ｀ヽ､
　　　　　　　　　ヽ.___,.イ_/ ｀7､,'　!´ i j ﾍ Y'i,.ィ'"＾v,.--}､｀＾ﾏ´/ _/ 7√¨¨ﾏ丁ﾝj_,.ｲ´ ﾏベへ｀ヽ､
　　　　　　　　　　 ／ //‐-/､/ヽ| ／　.　Ｖ 　 !　　〉¬ｰi､_〉､Y´,_}厶_rt__ri.}└１厶ィつ}ﾍへ>>＞ぅ,
　　　　　　　　　／/ //..__/／ ヽj'　!､__!　{　jｰ-'¨´／　 厂ヽ.__ﾏ＾¨¨´　　 ｀1　 r‐}_　 ｀ｰﾗ＾´ r､√
　　　　　　　　　Z/V ヽ,くノ _ 廴_j､ﾉ　 j,.､_y'　 　 /　　 ム._广＾i　　　　　 　 ｀¨´　 ｀辷'´厶ﾉ´

　　　　　　　　　　　　　　　　　ハスケル・カリー　＆　ウィリアム・ハワード

4. プログラムできないこと（停止性問題）
5. 証明できないこと（ゲーデルの不完全性定理）

何はともあれ、定義を見てみよう。

自然数論を含む帰納的に記述できる公理系が、ω無矛盾であれば、証明も反証もできない命題が存在する。
- ゲーデルの不完全性定理

なんのこっちゃだが、今から分かりやすく説明する。

プログラムとは何か

まだコンピュータが登場していない1930年代、「計算とは何か」を考えた人たちがいた。
現代から見れば、計算はコンピュータの仕事だから、「プログラムとは何か」となる。

最も有名な計算モデルが、チューリングのチューリングマシンである。

チューリングマシン

以下の３つでできている。

• 無限に長いテープ
• テープを読み書きするヘッド
• マシンの状態を記憶するメモリ

以下のように計算をする。

チューリングマシンは単純だが、何でも計算できる。

帰納的関数

次に、クリーネの帰納的関数という計算モデルを紹介する。

帰納的関数とは、プログラムでいえば、IF-THEN-ELSEとループと代入さえあれば何でも計算できるということで、BASICやC言語の考え方に近い。
以下のように計算をする。

ループに"箱"があって、その値を書きかえるのが、C言語の教科書によくある「変数とは箱のようなもの」という話のもとである。

ラムダ計算

次に、チャーチのラムダ計算という計算モデルを紹介する。

ラムダ計算は、Haskellなどの関数型言語の基礎であり、ループの代わりに再帰(入れ子)を使う。
以下のように計算をする。

再帰に"穴"があって、その値を書きかえないのが、Haskellの教科書によくある「変数とは穴(ラベル)のようなもので、Haskellには副作用がない」という話のもとである。

余談だが、チューリングとクリーネは、チャーチの弟子である。

　　　　 ＿＿__
　　　／＿_.）)ﾉヽ
　　 .|ミ.l　_　 ._ i.）
　 （＾'ﾐ/.´・ .〈・ ﾘ
　　.しi 　　r､_） | 　チューリングとクリーネはわしが育てた
　　　 |　 `ﾆﾆ' /
　　　ﾉ　`ｰ―i´ 
   アロンゾ・チャーチ

以上の3つの計算モデルは、後になって実は等価であるとわかった。
つまり、チューリングマシンができることは帰納的関数やラムダ計算でもできるし、その逆もできるとわかった。

証明とは何か

　　 ／￣￣＼
　／　　 _ノ　　＼
　|　　　 （ ●）（●）
.　|　　　　 （__人__）　　公理からはじめて
　 |　　　　　｀ ⌒´ﾉ　　　論理をつないだものだろ、常識的に考えて…
.　 |　　　　　　 　 }
.　 ヽ　　　　　 　 }
　　 ヽ　　　　　ノ　　　　　　　　＼
　　　/　　　 く　　＼　　　　　　　 ＼
　　　|　　　　 ＼ 　 ＼ 　 　　　　　　＼
　 　 |　　　　|ヽ、二⌒)､　 　 　　　　　 ＼
    ゲルハルト・ゲンツェン

ゲンツェンが考えた自然演繹という公理系は、常識的な感覚で証明とは何かを考えたもので、名前からして"自然"とついている。

以下のように証明をする。

数学的帰納法は、プログラムでいう再帰と原理的に一緒である。

証明＝プログラム

以上３つの計算モデルと１つの公理系をまとめると以下のようになる。

名前	作者	キモ	具体例
チューリングマシン	チューリング	無限に長いテープ	コンピュータ
帰納的関数	クリーネ	無限に続くループ	C言語
ラムダ計算	チャーチ	無限に続く再帰	Haskell
自然演繹	ゲンツェン	無限に続く数学的帰納法	証明

無限に続く数学的帰納法というのは、無限にある自然数が続く限り帰納法を繰り返せるということで、つまり、ゲーデルの不完全性定理にあった"自然数論を含む帰納的"である。

証明＝プログラムについては、
自然演繹と型付きラムダ計算がぴったり対応しているすげー！というカリー＝ハワード対応を筆頭に、
プログラムを数学的に厳密に定義しようというプログラム意味論や、証明の正しさをコンピュータで検証しようという定理証明器の研究がある。

以上より、"無限ループを記述できるプログラム"＝"自然数論を含む帰納的に記述できる公理系"を認めてほしい。

プログラムできないこと(停止性問題)

どうかすると無限ループしてしまうプログラムというのは、バグっていて使い物にならない。
それでは、"プログラムが無限ループするかを判定するプログラム"を書くことはできるだろうか？というのが停止性問題である。
冒頭で述べた、プログラムを扱うプログラム、メタプログラムのおでましである。

もしできるなら、ブラウザクラッシャがポップアップを無限にだすのを未然に防げてさぞ便利だろう。
結論からいえば、停止性問題は解決不能であり、そんなプログラムは不可能である。以下で証明する。

プログラムr(r)は、停止しないか、停止するか、のどちらかである。
場合1「r(r)は停止しない」とき、then loopを通ったはずである。よって、Oracle(r,r)は、「r(r)は停止する」と答えたはずである。矛盾している。
場合2「r(r)は停止する」とき、else stopを通ったはずである。よって、Oracle(r,r)は、「r(r)は停止しない」と答えたはずである。矛盾している。
どちらの場合も矛盾しているので、そもそも、Oracleの存在を仮定したのが誤りだったことになる。
よって、Oracleは存在しない。q.e.d.

メタプログラムにできないことは他にもたくさんあるが、たいていは停止性問題に帰着できる。

証明できないこと(ゲーデルの不完全性定理)

プログラムできないプログラムがあった。
そして、"無限ループを記述できるプログラム"＝"自然数論を含む帰納的に記述できる公理系"である。
よって、証明できない証明もあるはずだ、というのが、ゲーデルの不完全性定理である。

無矛盾かつ完全な公理系がある

停止性問題は、無限ループが原因で生まれる。よって、IF-THEN-ELSEと代入しかないような、ループを書けないプログラムには、停止性問題はない。ありとあらゆるプログラムが必ず停止する。
同様に、ゲーデルの不完全性定理は、数学的帰納法が原因で生まれる。よって、「もし〜ならば」しかないような、数学的帰納法が書けない公理系には、不完全性定理はない。ありとあらゆる命題の正しさを証明できる。

例えば、命題論理は、無矛盾かつ完全な公理系である。(fuga様のコメントをいただき訂正 2010/2/17 20:50)
無矛盾かつ完全な公理系としては例えば実閉体の理論やPresburger算術の理論がある。

よって、よくある勘違いに「どんな公理系も不完全である」というのがあるが、誤りである。
ただ、無限ループを書けないプログラムや、自然数論を扱えない公理系なんて、つまらなくて考えるに値しないと思って、「どんな公理系も」と言いたくなる気持ちはわからないでもない。

ゲーデル数

メタプログラムなら、プログラムをデータ(テキストファイル)として扱うことを自然に考えられるが、
メタ証明だと、証明を自然数として扱うという、頭の痛くなることを考えるはめになる。それがゲーデル数の考え方である。
ゲーデルはきっと大変だったろう。

停止性問題に似た数学の問題

例1. 円周率 3.141592... に、今日の日付 20100217 は出てくるだろうか？　あるいは、任意の自然数が出てくるだろうか？
出てくるまで計算を続けるしかない。もしかしたら永遠に出てこないかもしれない。

例2. コラッツの問題
数学の未解決問題である。有限回で必ず停止するか？というのが、停止性問題を連想させる。

ラッセルのパラドックス

停止性問題の結論は、プログラムが無限ループするかを判定するプログラムは無限ループする、だった。
つまり、

無限ループを判定するプログラム自身が、無限ループするプログラムの集合に含まれる。
不完全性定理の具体例としてよくあげられる、ラッセルのパラドックスの、床屋版が以下である。

ある村でたった一人の男性の床屋は、自分で髭を剃らない人全員の髭を剃り、それ以外の人の髭は剃らない。この場合、床屋自身の髭は誰が剃るのだろうか？

つまり、

自分で髭を剃らない人の髭を剃る人自身が、自分で髭を剃らない人の集合に含まれる。

停止性問題とラッセルのパラドックスは、よく似ている。

ゲーデルの不完全性定理の意義

普通にプログラムを書いていれば、メタプログラムや停止性問題には出会わない。
同様に、普通に証明を書いていれば、メタ数学や不完全性定理には出会わない。
停止性問題で困るプログラマがいないのと同様、不完全性定理で困る数学者もいない。

強いて言えば、停止性問題を知っていると、ブラウザクラッシャを未然に防ぐメタプログラムを開発しろ、と言われたとき、それは無理です、とすぐ断れる。
同様に、不完全性定理を知っていると、数学の無矛盾性を数学で証明しろ、と言われたとき、それは無理です、とすぐ断れる。

実用性はあまりない。

オブジェクト指向

今まで黙っていたが、オブジェクト指向(アクターモデル)も、立派な計算モデルである。

オブジェクト指向は、ヒューイット、アラン・ケイなどが60〜70年代に考え出した。
以下のように計算する。

ラムダ計算とオブジェクト指向は、よく似ている。クロージャとオブジェクトの微妙な関係

(ラムダ計算)

プログラムはなぜ動くか

抽象的な計算モデルが、だんだんほぐれて、チューリングマシンに落ちる様子を描いてみた。

いろんな事情があって、Coq(定理証明器) -> OCaml(型付きラムダ計算) -> C言語(帰納的関数) -> コンピュータ(チューリングマシン) という、コンパイラのピラミッドができているのが面白い。

参考文献

• Computability and Complexity: From a Programming Perspective (Foundations of Computing)

• Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)

• P.Wadler, Proofs are Programs(PDF)
• d.y.d, Curry-Howard Isomorphism
• クロージャとオブジェクトの微妙な関係
• 不完全性定理について(あるいは証明と計算について)