エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

不完全性定理(4)

不完全性定理とはなにか (ブルーバックス)』の不完全性定理の証明とチューリング機械の停止問題の証明について考えると、チューリング機械の停止問題の証明ではチューリング機械が停止するかどうか判定できると仮定したのに対して、不完全性定理の証明ではどうなっているのか考えます。不完全性定理の証明をチューリング機械の停止問題の証明に合わせて書き直したいと思います。まだそれはできていないので、まずはチューリング機械の停止問題から考えます。

ここで書いたチューリング機械の停止問題の記事では、チューリング機械をプログラミング言語のメモリー上での状態として議論しようとしていましたが、本の流れに合わせる都合上そうなっていなかったので、これを直していきたいと思います。

チューリング機械の停止問題

チューリング機械を「無限にメモリーがあるコンピューターで動くwhileループがあるプログラミング言語(変数名、数値(自然数)、計算の途中の状態は無限個使うことができる)の式」と考えます。このプログラミング言語を「プログラミング言語ω」とします。「プログラミング言語ω」の式はメモリー上では一つの自然数になっているとします。この自然数を式のコードと呼ぶことにします。

プログラミング言語ω」の式  x のコードを  c(x) とします。コード  i の式を  e(i) とします。
 f(i, j) \equiv \begin{cases}
\{v = j; e(i)\} & (i : E \ のとき) \\
\bot & (i : E \ ではないとき)
\end{cases}
とおきます。ここで「 \equiv」は式が一致することを表します。「 a : E」は「 a」が式のコードであることを表します。式  \psi の値を  u(\psi) とします。「 \bot」は式の値が存在しない(有限時間で値を計算することができない)ことを表します。 \{v = \alpha; \psi\} は式  \psi の自由変数  v自然数または変数  \alpha で置き換えた式の値を値とする式を表します。

 t(i, j) \cong \begin{cases}
1 & (f(i, j) \not \cong \bot \ のとき) \\
0 & (f(i, j) \cong \bot \ のとき)
\end{cases}
が成り立つような式  t(i, j) が存在すると仮定します。「 \cong」は式の値が(値が存在しない場合も含めて)一致することを表します。加減乗除などの演算はその演算の結果を値とする式を表します。たとえば「2 + 3」という式の値は  5 です。

 t(i, j) が存在すると仮定すると
 d(i, j) \equiv \begin{cases}
f(i, j) + 1 & (t(i, j) \cong 1 \ のとき) \\
0 & (t(i, j) \cong 0 \ のとき)
\end{cases}
を定義することができます。

 d(i, j) は自由変数の  v がなくなっているので再び  v を導入することができます。 d' \equiv \{k = v; d(k, k)\} n \equiv c(d') とおくと
 \begin{eqnarray*}
f(n, n) & \cong & \{v = n; e(n)\} \\
 & \cong & \{v = n; e(c(d'))\} \\
 & \cong & \{v = n; d'\} \\
 & \cong & \{v = n; \{k = v; d(k, k)\}\} \\
 & \cong & d(n, n) \\
 & \cong & \begin{cases}
f(n, n) + 1 & (t(n, n) \cong 1 \ のとき) \\
0 & (t(n, n) \cong 0 \ のとき)
\end{cases}
\end{eqnarray*}
となります。これは
 f(n, n) \cong \begin{cases}
f(n, n) & (t(n, n) \cong 1 \ のとき) \\
\bot & (t(n, n) \cong 0 \ のとき)
\end{cases}
に矛盾します。

よって「無限にメモリーがあるコンピューターで動くwhileループがあるプログラミング言語の式に値があるかどうかを判定するような式は存在しない」ということが成り立ちます。

 f(i, j) の値を表にします。
 \begin{matrix}
f(1, 1) & f(1, 2) & \cdots & f(1, n) & \cdots \\
f(2, 1) & f(2, 2) & \cdots & f(2, n) & \cdots \\
\vdots & \vdots & \ddots & \vdots &  \\
f(n, 1) & f(n, 2) & \cdots & f(n, n) & \cdots \\
\vdots & \vdots &  & \vdots &  \\
\end{matrix}
この対角線の値をすべて変更したものが  d(i, j) です。 d(v, v) もこの表の中にあるのでそれを  f(n, v) とすると
 \begin{eqnarray*}
f(n, n) & \cong & d(n, n) \\
 & \cong & \begin{cases}
f(n, n) + 1 & (t(n, n) \cong 1 \ のとき) \\
0 & (t(n, n) \cong 0 \ のとき)
\end{cases}
\end{eqnarray*}
となって矛盾が生じます。