Gemmaの日記 このページをアンテナに追加 RSSフィード

2010-02-16

計算モデルと論理とゲーデルの不完全性定理 01:22  計算モデルと論理とゲーデルの不完全性定理を含むブックマーク  計算モデルと論理とゲーデルの不完全性定理のブックマークコメント

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

話の流れは以下。

1. プログラムとは何か

2. 証明とは何か

3. 証明=プログラム

                   ,
           (   {、 {   ヽ.ー、、
               \、__ぃ._ゝ⌒ヾ iヾ)}、_
              ン_ー-_二ー-, 〉 {厶 _、ヽ              _
             ヽ._>'´ / /,ィ/ / ハYヘい       ,. -- 〃⌒
 r−-、      ィ´  〃 ,イ/7'  ,イイ/ 小ヽ 丶、 ,. ‐ '´ハ i   ″`ヽ、
、ヽ、     /幺ィ  {从{小込v' jゥ仏厶川リ}  YV,   小 Vj. |丶   ヽ
 ` ー-ミー--'_,辷三彡'´ | V'芯`   芬Yjル/ハ. /   V√ヽ._! l\ \ '⌒ヽ
  ,. -‐ ` ̄    _ファィ! "´     ``ン'´イハy′    l{辷 { い. ト、ヽ._ヽ、   \
y'´   __,,_ ___,,彡'´八ム   _'__ 、_幺イ厶/     |'心`VヽヘE、ヽY い、  \
′   / |!    r==ァ'゙’_ヘ、 ´_ー,Z.彡-―-〈   ‐- 、 ド¨    {tリj ハ> i`′   ヽ
.    /   !リ    ,.幺-‐=,.イ´'´ ,. / /   ヽ    \l __ '   `゙ ん}.i_,」      `、
.    i`¨¨´   . '´ /ィ<{V/  /,イ i′ ,ハ `、   、ぃヽ「⌒`j   厶イl」     、   ぃ ―――証明と
ヽい  l     /  /レ′/〈.い、___,{.{   , -‐ \ \ーヘ` ` `ヒ´_イy , ム、 、   ヽ.   }.}、
`  \V  /,   ,{ {  '´_,ム≧ー、-ヘー}-/  ,. -‐-、ヽノ  ヽ  ハ `バ´^)\`ー-)  }ハ.  ハ{
 ,. 、   >'/   { い.ィ/ゥ ̄`ハ}ヽ\.{ /    _Vごヽ.._/   }ー}`丶乙ヽ '7ノ^ }/
ヽ'^\ー '´_,,. -‐<ゝ`ー之,_ //  }ハヘ{、i    ヽ`マTハ_ _/;  ヽ、 ハ、}ノ┐
,、-‐¬''" ,イ丁二了 {  ___彡' / ノノ  ヘ!      `∨だ¬ /  ∠_` }ヘ ン
 〉 -r‐/√    l ハ._乙 -‐'´/´/    ム      ヾ^ `i′ \ ` ー1´ヽ
-ー‐¬、Y'      |/   /了¨¨´  , '  -‐ ' ,.小、       丶 !    丶.     i
  /_,.      ,?..._ {イ{   /    / |′丶       マi 、_         ト、     ,nyぃ/
 /´ /      ∠-- .._`丶、 ィ"¨¨ ーヘ 〉|   \      ヽ     -‐   ヽl `"¨¨´ ̄|il}い} , プログラムは―――
    { ,ィ,イ厂¨\.!  `ヽ/ '´ ̄`¨マ´/ |     i>、   , - \, '"⌒丶. ハ  __,,.. 」リ近'´
   ∨い、   ` ',         _,. -≧ュ、',      |エ\       Y         |´    ,ゝだンゥー
           i      ,./'´ヽ ヾ 'r-ヘ    l-, -― 、   l.        !    ` }} `^`
          、_r{ヽ   //´  ,.ィ √ }ーヘ  -‐'´__,. 、  ヽ   |__,,.. _、  、ヽ
          ュ?ム′ , '  /。/ // ,'ム斗ヘ  /    `¨´    l     ヽ   丶
         ゞイ} ,ム./   ∧/−-/ ァZ/! i._ぃ (._,,.. ヘ下、   i l |ィT_i_、_ \.  ',
         ケ´|./ 〈  ∧/__ ,<./ / 7/、!´ 「 i.ヘ r‐ 、___`ー--‐―_、i. l i!ヘヘヽ、\ }
         °厶イ\/∨¨7`ヽ'´ ; / l i  l lヘヾヽ._`¨`ーァー ユ´l=キミ、vヘ_ぃ. Y         「「おなじだよ♪」」
           ,.ゝヘ2__,イ'‐ / / ′!j_! | !. -i¬ ヘ.く`ヽ`¨´ー'´/ィケ i. l i! l マヘ.ヘ\j
         r'´  `¨^タ_ / / i /l_j、|i_,,. l-‐!__Vドヽ`ー‐z_'.イ√丁| i! ト、i_,.Vヘヾ`ヽ、
         ヽ.___,.イ_/ `7、,' !´ i j ヘ Y'i,.ィ'"^v,.--}、`^マ´/ _/ 7√¨¨マ丁ンj_,.イ´ マベへ`ヽ、
           / //‐-/、/ヽ| / . V   !  〉¬ーi、_〉、Y´,_}厶_rt__ri.}└1厶ィつ}ヘへ>>>ぅ,
         // //..__// ヽj' !、__! { jー-'¨´/  厂ヽ.__マ^¨¨´   `1  r‐}_  `ーラ^´ r、√
         Z/V ヽ,くノ _ 廴_j、ノ  j,.、_y'    /   ム._广^i        `¨´  `辷'´厶ノ´

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

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

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

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

自然数論を含む帰納的に記述できる公理系が、ω無矛盾であれば、証明も反証もできない命題が存在する。

- ゲーデルの不完全性定理

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

プログラムとは何か

まだコンピュータが登場していない1930年代、「計算とは何か」を考えた人たちがいた。

現代から見れば、計算はコンピュータの仕事だから、「プログラムとは何か」となる。

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

チューリングマシン

http://eva-lu-ator.net/~gemma/geocities/godel/turing.png

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

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

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

http://eva-lu-ator.net/~gemma/geocities/godel/turing321.png

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

帰納的関数

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

http://eva-lu-ator.net/~gemma/geocities/godel/kleene.png

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

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

http://eva-lu-ator.net/~gemma/geocities/godel/kleene321.png

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

ラムダ計算

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

http://eva-lu-ator.net/~gemma/geocities/godel/church.png

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

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

http://eva-lu-ator.net/~gemma/geocities/godel/church321.png

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

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

     ____
   /__.))ノヽ
   .|ミ.l _  ._ i.)
  (^'ミ/.´・ .〈・ リ
  .しi   r、_) |  チューリングとクリーネはわしが育てた
    |  `ニニ' /
   ノ `ー―i´
アロンゾ・チャーチ

以上の3つの計算モデルは、後になって実は等価であるとわかった。

つまり、チューリングマシンができることは帰納的関数やラムダ計算でもできるし、その逆もできるとわかった。

証明とは何か

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

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

http://eva-lu-ator.net/~gemma/geocities/godel/gentzen.png

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

http://eva-lu-ator.net/~gemma/geocities/godel/gentzen321.png

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

証明=プログラム

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

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

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

証明=プログラムについては、

自然演繹と型付きラムダ計算がぴったり対応しているすげー!というカリー=ハワード対応を筆頭に、

プログラムを数学的に厳密に定義しようというプログラム意味論や、証明の正しさをコンピュータで検証しようという定理証明器の研究がある。

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

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

どうかすると無限ループしてしまうプログラムというのは、バグっていて使い物にならない。

それでは、"プログラムが無限ループするかを判定するプログラム"を書くことはできるだろうか?というのが停止性問題である。

冒頭で述べた、プログラムを扱うプログラム、メタプログラムのおでましである。

もしできるなら、ブラウザクラッシャがポップアップを無限にだすのを未然に防げてさぞ便利だろう。

結論からいえば、停止性問題は解決不能であり、そんなプログラムは不可能である。以下で証明する。

http://eva-lu-ator.net/~gemma/geocities/godel/terminate.png

プログラム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. コラッツの問題

数学の未解決問題である。有限回で必ず停止するか?というのが、停止性問題を連想させる。

ラッセルのパラドックス

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

つまり、

無限ループを判定するプログラム自身が、無限ループするプログラムの集合に含まれる。

不完全性定理の具体例としてよくあげられる、ラッセルのパラドックスの、床屋版が以下である。

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

つまり、

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

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

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

普通にプログラムを書いていれば、メタプログラムや停止性問題には出会わない。

同様に、普通に証明を書いていれば、メタ数学や不完全性定理には出会わない。

停止性問題で困るプログラマがいないのと同様、不完全性定理で困る数学者もいない。

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

同様に、不完全性定理を知っていると、数学の無矛盾性を数学で証明しろ、と言われたとき、それは無理です、とすぐ断れる。

実用性はあまりない。

オブジェクト指向

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

http://eva-lu-ator.net/~gemma/geocities/godel/hewitt.png

オブジェクト指向は、ヒューイットアラン・ケイなどが60〜70年代に考え出した。

以下のように計算する。

http://eva-lu-ator.net/~gemma/geocities/godel/hewitt321.png

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

http://eva-lu-ator.net/~gemma/geocities/godel/church.png(ラムダ計算)

プログラムはなぜ動くか

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

http://eva-lu-ator.net/~gemma/geocities/godel/pyramid.png

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

参考文献

fugafuga 2010/02/17 12:50 間違いがあるので指摘します。
>例えば、命題論理は、無矛盾かつ完全な公理系である。
>よって、よくある勘違いに「どんな公理系も不完全である」というのがあるが、誤りである。
論理の演繹システムについて言われる「完全」というのは、公理系の「完全」とは異なります。
なので「どんな公理系も不完全である」への反論としては不適切です。
完全な公理系としては例えば実閉体の理論やPresburger算術の理論があります。

ShoonShoon 2010/02/17 14:41 証明=プログラム ってとこ詳しく説明願いたいんだが、、、
プログラム=任意の自然数 N に対して命題p(N)が成り立つことを帰納的に証明する
って考えればOK??

GemmaGemma 2010/02/17 20:51 fuga様
おっしゃる通りです。訂正しました。
ゲーデルの不完全性定理とゲーデルの完全性定理の"完全"は全く違う意味だから注意せよというやつにまんまと引っかかりました。
有益なコメントありがとうございます。

GemmaGemma 2010/02/17 21:07 Shoon
証明=プログラムについては、参考文献に挙げたP.WadlerのProofs are Programsが面白いです。
もう少し堅い説明は↓がおすすめです(参考文献に追加しました)。
http://www.ice.nuie.nagoya-u.ac.jp/~h003149b/lang/p/frag/frag_g.html

tobarikitobariki 2010/02/18 01:20 とても面白かったので、
がんばってゲーデルの不完全定理を理解したいと再熱しました。

GemmaGemma 2010/02/18 13:44 tobariki様
ありがとうございます。

staff456staff456 2010/03/03 19:56 こんにちは。2chRSSのやつ、使わせていただいてます。
で、質問なんですが、最後のURLに //が2つついているのは仕様でしょうか?

http://2ch2rss.dip.jp/rss.xml?url=http://venus.bbspink.com/test/read.cgi/megami//1202620202

こんな感じになるのでリーダーに登録できません・・・

GemmaGemma 2010/03/17 17:49 staff456様
修正しました。ご迷惑をおかけして申し訳ありませんでした。