プログラマのための「ゲーデルの不完全性定理」(2)：速攻速習編

予定を変更して、“ご用とお急ぎ”があるかた向けに、「停止問題＋不完全性定理チョビット」に関して、1回で完結する説明をします。ですから、忙しい方は、「あとで読む」ってタグでこのエントリーを単品ブックマークするといいですよ :-)。

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

実は、このエントリーで述べる速攻速習に向いた説明は、最初に思い付いたものの、しばらく考えてから却下したアイディアです。が、初回（兼ハブエントリー）が多少は注目されたようなので、「数回の続きものを順番に読むのは耐えられん！」という要望にも応えようか、と気が変わりました。実際に要望があったわけじゃないけど、（いろんなリンクから来る）多くの人の眼に触れれば、そう思う人がいるのも当然だと推測するので。

僕が速攻速習方式をなぜ一旦は却下したかは、次回エントリーまたはキマイラ・サイトの記事で説明します、たぶん。
今回の内容：

JavaScriptに関するお約束など
「プログラムが引数に対して止まる」ということ：停止問題
関数willStop 登場！
この停止問題を考えてみよう
mysteryの停止問題はミステリー
なにかが間違っている
ゲーデルの不完全性定理への（ほんの少し）展望

前の記事ハブエントリー＋総論

●JavaScriptに関するお約束など

これから、JavaScriptの関数で、文字列（String型）引数を1つだけ持つものを考えます、戻り値はなんでもかまいません。さらに、取り扱いの便宜上、引数変数の名前はargに固定します（これ、お約束ね）。そんな関数の例をいくつか出しましょう。



function length(arg) {

 return arg.length;

}
function forever(arg) {

 while(true);

}
function sumUpToLength(arg) {

 var result = 0;

 for (var i = 1; i <= arg.length; i++) {

  result += i;

 }

 alert(result);

}
function replaceAsterToX(arg) {

 var s = arg.replace("*", "X");

 return s;

}

引数が1つでしかも名前がargと決まっているので、関数定義本体だけあれば、次のようにして関数を作り出せます。



 var length = new Function("arg", "return arg.length;");

少しでも楽なように、上のコードを関数にしておきましょう。



function makeFunc(def) {

 return new Function("arg", def);

}

ネーミング・コンベンションとして、関数定義が入った文字列にhogeDef、それからmakeFuncして出来た関数にhogeFuncという名前を付けることにします。例えば：



 var lengthDef = "return arg.length;";

 var lengthFunc = makeFunc(lengthDef);

●「プログラムが引数に対して止まる」ということ：停止問題

以下でプログラムと言ったら、“文字列型引数を1つ持つ関数の定義本体のことだ”とします。「あるプログラムprogDefが引数someArgに対して止まる」とは、そのプログラム（関数の定義本体）から作った関数progFuncにsomeArgを渡した呼び出しが、有限時間内に正常に戻ってくることです。



 var progDef = "/* プログラムのソース */ ...";

 var progFunc = makeFunc(progDef);

 progFunc(someArg); // この呼び出しが戻ってくるか？

 // ここに到着すれば、

 // progDefが引数someArgに対して止まると言える。

今後、progDefに構文エラーはないと仮定しましょう（構文エラーのケースを考えてもつまらない）。また、progDef内から例外による脱出はないものとします。

さて、（構文エラーがない）プログラムに特定の引数を与えたとき止まる（停止する）かどうかを問うのが停止問題です。次の例を考えてみてください。



 var progDef = "var n = Number(arg); for (var i = 0; i != n; i++);"

 var progFunc = makeFunc(progDef);

 var argEx1 = "10";

 var argEx2 =  "0";

 var argEx3 = "-1";

この状況で、progFunc(argEx1)、progFunc(argEx2)、progFunc(argEx3)などの呼び出しが停止するか？さー、どうでしょう。この例に限って言えば、progFunc(argEx1)とprogFunc(argEx2)は停止して、progFunc(argEx3)は停止しません（無限に走り続ける）、そのことは、ソースコードであるprogDefをよく眺めればわかりますね。

●関数willStop 登場！

ここで、驚異の関数willStopの登場です。willStopは、2引数の関数で、willStop(progDef, someArg)として呼び出すと、プログラムprogDefがsomeArgに対して止まるときにはtrue、止まらない（無限に走り続ける）ときにはfalseを返します。willStopは、実際にprogDef（から作った関数）を走らせるわけではなくて、ソースコード（の文字列）と引数値を解析して停止性を判断します。関数willStopを使えば、実際にプログラムを走らせることなく事前に、停止するか（あるいは無限走行するか）をチェックできます。素晴らしい！

ただし、willStopの使用には若干の注意が必要です。次のコードを見てください。



 var n = Number(arg);

 var ua = window.navigator.userAgent;

 if (ua.indexOf("Gecko") >= 0) n = -n;

 for (var i = 0; i != n; i++);

これは、引数argの値だけでなくて、大域的な環境からの値window.navigator.userAgentによって動作が変わるプログラムです。willStopは、willStop自身が実行されるときの大域環境を参照するので、他の異なる実行環境での停止性は判定できません。

プログラム自体とargの値だけで挙動が完全に決定されるプログラムなら、willStopの判定結果は環境によらず通用します。

●この停止問題を考えてみよう

ここで次のコードを考えましょう。



var mysteryDef = "if (willStop(arg, arg)){while(true);}";

var stopOrNot = willStop(mysteryDef, mysteryDef);

alert(stopOrNot); // 何が表示されるでしょうか？

これを実行する前に、alertで表示される結果を予測しましょう。たった3行のプログラムですもの、簡単にわかりますよね。わかるはず…。

念のため再確認すると、willStop(mysteryDef, mysteryDef)が「trueを返すかfalseを返すか」は、次のコードが「有限時間で止まるか無限に走り続けるか」を忠実に反映します。



 var mysteryDef = "if (willStop(arg, arg)){while(true);}";

 var mysteryFunc = makeFunc(mysteryDef);

 mysteryFunc(mysteryDef); // この呼び出しが戻ってくるか？

 // ここに到着すれば、

 // mysteryDefが引数mysteryDefに対して止まると言える。

mysteryFuncをfunction宣言文で見やすく書けば次のようですね。



function mysteryFunc(arg) {

 if (willStop(arg, arg)) {

   while(true);

 }

}

そして、mysteryFunc(mysteryDef)という呼び出しが戻ってくるか、行ったきり（いつまでも戻らないか）、それが問題、大問題。

●mysteryの停止問題はミステリー

mysteryFunc(mysteryDef)は、止まるか止まらない（無限に走る）かのどちらかです。2つの場合しかありません。各場合で、関数mysteryFuncの内部動作を追いかけましょう。

・mysteryFunc(mysteryDef)が止まる場合

if (willStop(arg, arg)) {while(true);} のargにはmysteryDefが入るので、if文はif (willStop(mysteryDef, mysteryDef))となります。「willStop(mysteryDef, mysteryDef)がtrueを返すこと」と「mysteryFunc(mysteryDef)が止まること」は同じことでした。そして今まさに、mysteryFunc(mysteryDef)が止まる場合を考えているので、if文の条件はtrueとなります。

ifの条件がtrueなので、while(true);に制御が移ります。そして、無限ループに陥＜おちい＞り、関数mysteryFuncから戻ることは二度とできませんね。

んっ？アッ、アレーーー!? いま、mysteryFunc(mysteryDef)が止まる場合を考えているのでしたよね。「関数mysteryFuncから戻ることは二度とできません」って、それじゃ止まんねーじゃん!? それでいいんか。止まる場合は止まらない、って、それでいいんかよー(叫)。

・mysteryFunc(mysteryDef)が止まらない場合

気を取り直して、mysteryFunc(mysteryDef)が止まらない場合を考えましょう。さっきの止まる場合はたぶん仮定がまずかった、ってことで。こっちなら大丈夫かと。

……… （みなさん、考えましょうね）
：
：
…… 止まらない場合は止まる、って、それでいいんかよー(叫)。

●なにかが間違っている

mysteryFunc(mysteryDef)という呼び出しが止まるかどうか、この停止問題の考察はミステリアスな結果になってしまいました。もう一度要点を書いておけば：

mysteryFunc(mysteryDef)は、“止まるか止まらないか”のどちらかだ。
止まると仮定して、関数mysteryFuncのソースコード（mysteryDef）に基づいて動作を追跡すれば、明らかに止まらない。
止まらないと仮定して、関数mysteryFuncのソースコード（mysteryDef）に基づいて動作を追跡すれば、明らかに止まる。

1番目の判断を疑うことは意義のある行為ですが、いまここでそれをやると収拾がつかなくなるので、「“止まるか止まらないか”のどちらかだ」という発想は正しいとしましょう。2番目と3番目の追跡作業も間違いを犯しているとは考えにくいですね。

「ソースコードレビューと机上実行で結論が出ないなら、ほんとに実行してみよう」と誰かが言いそうです。これはいい提案です。が、関数mysteryFunc内で関数willStopを呼んでいるので、関数willStopのソース（willstop.jsでしょう）が必要になります。どこからダウンロードできるでしょうか？えっ、僕は知りませんよ。

今回は「速攻速習編」ですから、あまり引っ張らないでタネ明かししましょう。willstop.jsはどこからもダウンロードできません。つーか、関数willStopは存在しません。まだ誰も書いてないから存在しないのではなくて、誰も書けないから存在しないのです。

ミステリアス（パラドキシカル）な結果になってしまったのは、途中の考え方、その過程が間違っているのではなくて、ありもしないwillStop関数を「在る」として話をはじめてしまったせいです。無いんですよ、そんなもの。willStopは誰も（全能の神様でも）作れません。

●ゲーデルの不完全性定理への（ほんの少し）展望

このエントリーは、1回読み切り可能としたいので、ごく手短に、停止問題とゲーデルの不完全性定理との関係に触れておきます。

関数willStopが実現不可能なのは、要求が強すぎる（高望み）のせいです。その要求には次が含まれます：

willStopの第1引数には、任意のプログラム（を表現する文字列）を入れてよい。
willStopは必ずtrueかfalseを返す。

これらの要求を緩和（弱く）すれば、willStopが実現できることもあります。扱えるプログラム（第1引数への入力）を制限してしまえば、その範囲内での停止性判定は可能になりえます。また、willStop自体が無限に走る（戻らない）ことも許すなら、「止まったときは、正しくtrueかfaseを返す」という関数を実現できます。

ゲーデルの不完全性定理では、willStop(progDef, someArg)の代わりにcanProve(predDef, someArg)を考えます。この意味は：

1引数で真偽値（trueかfalse）を返す関数を述語（predicate）と呼ぶ。
predDefは、述語の関数定義本体（を表す文字列）である。
canProve(predDef, someArg)は、predDefのargをsomeArgで置換した定義（あくまで文字列！）が、ある機械的定理証明系で証明可能であればtrue、反証可能（否定が証明可能）であればfalseを返す。

この状況で、次のコードを考えます。



 var cannotProveDef = 

  "if (canProve(arg, arg)) {return false;} else {return true;}";

 var provableOrNot = canProve(cannotProveDef, cannotProveDef);

 alert(provableOrNot);

停止問題と同じ議論でパラドックス（正確には矛盾）が生じます。しかし、停止問題とは異なり、「だからcanProveなんてあり得ない」とは言えません。なぜなら、ゲーデルは非常によくできたcanProveをホントに作ってしまったからです。

ただし！ゲーデルは嘘つきでもホラ吹きでもないので、「canProveは、どんな述語定義に対しても必ずtrueかfalseを返す」とは言ってません。確実な前提と確実な推論から導かれる結果は、ゲーデルが定義したcanProve関数（に相当するアルゴリズム）は完全ではないということです。「完全ではない」の意味は、canProve(predDef, someArg)がtrueもfalseも返さない事態が起こりえるということです。これは、証明可能でも反証可能でもない命題の存在を示します。

では、関数canProve（の実装に使われている証明アルゴリズム）はどの程度に“よくできたもの”なのでしょうか。多くの人が、「アルゴリズムとして記述可能な人間の知的行為」は事実上canProveで尽きていると考えています。別言すれば、人間もcanProve以上のことは出来ないことになります。ただし、「人間の知的行為はアルゴリズムとして記述可能か」という問題は残ります。ですから、「アルゴリズム的に行為する限り、人間もcanProve以上のことは出来ない」と言うのがより適切でしょう。

これで、1回読み切り速攻速習編は終わりです。実際のJavaScriptコードを使っているので、雰囲気だけのオシャベリよりは、ゲーデル的現象のメカニズムを伝えられたかな、と思います（そう期待します）。ゲーデルが実際に使った方法や、論理学の基礎知識に興味があるかたは、続く回もフォローしてみてください。