檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2006-01-04 (水)

プログラマのための「ゲーデルの不完全性定理」(1)

| 07:56 | プログラマのための「ゲーデルの不完全性定理」(1)を含むブックマーク

「プログラマのためのJavaScript」の番外シリーズ -- いやっ、ホントに。

これはシリーズのハブエントリーです。番号を(0じゃなくて)1にしたのは、全体目次だけじゃなくて内容が含まれるから。

    ※ 印刷時にはサイドバーは消えるはずです、お試しください。

シリーズ全体目次(予定)

  1. (この記事;総論)
  2. 速攻速習編
  3. 自己適用からゲーデル化へ
  4. 「展望」への緊急パッチ(オハナシだよ)
  5. Reflective JavaScript
  6. 停止問題の構造
  7. 不完全性定理の構造

今回の内容:

  1. ゲーデルの不完全性定理とプログラミング
  2. ゲーデルが示したこと
  3. 不完全性定理の兄弟 -- 停止問題
  4. JavaScript使うんだもんね
  5. 関連する記事(参考)

●ゲーデルの不完全性定理とプログラミング

「ゲーデル」(人名;Kurt Godel、'o'の上に点々が付いてる)や彼の「不完全性定理」とかって、名前くらいは聞いたことがあるでしょ。えっ、ない? ゲーデルって人は「論理体系で出来ることには限界があるよ」ってことをハッキリと示して(それが不完全性定理)、人々をがっかりさせたのです(喜んだ人もいますが、もちろん)。

「不完全性定理は、人間の知性/理性の限界を示した」とか言う人(例:オッペンハイマー)もいるけど、ゲーデルの定理は、あくまでも論理体系の能力/機能に関するものです。(形式的な)論理体系は一種の抽象機械ですから、不完全性定理の主張を「計算機で出来ることには限界があるよ」と言い換えても差しつかえないでしょう。ですが、「計算機で出来ることの限界」=「人間の知性/理性の限界」であるかどうかは自明な問題ではありません(難しいから議論の対象にはしません:-))。

まー、いずれにしても、ゲーデルの不完全性定理は、計算機やプログラミングと無関係ではありません。ゲーデルが展開した論法は、計算機/プログラミングに馴染<なじ>みがある人には十分に理解可能です。

そこで、プログラミングの諸概念を使って、ゲーデルの不完全性定理の変種(バリアント)を示してみます。この変種は、道具立てはオリジナルと違いますが、背後にある考え方と基本的メカニズムはオリジナルと同じです。

●ゲーデルが示したこと

ゲーデルの歴史的論文は、"On Formally Undecidable Propositions of Principia Mathematica and Related Systems"(原文はドイツ語;1930年受理、1931年出版)というタイトルです。"Principia Mathematica and Related Systems"とは、要するに(形式的な)論理体系のことです。論理体系のなかに、formal(形式的、機械的)には真偽が決定できない(Undecidableな)命題(Propositions)があるぜ、ってことね。

以下でしばしば登場する「形式的」(formal, formally)って言葉は、「記号の機械的操作に基づく」って意味だと理解してください。だから、形式的な論理体系とは、命題(言明、主張)が記号で表現されていて、推論はその記号を機械的に操作して進めるようなシステムですね。形式的な体系は、コンピュータ上に実装できます。言葉を換えれば、コンピュータ上に実装できるような記号計算の体系を、形式的体系と呼んでいるってことです。

“形式的な論理体系”における命題(記号的表現)とは、例えば、「∀x.(x2 = 1 → x = 1)」、「¬∃x.(x2 < 0)」とか;それぞれ「どんなxでも、xの自乗が1ならばxは1である」、「xの自乗が負になるようなxは存在しない」って意味です。いま、変数xは整数の範囲で考えるとしています。

上の例のように、我々が日常自然言語で述べた整数に関する命題は、記号的な表現に翻訳できます。そして、それらの命題には真偽が定まっているでしょう。もちろん、命題に曖昧さが残らないように十分な取り決めをします。例えば、「x2 = 1 → x = 1」は、xが自然数(負ではない)なら真ですが、-1を考えると真ではありません。変数が走る領域もシッカリと決めないといけませんね。そもそも、「ならば」(記号表現では→)の解釈とかもハッキリさせておかないと、「1を自乗すると間違いなく1なんだから、これは真じゃん」とかイチャモンがつきます。(「ならば」「任意のx(記号的に∀x)」の通常の解釈では、自乗して1だが、それ自身は1ではない数があれば、「∀x.(x2 = 1 → x = 1)」は偽です。)

命題の記号的な表現、その解釈などを曖昧さなく“もの凄くキッチリと”決めれば、どの命題も真偽が決まるだろうと期待されます。その内容が難し過ぎると「真偽が決まる」も怪しい気がするので、内容的には整数とその加減乗除くらいに制限しましょう。“その程度”の命題を算術的的命題と呼びます。

算術的な命題の真偽を実際に確認するには、推論を重ねて証明するか、その否定を証明して反証(証明による反駁<はんばく>)するかです。反例を構成して反駁することも否定の証明(反証)の一種です。これは、別に算術的命題に限らなくて、論理的な命題を論理的に示すときの一般的な手順ですね。

ゲーデル以前には、多くの人が、真な命題はいずれは証明されるだろう(そして、偽な命題はいずれは反証されるだろう)と期待していました。証明や反証ができてない命題があるのは、我々の努力や能力が足りないせいであり、「いつか証明/反証されるはず」と考えていたわけです。しかし、算術的命題のなかにも、証明も反証もできないものが存在することをゲーデルは示したのです。

●不完全性定理の兄弟 -- 停止問題

ゲーデルが示した決定不可能な命題は、原理的に証明も反証もできないもので、努力や能力とは何の関係もありません。証明(反証も含む)は、ルールにしたがった手続きであり、機械的な行為です。ゲーデルの結果は、機械的行為では真偽判定が出来ない、と言っています。

真偽判定に限らず、機械的手続きでは出来ないことは色々あります。機械的手続きで計算できない関数、機械的手続きでは列挙できない集合なども存在します。「機械的手続きでは出来ないことがある」という事態を総称して、ここではゲーデル的現象と呼びましょう。

コンピュータに関連したゲーデル的現象があります。「停止問題の決定不可能性」はそのひとつで、プログラムが停止するか(無限に走り続けないか)どうかを決定する手段が原理的に存在しないことを意味します。

「停止問題の決定不可能性」は、「ゲーデルの不完全性定理」と近い、というか兄弟のようなものです。このシリーズでは最初に「停止問題の決定不可能性」を紹介し、ほぼ同様な議論で「ゲーデルの(第一)不完全性定理」を示す予定です。

●JavaScript使うんだもんね

ゲーデルの不完全性定理では、機械的定理証明系の概念(証明可能性の定義)が必要ですが、停止問題(の決定不可能性)は、コンピュータとプログラミングの基礎知識だけで、問題なく完全に理解可能です。逆に、停止問題を理解することを目標として、“基礎知識”を習得するのはよい考えだと思います。その“基礎知識”には次が含まれます。

  • プログラム内蔵方式(コードとデータの均質性)
  • 仮想機械方式とバイトコード
  • ソースコード、目的コード、コンパイラ
  • 計算現象の観察、現象に関する言明、法則

停止問題が理解できれば、細部はともかくとして、ゲーデルの不完全性定理の実質的内容をつかみ取ることができるはずです。

最後に、冒頭で「『プログラマのためのJavaScript』の番外シリーズ」と言った理由をあかしておきます。停止問題と不完全性定理の説明にJavaScriptを使うからです。このような説明に、JavaScriptはけっこう向いているようです。

●関連する記事(参考)

僕がなんでこんなことを書く気になったかは、次の記事を見てください。

僕のネタモト(情報源)もこれに書いてあります。ただし、今後「発端編」記事を前提にすることはありません。

形式的体系に慣れるには、次の記事が参考になるかもしれません。

自分で言うのもなんですが、上記記事は形式的体系への入門として割とよくできていると思います。

hengsuhengsu 2006/01/04 13:02 偶然ですが、不完全性定理とプログラミングに関する本を読んでいるので、期待しています。ご参考までに、今読んでいる本を紹介します:G.J.チャイティン「数学の限界」「知の限界(The Unknownable)」。チューリングの方針に沿って、S式で証明しています。勿論、更に先を行っているので、ご興味があると思います。

m-hiyamam-hiyama 2006/01/05 09:49 hengsuさん、こんにちは。
チャイティンはS式を使っているのですか。そういえば、チャイティンの講演集をLisperの黒川さんが翻訳してましたね。
チャイティンはペンローズには同意しないようですが、「知性=構成的アルゴリズム」派なんでしょうか? -- あっ、この議論はしないと言ったのだった(苦笑)。

no-nameno-name 2006/01/06 11:13 初めて書き込ませていただきます。
ゲーデルについては、LISP には長い伝統があるようです。
http://www.iba.k.u-tokyo.ac.jp/~yabuki/tip/lisp/why_lisp.html

また、LISPERは、JavaScriptをLISPの近縁とみなしています。
http://d.hatena.ne.jp/brazil/20050915/1126717649

私自身、Schemeを学んだとき
「JavaScriptは、Schemeからリスト処理を取り除き、C風の文法と
プロトタイプを導入したものなんだなあ」と感じました。

では、今後の展開を楽しみにさせていただきます。

m-hiyamam-hiyama 2006/01/06 11:37 no-nameさん、こんにちは。情報ありがとうございます。
> ゲーデルについては、LISP には長い伝統があるようです。
レイフィケーションやメタプログラミングが容易ですから、自己言及/自己適用を分析しやすいのでしょうね。
> JavaScriptは、Schemeからリスト処理を取り除き、[snip]
そうですね、http://d.hatena.ne.jp/m-hiyama/20050830/1125393993 の「今回のまとめ(+雑感)」という所で、同じような感想を書いたことがあります :-)

それと、hengsuさんご指摘の「*の限界」本も、黒川さんが翻訳者なんですね、知りませんでした。

bonotakebonotake 2008/09/10 07:17 全くどうでもいいところの蒸し返しなのですが、
> Godel、’o’の上に点々が付いてる
「oの上に点々」は oe と書いてもいいことになってます。(というか、元々はそっちの方が正しい?)僕のドイツ人の友達も、英語でメールくれるときは自分の名前にあるのを oe と書いてます。
あるいは、”& o uml;” (スペースは抜かす)とかけば、HTMLで表記できます。はてなでもかけますよ。

「oの上に点々」と書くよりは楽チンだと思うので、ご参考まで。

m-hiyamam-hiyama 2008/09/10 08:58 bonotakeさん、
ö -- なるほど。
ご教示ありがとうございます。

西川くん西川くん 2010/05/13 07:05 僕は、法学部出身(しかも3流私立大学)なので、数学や記号論、論理学などは全く疎いのですが、以前、ダグラス・R・ホフスタッターの「ゲーデル、エッシャー、バッハ」(副題:あるいは不思議の環)という本を読んでみた事があります。今後、「不完全定理」を理解するために数学を勉強したいのですが、どの程度の基礎知識が必要でしょうか?(最低、高校数学くらいは?)

m-hiyamam-hiyama 2010/05/13 11:01 西川くんさん、
ウーム、これは大変難しい質問ですね。ちょっと考えさせてください。

西川くん西川くん 2010/05/13 13:14 ふと、想い出したのですが「不完全性定理」って「プログラムの無限ループの様に、言葉が、あるいは言葉で定義するということがメビウスの輪のごとく永久ループしてしまうということですか?それって「生命」の持つ「エントロピーの法則」と関係あるんですか?あるいはマルクスのいう「社会の下部(物質)構造が社会の上部(意識)構造を決定する」ということとのループ構造(つまり鶏が先か卵が先か?)ということと関係あるんですか?

西川くん西川くん 2010/05/13 16:31 どうも分けのわからんコメントですいませんでした。まぁ〜要するに「脳が脳そのものを意識するという自己言及性の持つ無限ループ的不可解性」とでも理解しときます。ありがとうございました。

m-hiyamam-hiyama 2010/05/15 18:35 西川くんさん、
だいぶ時間がたってしまいましたが、僕がお答えできることを記しておきます。

> ウーム、これは大変難しい質問ですね。ちょっと考えさせてください。

と僕が言った質問とは、

> 今後、「不完全定理」を理解するために数学を勉強したいのですが、どの程度の基礎知識が必要でしょうか?

コレ↑です。僕自身、系統的に勉強したわけではないし、何か1冊の教科書をシッカリ読んだ経験もありません。
なので、「この教科書を読みなさい」みたいなアドバイスができないのです。
竹内外史や前原昭二のような世界的大家の著作なら、内容的に間違いはありませんが、読みやすいかどうかは別問題です。
僕が普段参照している本は小野寛晰・著『情報科学における論理』ですが、ハンドブックとしてはコレ便利なんですが、自習に向くかどうかは疑問です。
戸田山和久・著『論理学をつくる』は自習向けに評判がいいようです。でも、向き不向きがあるでしょう。


以下に、老婆心でご注意をしておきます。

> 「不完全性定理」って「プログラムの無限ループの様に、言葉が、あるいは言葉で定義するということがメビウスの輪のごとく永久ループしてしまうということですか?
> それって「生命」の持つ「エントロピーの法則」と関係あるんですか?
> あるいはマルクスのいう「社会の下部(物質)構造が社会の上部(意識)構造を決定する」ということとのループ構造(つまり鶏が先か卵が先か?)ということと関係あるんですか?
> まぁ〜要するに「脳が脳そのものを意識するという自己言及性の持つ無限ループ的不可解性」とでも理解しときます。

「不完全性定理」は論理学(ロジック)の定理です。論理学のなかで、論理的構造に関するある特定の主張をしており、論理学の技術と文脈において正確な解釈が存在します。それ以外の分野、たとえばプログラミングの現象のなかで解釈することもできます。それは、正確な翻訳(構文論と意味論の変換機構)があるからです。

メビウスの輪(それ自体は幾何学的に正確に定義できます)とどう関係するかは、論理的な主張と幾何学的な主張の翻訳を自分で定義するか、既にある(もしあれば)翻訳を指定しないと何も答えられません。生命との関係も、マルクスとの関係も、脳との関係も同様です。
問を定式化する枠組みがないと、問に対する答えの妥当性の判断ができません。

「不完全性定理」を理解するとは、論理学の技術を(かなりヘビーに)使った定理の証明を追いかける事なので、アナロジーも思弁も哲学も不要です。アナロジーや思弁や哲学をいくら動員しても、論理学の定理であるとところの「不完全性定理」を理解することは絶対にできません。

掛け算九九を覚えてなくて、繰り上がり筆算のトレーニングも全くしたことがない人達が「掛け算の本質とはなんであるか?」とかの問を熱心に議論していたらコッケイでしょう。

論理計算もある種の計算なので、掛け算九九の暗唱や繰り上がりの練習と同様にトレーニングでしか習得できません。それだけは確かです。

http://d.hatena.ne.jp/m-hiyama/20081020/1224461181 とかでも同じ注意を書いています。

m-hiyamam-hiyama 2010/05/17 08:44 ちょっと補足。

typo修正引用> アナロジーや思弁や哲学をいくら動員しても、論理学の定理であるところの「不完全性定理」を理解することは絶対にできません。

アナロジーや思弁や哲学を動員すればするほど、誤解、錯覚、妄想などが積み重なるばかりだと思うんですが、一方で、そのような誤解・錯覚・妄想はある種の娯楽となり得るので、一概に否定はしません。ただし、その「娯楽」は「理解」とは別物なので、区別すべきだとは言えます。娯楽を求めているのか、理解を求めているのかで、アドバイスはまったく違ったものとなるでしょう。

竹内、前原、小野、戸田山といった著者の名前を出したのは、「理解」を求めているという前提です。