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

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

不完全性定理(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*}
となって矛盾が生じます。

不完全性定理(3)

不完全性定理とはなにか (ブルーバックス)』の不完全性定理の証明をプログラミング言語を使って書き直していきます。しかし、すべてプログラミング言語のようにはできないので、まずはデータをプログラミング言語の式のように表すことを考えます。

不完全性定理の証明

この本の流れに沿って書き直していきます。

【ステップ1】 すべての命題  f(i, v) の一覧表を作る。

この本では「1変数の命題  F(y) を網羅した一覧表を作る」だったのですが変更します。

命題や証明は(プログラミング言語の式のように構造を持った)「式」として表します。命題の式を論理式、証明の式を証明式と呼ぶことにします。無限個使うことができる変数名、数値はプログラミング言語のリストのように表します。構造の上位の要素が演算子のとき、その直下の要素は、有限個の決まった個数のその演算子の被演算子とします。構造の上位の要素が変数名を表す記号のとき、その直下の要素は、変数名の次の文字とします。変数名に使える文字は有限個とします。構造の上位の要素が数値を表す記号のとき、その直下の要素は、数値の次の文字とします。数値に使える文字は有限個とします。

式のある部分を考えると、その部分の最上位の要素の種類は有限個となります。その直下の要素は最大で演算子の被演算子の最大の個数となります。よって、式の「深さ」が有限とすると、式の個数は有限となります。

この式を長方形の表の形で表します。表の右方向には式の下位の要素、下の方向には被演算子を順に記入していくとします。演算子の被演算子が複数あるときは、2個目の被演算子以降は上位の要素は空白として表を作ることができます。下位の要素がないときも空白とします。これはプログラミング言語の式を表の形で表すような方法です。この表全体を文字列と考えて、その順序によって式に順序を導入することができます。たとえば、表の横方向の並びを1つの文字列と考え、それを縦方向にすべて連結した文字列を考えます(「次元」に関する辞書式順序の並び)。その文字列に辞書式順序を導入します。これによって式の「深さ」が決まった有限の値である式の全体は、有限全順序集合となります。これを式の「深さ」が小さいものから順に並べると、すべての式に番号をつけることができます。

逆に番号を指定すると、構造を再現することができます。

論理式、証明式と番号の対応を表すため、プログラミング言語の関数定義のような記法を導入します。プログラミング言語でできることだけをやっていって、全体をプログラミング言語で記述できるようにします。これを説明するため、プログラミング言語の関数のような関数を「言語関数」、その引数を「言語関数引数」と呼ぶことにします。

 i 番目の論理式を  e(i) とします。論理式  x の番号を  e^{-1}(x) とします。

 e(i) e は「言語関数」、 i e の「言語関数引数」です。 e(i) (「言語関数定義」と呼ぶことにします)の  i自然数または論理変数(論理式で使う変数)  s を指定した e(s) は、 e(i) に現れる「言語関数引数」 i をすべて  s に置き換えたものを表します。論理変数は大文字で表すことにします。

 e^{-1}(x) e^{-1} は「言語関数」、 x e^{-1} の「言語関数引数」です。

論理式  x に現れるすべての自由変数(式のある部分だけで使われる変数(束縛変数)ではない論理変数)  V を論理変数または自然数  s に変更した式を  x[V \mapsto s] と表すことにします。

この手順は以下のようになります。論理式の一部が  \forall V (P) または  \exists V (P) の形になっているとき、その部分のすべての論理変数  V を新しい変数  W に置き換えます。これを式の下位の部分から順に、 \forall V (P) または  \exists V (P) の形の式に論理変数  V が現れなくなるまで行います。その後すべての論理変数  V s に置き換えます。式に現れる変数は有限個で、変数は無限個あるので、プログラミング言語でこの手順を記述することができます。これは公理系から成り立つとします。

 f(i, s) = e(i)[V \mapsto s] とおきます。

 k 番目の証明式を  g(k) とします。証明式  y の番号を  g^{-1}(y) とします。 g(k) g は「言語関数」、 k g の「言語関数引数」です。 g^{-1}(y) g^{-1} は「言語関数」、 y g^{-1} の「言語関数引数」です。

証明式は推論規則の論理式とします。論理式は、証明式で変換することができます。変換した結果は「推論の要素」の論理式となります。結果が真のとき、その証明式はその論理式を真にする証明式と呼ぶことにします。

論理式を真にする証明式が存在するとき、その論理式は真であるとします。

以上のことは公理系から成り立つとします。この本の証明は(詳しく書かれていないのでわかりませんが)ペアノ算術の公理系に基づくと考えられますが、ここではこの公理系に関する不完全性を示します。

この本では番号は(詳しいことはわかりませんが)飛び飛びとなっていますが、ここでは番号はすべての自然数とします。式として成立しないものも含んでも良いとします。

【ステップ2】「 f(i, s) を真にする証明式が存在する」という論理式を  r(i, s) とおく。

 p(k, i) を「 k 番目の証明式  g(k) i 番目の論理式  e(i) を真にする証明式である」という論理式とします。

 r(i, s) = \exists k ( p(k, e^{-1}( f(i, s) ))) とおきます。

  •  r(i, s) \iff i 番目の論理式  e(i) の自由変数  V をすべて論理変数または自然数  s で置き換えた式  f(i, s) を真にする証明式が存在する
  •  \lnot r(i, s) \iff i 番目の論理式  e(i) の自由変数  V をすべて論理変数または自然数  s で置き換えた式  f(i, s) を真にする証明式が存在しない

となります。

【ステップ3】「言語関数定義」  r(i, s) i s を論理変数  V に置き換え、否定にした論理式  \lnot r(V, V) がある。これは、ステップ1で作った一覧表のどこかにある。それが  n 番目の論理式だったとする。つまり、 f(n, V) = \lnot r(V, V)

 r(i, s) の「関数引数」  i s は論理変数に置き換えることができ、置き換えると論理式になるものでした。 r(i, s) i s を論理変数  V に置き換えると論理式  r(V, V) になります。この否定の論理式  \lnot r(V, V) の番号を  n とおきます。 n = e^{-1}(\lnot r(V, V)) です。

【ステップ4】 f(n, V) = \lnot r(V, V) の論理変数  V に(自分自身の番号)  n を代入する(「言語関数定義」  f(i, s) i n s V で置き換える)。すなわち、 f(n, n) = \lnot r(n, n)

 e(n) = \lnot r(V, V) であるから

 f(n, n) = e(n)[V \mapsto n] = (\lnot r(V, V))[V \mapsto n] =  \lnot r(n, n)

が成り立ちます。

【ステップ5】ステップ4で作った論理式  f(n, n) = \lnot r(n, n) の右辺の内容は、(ステップ2を思い出せば)「 f(n, n) を真にする証明式が存在しない」となる。それは、 f(n, n) が証明できない、ということだ。でも、左辺を見れば、それは  f(n, n) にほかならない。すなわち、「この論理式は証明できません」という論理式  f(n, n) ができてしまった

 f(n, n) が何なのか考えてみます。

  • 自由変数のない論理式は真または偽
  • 論理式を真にする証明式が存在するならばその論理式は真
  • 自由変数のない論理式を真にする証明式が存在しないならばその論理式は証明できない

とします。

 f(n, n) f(n, s) の「関数引数」  s自然数  n で置き換えたものなので、自由変数のない論理式となっています。 f(n, n) が偽であるとすると、「 f(n, n) を真にする証明式が存在する」ということになります。すると  f(n, n) は真ということになって  f(n, n) が偽であることに矛盾します。よって  f(n, n) は真でなければなりません。 f(n, n) が真ならば「 f(n, n) を真にする証明式が存在しない」ということになって  f(n, n) は証明できないということになります。よって  f(n, n) は真であり証明できないということになります。

 f(i, s) を表にしたときに対角線に現れるものの1つが  f(n, n) となります。
 \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}

今後の目標(1)

不完全性定理」の証明を書き直そうとしていたら新年になってしまいました。今後の目標を書いていこうと思います。毎年何か書こうと思っていたのですが、PCが壊れてから書いていませんでした。

このブログについて

サーバーで永久に動作するプログラムを論理プログラミングで表す方法について調べていました。この目的で、現在は数式で表すことが難しいものをビジュアルプログラミングで表す例がないか調べています。

このブログでは、当初は数式で表すことが難しいため通常は数式の変形で書かないようなものを数式の変形を使って証明することを考えていました。これをエレファントな証明と呼んでいました。現在はビジュアルプログラミングを使おうと考えています。これを「エレファント・ビジュアライザー」と呼ぶことにします。

今後の目標

まず現在は「不完全性定理」ついて調べています。これはビジュアルプログラミングを数式の変形の代わりに使えるかどうかを調べるための例にならないかと思っているためです。ビジュアルプログラミングについては今後も調べていきます。

また「平方剰余の相互法則」についての本

(Kindle版があります)も読んでみたのですが、これもビジュアルプログラミングを数式の変形の代わりに使う例になるかもしれないので調べていきたいと思います。

「笑わない数学」という番組で超越数の話題があったので以下の本を読んでみました(Kindle版があります)。

eの定義やバーゼル問題についても調べてみましたが、複素関数積分を使ったほうが良いようです。複素関数論関係の本(Kindle版があります)をいくつか見てみましたが、(代数学の基本定理について調べたときにも見てみたのですが)ビジュアルプログラミングを使って何かやるのは難しそうです。

まずはこの問題(ビジュアルプログラミングを数式の変形の代わりに使うこと)を解決していきたいと思います。

現在の状況

不完全性定理」を調べているときに数理論理学関係の本でKindle版はないがKinoppyにある本があったので購入しました。

普通の本は字が小さくて結局読まないことになるのでなるべく電子書籍が良いのですが(電子書籍の場合も全部読むというわけではないのですが)、以下の本はたぶん電子書籍版がないので普通の本を買いました。

岩波文庫の方は持っていたかもしれないのですがわからないので買いました。

その他Kinoppyにあったものを書いておきます。

「数学のかんどころ」のシリーズもKinoppyにあったので買いました。

この本は普通の本を持っていて多項式について調べるときに読んでいたのですが、電子書籍の方が読みやすいので買いました。

複素関数論はKindleにもいくつかあるのですが以下のもの(Kinoppyにあります)も買ってみました。

Kinoppyでは以下の本も買っています。

不完全性定理(2)

不完全性定理とはなにか (ブルーバックス)』では「チューリング機械の停止問題」を参考にして「不完全性定理」を考えるということなので、前回は「チューリング機械の停止問題」について調べてみました。チューリング機械を扱うのではなく、無限のメモリーを持つコンピューター上のプログラミング言語の関数として考えました。チューリング機械の詳細な議論はしていませんが、この本でもそう書かれているようにだいたい同じものと考えられます。この方針を継続して不完全性定理についても考えていきます。

(論理式で書かれた)命題をプログラミング言語の式と考えます。命題の証明は、(関数の実行と同様に一定の有限の時間で行われる「段階」に分けることができて、各「段階」では推論規則(複数あります)または公理(複数あります)の1つが適用されます。有限個の「段階」で「常に真である命題」に到達したとき、または逆に「常に真である命題」から出発して有限個の「段階」で命題に到達したとき、命題は証明可能となります。そうではないときは命題は証明可能ではありません。

命題は「ソースコード」(文字列)で表されているとします。任意の文字列は「構文解析」によって「ソースコード」かどうかを判定することができるとします。変数名は「リスト」になっているとします。

命題が証明可能であるとき、証明の各「段階」をすべて(構造に従って)並べて書いたものを形式証明とします。形式証明は「ソースコード」(文字列)で表されているとし、命題の一部分とすることができます。

ゲーデル数を使った証明ではないので条件は違いますが、条件が強くなっているので不完全性の証明には問題ありません。

不完全性定理の証明

この本の流れに沿って見ていきます。チューリング機械の停止問題と比較するとわかりやすいと、この本では言っているようなので、できるだけチューリング機械の停止問題の記述に合わせてみることにします。

【ステップ1】 1変数の命題  F(y) を網羅した一覧表を作る。並べ方は、その命題の番号の小さい順とする。( F_{1}(y) F_{2}(y) F_{3}(y),……)

命題や形式証明は(プログラミング言語の式のように構造を持った)「式」として表します。

「式」のソースコードから「構造の『深さ』に関する帰納法」によって「式」に番号をつけることができます。無限個使うことができる変数名はリストで表されているので、これは可能です。逆に「式」を指定すると、構造を再現することができます。番号  i に対応する「式」を 「 i 番目の『式』」 e(i) とします。

【ステップ2】「 F_k(l) の形式証明の『式』  x が存在する」という命題を考える。これを  \exists x P(x,k,l) と略記する。
【ステップ3】命題  \exists x P(x,k,l) k l を変数  y に置き換え、否定にした命題  \lnot \exists x P(x,y,y) を考える。これは1変数  y をもつ命題なので、ステップ1で作った一覧表のどこかにある。それがたまたま上から  n 番目だったので、 F_n(y) と書く。つまり、 F_n(y) = \lnot \exists x P(x,y,y)
【ステップ4】 F_n(y) = \lnot \exists x P(x,y,y) の変数  y に(自分自身の背番号) n ( n 番目の「式」を表す自然数)を代入する。すなわち、 F_n(n) = \lnot \exists x P(x,n,n)
【ステップ5】ステップ4で作った命題  F_n(n) = \lnot \exists x P(x,n,n) の右辺の内容は、(ステップ2を思い出せば)「 F_n(n) の形式証明の『式』 x が存在しない」となる。対応する「式」の自然数が存在しないのだから、それは、 F_n(n) が証明できない、ということだ。でも、左辺を見れば、それは  F_n(n) にほかならない。すなわち、「この命題は証明できません」という命題  F_n(n) ができてしまった!

これは何を言っているのか考えてみます。ゲーデル数を使った議論は一階述語論理に「ペアノ算術」の公理系を追加した体系の議論で、ここでは一階述語論理に(ここには書いていませんが)プログラミング言語の「式」の公理系を追加した体系の議論となっています。一階述語論理では変数のない命題は真であるか偽であるかのどちらかになるので、ゲーデル数の議論でも「式」の議論でもそうなります。

自然数に関する命題  F_n(n) F_n(y) の変数  y を特定の自然数  n で置き換えたものなので、変数のない命題となっています。自然数  n に関する命題  F_n(n) が偽であるとすると、「 F_n(n) の形式証明の『式』を表す自然数が存在する」ということになります。すると  F_n(n) は真ということになって  F_n(n) が偽であることに矛盾します。よって  F_n(n) は真でなければなりません。 F_n(n) は真ならば「 F_n(n) の形式証明の『式』を表す自然数が存在しない」ということになって  F_n(n) は証明できないということになります。よって  F_n(n) は真で証明できないということになります。

チューリング機械の停止問題では関数が停止するかどうか決まっていると仮定したところが、この議論では「 F_k(l) の形式証明の式が存在する」という命題を考えるようになっています。ここが異なっているため命題がわかりにくくなっていると思われるので、同じようにできないか検討してみたいと思います。

中間報告(16)

ここの主な目的はサーバーのプログラムをブラウザーから更新できるようにするための理論を考えることです。ブログなどではブラウザーから更新することができるのですが、サーバーのプログラムを更新するというものではないため、多くの人がブログなどを書いてもシステムの改善にはつながらないという問題点があります。

ユーザーのブラウザーでの入力からサーバーのプログラムを作成することができれば良いのではないかと思うのですが、ブラウザー側でプログラムを作ったとしてもそれがサーバー側に反映されることはないように思います。それをサーバー側に反映させるためのプログラミング言語や理論が必要なのではないかということでいろいろ調べています。

論理プログラミングによる永続的プログラミング

永続性という用語は、ある時点の状態を記録して復元することを表すようですが、ここでは、サーバー上で永久に動くプログラムの状態を表すことを考えます。

論理プログラミングのデータを半環と考えて、多項式の極限を求めるように極限を作ることによって永続的プログラミングのデータを表すことを考えます。これは今のところうまく表すことができていませんが、これをビジュアルプログラミングを使って表すことを考えていきます。

クロージャーによる永続的プログラミング

クロージャーはどのように定義すれば良いのかよくわからないので調べています。クロージャーを使えば永続的プログラミングを表すことができると考えていて、論理プログラミングの場合と同様に、これをビジュアルプログラミングを使って表すことを考えています。

代数的構造での単一化

ある代数的構造の公理を組み合わせて、「最も一般的な定理」を作っていきます。これはもともと数式の変形で記述する事は可能ですが、数式で書くと複雑になるので、ビジュアルプログラミングを使って記述することを考えています。

多項式の計算と帰納法での単一化

帰納法での単一化は、代数的構造での単一化と同様です。帰納法の公理を組み合わせて、「最も一般的な定理」を作っていきます。

ガロア理論の説明に現れる計算の中に多項式の計算と帰納法で記述できそうなものがあります。これを数式の変形で記述しようとしていましたが、まだできていません。数式の変形で書こうとすると複雑になるので、ビジュアルプログラミングを使って記述することを考えていきます。

順序に依存しない記述

連立1次方程式の解は方程式の順序には依存しないのですが、方程式の順序に依存しないように解法を記述することが通常の数学の記法ではできないので、これを記述するための記法を考えていましたができていませんでした。これを数式の変形で記述しようとすると複雑になるので、ビジュアルプログラミングを使うことができないかと考えています。

素因数分解の一意性を説明する場合にも、ビジュアルプログラミングを使うことができないかと考えています。

可換モノイドのようなものを一般化したモノイド圏というものがあるので、これをビジュアルプログラミングで記述することができればいろいろ使えるのではないかと考えています。

不完全性定理(1)

不完全性定理とはなにか (ブルーバックス)』という本を見ると、不完全性定理について調べるためのヒントがいろいろ書かれていたので少し調べてみようと思います。また、ビジュアルプログラミングで何かやる例にすることができるかもしれないと考えています。

この本では「不完全性定理」は「チューリング機械の停止問題」と同様に考えることができるという主張のようなので、まず「チューリング機械の停止問題」を考えてみます。

この本では「万能チューリング機械」を無限のメモリーを持つコンピューターで動くプログラミング言語と考えればわかりやすいということのようです。この本ではプログラミング言語BASICで説明されていますが、ここではプログラミング言語Cで説明しようと思います。「チューリング機械」をプログラミング言語Cのようなプログラミング言語の関数と考えます。「万能チューリング機械」をちゃんと定義すると長くなるので入門書では省略されていて、そのためにわかりにくくなっている場合が多いですが、この本でもわかりにくくなっているように思います。

この本では入力と出力があるBASICのプログラムを考えていますが、ここではCの引数と戻り値がある関数を考えます。
この本では(BASICのプログラムで)少なくともWHILEループを使うことができて、無限ループを書くことができるようになっていますが、ここで(Cの)whileループを使うことができて、無限ループを書くことができるとします。

関数の実行は一定の有限の時間で行われる「段階」の分けることができて、各「段階」では代入、分岐、ループのためのジャンプなどが行われます。各「段階」は通常は順に実行されますが、ジャンプによって指定した「段階」に移動することもあります。有限個の「段階」でreturnステートメントに到達して値を返却したとき関数は終了します。そうではないとき(無限ループに入ったとき)関数は終了しません。関数が終了しないとき関数の値は  \bot とします。

無限のメモリーを持つコンピューターで動くプログラミング言語の関数を考えます。このプログラミング言語は、プログラミング言語Cのようなプログラミング言語で、任意の個数の変数を持ち、任意の桁数の自然数を表すことができるとします。このプログラミング言語プログラミング言語ωと呼ぶことにします。これは、もし無限のメモリーがあるなら通常のプログラミング言語Cでも成り立ちます。

このプログラミング言語ωの、引数がすべて自然数で、戻り値も自然数である関数を考えます。複数の自然数を一つの自然数にまとめることは可能で、そのまとめた自然数を元の複数の自然数に復元することも可能なので、引数の個数は1個のものを考えます。引数が複数の場合は、その複数の引数をまとめて一つの引数とし、それを元の複数の自然数に復元すると考えます。引数が複数のとき  (x_1, x_2, \cdots, x_n) のように「組」の形で書くこともできるとします。

「Cで書いたCの処理系」がありますが、それと同様にωでωの処理系を書きます。ωで書いたωの処理系をちゃんとした定義で書いたバージョンを、万能チューリング機械と考えることができます。ωで何ができるのかは説明していないのでCをイメージして想像することになります。

ωの関数  f のはコンピューターのメモリー上では一つの自然数で表されます。この自然数 \overline{f} と書くことにします( f のコードと呼ぶことにします)。関数  f を引数  x で実行したときの戻り値があるとき、その戻り値を  f(x) と書くことにします。戻り値がないときは  f(x) \bot と書くことにします。

関数は「ソースコード」(文字列)で表されているとします。任意の文字列は「構文解析」によって「ソースコード」かどうかを判定することができるとします。関数の引数、変数名、数値は「リスト」になっているとします。

停止問題

この本の流れに沿って見ていきます。少しわかりにくいところがあると思われます。

【ステップ1】あらゆる計算にそれぞれ特化したチューリング機械 T に背番号(添え字)をつけて縦に並べる

関数のソースコードから「構造の『深さ』に関する帰納法」によって関数に番号をつけることができます。無限個使うことができる変数名、数値はリストで表されているので、これは可能です。逆に番号を指定すると、構造を再現することができます。番号  i に対応する関数を 「 i 番目の関数」 e(i) とします(この本の表記では  T_i ですが  i の関数になっていることを強調するためにこのように書くこともできるものとします)。

【ステップ2】T に入力できるデータ(1、2、3、…)を横に並べる
【ステップ3】各チューリング機械に1、2、3、…を入力した出力結果(または「計算が終わらない」ことを意味する疑問符)を一覧表にする

疑問符は  \bot の意味です。任意の一つのチューリング機械に任意の一つの自然数を入力したとき、停止するかどうかは決まっていると仮定します。これは仮定で、これを仮定するとどうなるのかを議論します。

この本によると、この表が表すチューリング機械を万能チューリング機械と呼びます。表の縦軸と横軸の2つの引数が必要ですが、2つの引数を1つにまとめることが可能なので、この表をチューリング機械と考えることができます。 「 i 番目の関数」 e(i) の引数が  n のときの値  e(i)(n) の引数をまとめた  e(i, n) (または  e( (i, n) ))を万能チューリング機械とみなします。

【ステップ4】表の対角線の各出力を変える。たとえば「1を足す」ことにしよう。ただし、計算が終わらない場合は「0」に変えることにする。この結果を与えるチューリング機械を D と呼ぶことにする。
【ステップ5】ステップ4で作ったチューリング機械も、チューリング機械である以上、一覧表のどこかにあるはずだが、それは  T_1 ではない。なぜなら  T_1 に1を入力した結果が異なるから。同様に、それは  T_2 でもないし、 T_3 でもないし…一覧表のどこにも載っていない!
【ステップ6】チューリング機械 D がチューリング機械の一覧表に載っていない矛盾は、そもそもの仮定がまちがっていたからにほかならない。すなわち、任意のチューリング機械が停止するかしないかは決められないのである。

この本でこの後に書かれているように、このチューリング機械を  d として書き直します。任意の  x に対して  e(x,x) が停止するかどうかを判定することができると仮定すると、チューリング機械
 d(x) = \begin{cases}
e(x,x)+1 & (e(x,x) \ne \bot) \\
0 & (e(x,x) = \bot) \\
\end{cases}
を定義することができます。このチューリング機械  d e(1), e(2), \cdots の中にあります。これを  e(n) とすると、 d(n) = e(n,n) となって  d の定義に矛盾します。よって e(x,x) が停止するかどうかを判定することはできないことになります。

この本では「考え方はカントール対角線論法と同じなので、ほとんどの読者が理解できたはずだ」と書かれていますが、

などのところがわかりにくいので簡単ではないです。

中間報告(15)

ビジュアルプログラミングの調査

Blockly  |  Google for Developers」、「Charts  |  Google for Developers」をTypeScriptから使うことができるようになりました。

ビジュアルプログラミングによる数式の変形

通常の数式の変形では難しいことをビジュアルプログラミングでやるとどうなるかの調査ですが、「Blockly  |  Google for Developers」ではブロックを組み合わせたときに何かを選択するというのは難しそうなので、「検証的プログラミング」では通常のプログラムのように書いたものとビジュアルプログラミングを組み合わせることを検討中です。

サーバー対ブラウザープログラミング

新しいプログラミング・パラダイム』、『続 新しいプログラミング・パラダイム』がありました。持っていたはずが見当たらなくなっていたのですが、見つかりました。しかし「bit」の連載と内容はほぼ同じですし、「bit」電子版の方が文字を拡大できて読みやすいので「bit」の方を読んでいこうと思います。

自由可換モノイドの記法

素因数分解の一意性や連立一次方程式の解法を通常の数学の記法で書くと、その内容に比べて記述が複雑になりすぎるという点をなんとかできないか、ということで考えていたのですが中断していました。

圏論の道案内 ~矢印でえがく数学の世界~ 数学への招待』の最初の方で自由可換モノイドについての話題があるように書かれていたと思うのですが、とくに詳しく書かれてはいませんでした。『線型代数対話 第3巻 量系のテンソル積 多重線型性とその周辺 (線型代数対話 3巻)』では自由可換モノイドについて書かれているようなので、今後読んでいこうと思います。