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

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

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

［参照用 記事］

あっ、言い忘れていた：なんで停止性なのか？

雑記／備忘

たけをさん http://d.hatena.ne.jp/bonotake/20090219/1235053277 ：

お絵描き（ラムダ計算）の話がなんで計算可能性の話につながるの？

... [snip]

大きく外れてはいないと思ってるんですが。

まー気まぐれみたいなものです。が、

コード（関数）とデータ（値）が同じ整数/バイナリにエンコードできるようになって、その2つが一緒くたに扱えるようになったからパラドックスも発生するようになったってことですかね

当たり。そのとおりです。

もうちょっと説明を加えます。「せっかくだから停止性の問題を話そう」と思った流れは以下のごとくです。

内容：

  1. 関数そのものと関数コード
  2. 関数の自己適用／自己言及
  3. 自己言及のパラドックス
  4. 関数コードがデータとみなせるなら、どんなデータでもOK
  5. 面白いから言ってみただけ、かもね

関数そのものと関数コード

自己適用／自己言及が出てくるまでの筋書きを説明したいのですが、まずは、計算可能関数の全体と、コンパイルした関数コードの対応関係を確認しておきます。

Nは自然数全体の集合、つまり N = {0, 1, 2, ... } とします（いちいち太字にしませんが、通常は太くNと書かれます。）べきNNは、NからNへの関数の全体と考えていいのですが、ここでは「任意の関数」ではなくて「計算可能関数だけ」を考えます。さらに、NN はデータとみなしたい。そこで、NN はコンパイルされたバイナリ関数コードの集合だと考えることにします。以下、バイナリコード＝ビット列は自然数と適宜同一視します。ヨロシク。

関数f:N→N に対して、f^() ∈NN となります。念のため、大きなラムダ式を使った計算をしてみると、f^ = Λ(f) = Λ<x|f(x)> = <|λx.f(x)>、f^() = <|λx.f(x)>() = λx.f(x) です。つまり、セミフォーマルな小さなラムダ式λx.f(x)は、fそのものじゃなくて、NNの要素（関数コード）を表しているとみなすべきなのです。E(f^(), a) = E(λx.f(x), a) = (λx.f(x))・a = f(a) ですね、「・（ドット）」はEの中置演算子記法です。

換言すれば、NNの要素とは、計算可能関数fにラムダオペレータΛ（あるいはハット^、あるいはカリー化、あるいは抽象化）を適用したデータなのです。我々の文脈では、「ｆをコンパイルしたバイナリ関数コード」とは、f^()のことを指しています。ラムダ抽象化＝カリー化＝理念的コンパイルです。

バイナリ関数コードφ∈NNが与えられると、f(x) = E(φ, x) としてfを再現できます。このことは、N→N という関数とNNのデータの間に1：1の対応があることを意味します。ただし、この1：1対応に関しては、かなり精密な議論をしないと誤解や混乱が生じます*1。できればこの点を別に説明したいのですが、今日はしません。

「N→N という関数の全体」（計算可能関数しか考えてないので、プログラムの全体と言っても同じ）は、この世界（fが所属する世界）を外から眺めないと把握できない集合ですが、NNはこの世界のなかに個物として存在するデータ領域です。

世界の外からしか把握できないはずの集合ComputableFunc(N, N)が、この世界のなかにあるデータ領域NNと同型になっている根拠は、大文字ラムダΛが「関数（働き）←→関数コード（ある種のデータ）」の対応「f←→f^()」を与えているからで、その様子を端的に表現しているのが、基本等式

  • f(x) = E(f^(), x)

です。そしてもちろん、ComputableFunc(N, N) → NN という対応は、スノーグローブ現象によるミニチュア化の一例です*2。

関数の自己適用／自己言及

ここで現実のコンピュータを眺めてみれば、関数コード（型がNNであるデータ*3）は、そのままただちにビット列データとみなせるので、NNからNへの埋め込みが存在します。それならいっそ NN⊆N とみなしてしまいましょう。すると実行エンジン（apply, eval, exec, engine、お好きに呼んでください） E:NN, N→N は、E:N, N→N とみなしてもいいことになります。

以上が、「実行可能形式もデータも所詮はビット列」の背景です。

さてそうなると、自己適用 f(f) の正確な定義ができるようになります。引数となるfのほうは、φ = f^() と置いた上で、f(f) とは実は f(φ) だと解釈します。すると、基本等式を使って f(φ) = E(f^(), φ) = E(φ, φ)。若干、不正確な表現ですが、

  • f(f) = E(φ, φ) = E(f^(), f^()) = f^()・f^()) = (λx.f(x))・(λx.f(x))

です。

つまり、「fが自分自身を引数にもらう」状況は、fのコンパイル済み関数コードφを使えば、同じビット列φをコード領域とデータ領域の両方に置いたうえで、実行エンジンEを走らせるだけのことです。合理的に定義されたE(φ, φ)の結果が、矛盾的とも言える自己適用 f(f) の結果とみなせます。

自己言及のパラドックス

自己適用を解釈する枠組みがせっかく出来たのですから、「自己言及のパラドックス」を扱わないのは、まったくもってもったいない。

あの関数 s(x)（このエントリー最後を参照）は、 与えられた引数xに対して、

  • x(x) が止まるなら私は止まらない、x(x) が止まらないなら私は止まる

と言ってます。つまり、xの自己適用の挙動x(x)をみて自分の挙動s(x)を決めているわけです。もしxが自分自身であるなら：

  • s(s) が止まるなら私は止まらない、s(s) が止まらないなら私は止まる

となります。しかし困ったことに、上の文がまさに s(s)（実際はE(σ, σ)）の定義そのものなので、s(s) の計算に s(s) が参照されることになります。これが無限再帰で止まらないならある意味“自然”ですが、goodの定義によれば、有限時間内に「s(s) が止まる」か「s(s) が止まらない」かのどちらかに決定します。そこから、

  • 「s(s) が止まる」なら「s(s)は止まらない」
  • 「s(s) が止まらない」なら「s(s)は止まる」

という矛盾が出ます。矛盾の原因は自己適用／自己言及そのものというより、自己適用の無限連鎖／無限後退を「goodの力で断ち切れる」と仮定したことです。そんなパワフルなgoodなんてあるわきゃないよ！ が事の顛末です。

関数コードがデータとみなせるなら、どんなデータでもOK

以上の論法のキモは、関数コードの集合NNがデータの集合Nに埋め込めることです。今回はデータの集合として自然数＝ビット列を取りました。しかし、関数コードがデータとみなせるなら、データの種類はなんだってかまいません。コンパイル結果がバイナリかどうかは何ら本質的なことではありません。

例えば、「関数コードが文字列データとみなせる」とか「関数コードが二分木リストとみなせる」とかでも、同じ手順で矛盾を導けます。とあるデータ領域をDとして、次が成り立つなら、同じ議論が出来るのです。

  1. f:D→D に対して、f^()∈DD が決まり、E(f^(), x) = f(x) 。ここで E:DD, D→D 。
  2. DD⊆Dとみなせる。より正確に言えば、j:DD→D という単射jが存在する*4。

データとして文字列を考えたケースが「プログラマのための『ゲーデルの不完全性定理』(2)：速攻速習編」にあります。併せてお読みください。

面白いから言ってみただけ、かもね

要するに、基本等式から f(f) = E(φ, φ) = E(f^(), f^()) が出てくるんだから、これを使って何か一席と思ったら、即座に「不可能性の証明」というネタが思い浮かんだってわけ。本来この話題は基本等式の応用というか寄り道なんですけど、好みのネタなのでしゃべってしまった、ってことです。

ちなみに、スライドの「我々は何を知りえないかを知りうる -- 不思議だ。」だけリッパな文字にしたのは僕の指示じゃないです。若い子が気を利かしたのでしょう。セミナー始まる直前に、あのスライドページを見て、これをオチにしようと決めたのも、まー気まぐれですね。


参考：

  • GOOD(f, a) = true -- 関数fに具体的な引数値aを渡すと計算が止まって値を返す
  • GOOD(f, a) = false -- 関数fに具体的な引数値aを渡すと、例外を起こすか計算が止まらないで、値は返さない
  • good(φ, a) = GOOD(f, a) ただし、φ = f^()



int s(any_number_or_any_bitcombination_t x)

{

 if (good(x, x)) {

  while(1) {

   ; // do nothing

  }

  return 0; // cannot reach

 } else {

  return 0;

 }

}

*1:例えば、関数と関数コードが1:1に対応するなら、2つの関数の外延的同値性が実効的に判定可能なように思えます。が、それは誤解です。

*2:ComputableFunc(N, N) は世界のなかにあるモノではなくて、世界の一部分（portion）です。それに対してNNは、世界のなかにあり世界を構成する基本要素（individual）です。

*3:この言い方も、誤解を与える可能性がありますね。N内で関数コードとみなせるビット列の全体をVとすると、NN⊆V ですが、NN＝V ではありません。

*4:実際には、単射jだけでなく、全射p:D→DDも存在して、pとjを結合してレトラクトになっていることまで要求します。レトラクト（レトラクション、EPペア）については、http://d.hatena.ne.jp/m-hiyama/searchdiary?word=%a5%ec%a5%c8%a5%e9%a5%af 参照。