このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

プログラマのための「ゲーデルの不完全性定理」(3):自己適用からゲーデル化へ

前回(第2回)、1回でも完結する形で、停止問題と不完全性定理のオーバービューを与えました。これはこれで分かりやすく全体像を見渡せるから書いて良かったな、と思っています。がしかし、前回のような説明に、僕自身は不満も感じるんですよね。そこらへんの事情を述べようと思ったのですが…

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

  1. 著述スタイルを変更します、たぶん
  2. 自己適用/自己言及
  3. 符号化とウロボロス
  4. メタレベルも取り込むこと:レイフィケーション
  5. ゲーデル符号化、ゲーデル
  6. また自己批判

●著述スタイルを変更します、たぶん

前回(第2回)は、実は当初の予定から外れたエントリーでした。なぜに予定外だったかを説明するエントリーはなおさらに予定外となります。そんな展開では、当初の予定なんか守れっこないなー、… まー、そもそも予定を守る必然性もないし。

そこで、説明としての筋書きはあまり気にせず、日記風(?)のスタイル(思い付きと勢い重視)で書き続けようと思います。それでも、僕が強調したい点は決まっているので、回を重ねれば(多少の脱線はあっても)言いたいことはいずれは書くことになるでしょう。

というわけで、今日のお題は「自己適用」となりました。これは、自然言語による「ゲーデル不完全性定理」の解説を僕が嫌っている理由、LispのS式を使った定式化や僕自身の前回の説明にも不満である理由を明らかにするための準備なのです。(けど、単品でも意味あるかなー、と。)

●自己適用/自己言及

ゲーデル的現象には、自己適用/自己言及が付きまといます。そこで、自己適用/自己言及について、プログラミング寄りの観点から説明します。

多くのプログラミング言語/実行環境が自己適用のメカニズムを潜在的あるいはに明示的に持っています。プログラムPが引数(パラメータ)を1つ持つとして、P自身を実引数として渡した形 P(P) 自己適用です。とはいえ、通常、Pの引数としてプログラムをそのまま渡すことは許されない(あるいはうまく解釈できない)ので、何らかの細工が必要です。

その細工のひとつに、プログラムPをデータ化したDを引数に使う、という方法があります。つまり、自己適用P(P)といいながら、実のところはP(D)を考えるのです。PからDを作る操作を符号化(コード化、coding、encoding)と呼びます。Dが所属するデータ領域は符号空間と呼ぶことにしましょう。そして、Pの符号化をcode(P)と書くことにします。この記法では、D = code(P) ですから、自己適用P(P)の正体はP(code(P))となります。

前回のJavaScriptを使った例では、次のプログラムテキスト:


if (willStop(arg, arg)) {
while (true);
}
に対して、文字列"if (willStop(arg, arg)){while (true);}"が対応する符号になっていました。このケースでは、符号化はプログラムテキストの文字列化であり、符号空間は文字列全体の領域だったのです。

文字列はJavaScriptのデータなので、プログラム(関数と思ってよい)に文字列を渡すことは何の問題もありません。こうして、自己適用が符号化 -- プログラムテキストの文字列化 -- を経由して実現できたわけですね。次のmysteryFunc(mysteryDef)が自己適用です。


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

なお、自己言及とは、プログラム(関数)が真偽値を返すときの自己適用のことです。引数を1つ持ち真偽値を返す関数(述語と呼ぶのでした)は、自然言語では“何かに対する記述/主張”に対応します。例えば、「xは嘘つきです」はxに対する記述/主張です。この文のxに自分自身(私)を代入すると「私は嘘つきです」となり、有名な嘘つきのパラドックスが生じます。(嘘つきのパラドックにも、いずれは触れるつもりですが、とりあえず今日は「そんなのもあるよ」ってことで深入りしません。)

●符号化とウロボロス

さて、「プログラムを符号化して、その符号が再びプログラムで扱える」という状況を絵に描いてみます(汚い手描きの図ですが(苦笑))。

JavaScriptの場合では、符号空間はすべての文字列からなる領域です。符号化は“プログラムテキストの文字列化”ですね。一般には、符号空間はプログラムテキストとは別物と考えられます。しかしJavaScriptでは、符号=文字列に対してリテラル表現(二重引用符で括った形)が存在します。図で「埋め込み」と書いてあるのは、文字列データを文字列リテラルとして表現することにより、符号空間をプログラムテキスト(の領域、空間)の内部に取り込むことです。

符号化と埋め込みにより、プログラムテキスト(構文的な表現)の全体が、その内部にそっくり写像されます。この操作はいくらでも繰り返せるので、自分自身を自分自身のなかに取り込む構図が無限に続く、合わせ鏡のような状況となります。

ウルボロスという自分の尾を自分で飲み込もうとしている蛇、その蛇が自分自身をスッカリおなかに収めてしまったようなものです。でも、自分自身が自分のおなかに入っているって、それって … あー、考えると眠れない。大丈夫、考えなければ眠れます。

●メタレベルも取り込むこと:レイフィケーション

先走りぎみに、もうちょっと進んでおきます。

述語とは、“何かに対する記述/主張”だと言いました。「xは嘘つきです」はプログラムで表現しにくいですが、「xは0以上100未満(の整数)です」なら簡単ですね。0 <= x && x < 100と書けます。今の例は、対象物を整数とした記述/主張となります。

プログラミングシステム(言語+実行系)では、対象とするデータに対して記述/主張を行うことができます。もし、前節のようにプログラムの符号化と符号空間の埋め込みがあるなら、「対象+記述」を含む全体を自分自身のなかに写像できますね(次の図)。

図で「自己符号化」というのは「プログラムの符号化と符号空間の埋め込み」の組み合わせのことです。

さて、我々はプログラミングシステム(特に、そのなかでのデータに対する記述)を外から眺めて記述/主張を行えます。これは、我々・人間がプログラミングシステムに対して行う記述/主張です。例えば、「0 <= x && x < 100というコードを、x = 20 という状況で走らせたら値はtrueだ」とか。この記述/主張は、プログラミングシステムの内部に在るもの(プログラミング言語で書かれたテキスト)ではなくて、プログラミングシステムの外部(人間と現実の世界)に在ります。

言い方を変えれば、「0 <= x && x < 100というコードを、x = 20 という状況で走らせたら値はtrueだ」は、メタな言明(記述/主張)です。ところが、メタな言明の対象であるプログラミングシステムは、自己符号化により、プログラミングシステムのデータ表現の内部に(自分のおなかに飲み込まれた蛇のごとく)そっくりそのまま埋め込まれています。ですから、メタ言明をプログラミングシステム内部の表現に写像することも可能になるのです。

前回の約束事に従って、関数の引数名をargと決めてかかるなら、「0 <= x && x < 100というコードを、x = 20 という状況で走らせたら値はtrueだ」は、次のプログラム(関数)で表現できます。


function metaStatement() {
var pred = makeFunc("return (0 <= arg && arg < 100);");
return (pred(20) == true);
}

このように、メタ言明を対象システム内の言明として表現することをレイフィケーションと呼びます。レイフィケーションとは、メタレベルにある言葉・表現を、対象レベルに引きずり落とすことです。先の図では、点線の矢印がレイフィケーションですね。

ゲーデル符号化、ゲーデル

狭い意味でのゲーデル符号化は、自然数(非負の整数)を符号空間として、対象システム(形式的体系)を符号化する操作です。そうすると、対象システムに対するメタ言明は、レイフィケーションにより自然数に対する言明(これは算術的命題)に落ちます。自然数は、もっとも初等的でハッキリとした対象なので、非常に厳密な議論ができます。つまりは、幾分うさんくさげなメタ言明に、これ以上は望めない明晰性を与えることができるわけです。

レイフィケーション(メタ言明の算術命題への写像)も含めてゲーデル符号化と呼ぶこともあります。また、符号化とレイフィケーションの手順をハッキリ定めて、合理的な自己言及の仕掛けを作ること(広義のゲーデル符号化)をゲーデル(算術化)といいます。

符号空間を自然数以外にとってもゲーデル化は可能です。Lisper達は、符号空間をS式の領域として、クォーティング(「'」を付ける)で自己符号化を達成します。そして、自然言語記号論理の式をS式(これはLispのプログラムテキストでもありデータでもある)に翻訳してレイフィケーションを行うのですね。前回の僕の説明は、“プログラムテキストの文字列化”が自己符号化で、自然言語記号論理の式をJavaScriptコードに書き下してレイファイ(reify;動詞)しました。

●また自己批判

ゲーデル不完全性定理を納得するには、ゲーデル符号化、ゲーデル化(ゲーデル符号化に伴うレイフィケーション)を具体的にフォローすべきだ、というのが僕の見解なのですが、それに反して、今回もなんか一般論/抽象論だったようです。しかし、ゲーデル的現象の背後にある状況を俯瞰<ふかん>する意味はあったかもしれません。