Kolmogorov複雑度の計算不能性
メモ
要するに，
Kolmogorov複雑度が$ L以上の自然数$ xが存在することは示すことが出来る(Lem2)
しかしながら，その$ xが具体的にはどれなのかは計算出来ない(Thm3)，というところが力点となる．
ただし前提が可能なのかはかなり怪しい気もする．
Def:
自然数
$ \N = \{1,2,\dots\}とする
$ 0は入らないことに注意！
空バイナリ列について
長さが$ 0の空バイナリ列$ \varepsilonについては考えないものとする．
自然数のバイナリ列
バイナリ列を2進数表記された自然数と見たとき，$ n \in \Nに対応するもっとも短いバイナリ列を$ nのバイナリ列という．
remark:$ 7と見れるバイナリ列は$ \sf 111,0111,00111,000111,\dotsとあるが，$ 7のバイナリ列と言ったときは$ \sf 111である．
$ nのバイナリ列の長さを$ |n|として表す．
長さが$ Lである自然数$ x（すなわち$ |x| = L）を，長さ$ Lの自然数という．
remark:
長さ$ Lの自然数として有効なものは必ず$ \mathsf{1}\underbrace{\mathsf{01110110010}}_{L - 1}の様に表される．
したがって，長さ$ Lの自然数は$ 2^{L-1}個存在する．
話がややこしくなるので，永遠に止まらないプログラムは考えないものとする．
プログラム$ \sf Pが$ \mathcal{U}上で計算したとき停止して何らかの自然数$ n \in \Nを1つ出力したとき，$ \mathsf{P}は$ \mathcal{U}上で有効といい，この状況を$ \mathcal{U}(\mathsf{P}) \Rightarrow nと表記する．
バイナリ列とプログラムには1:1の対応があるとする．
ただし，あるバイナリ列に対応するプログラムが$ \mathcal{U}上で有効かは保証されない．
当然，このエンコーディングは有限時間で終わるものとする．
プログラム$ \mathsf{P}をエンコードしたバイナリ列$ \beta_\mathsf{P}の長さ$ |\beta_\mathsf{P}|を，$ fの長さと呼び$ |\mathsf{P}|として表す．
$ n \in \Nを出力する有効なプログラム全体の中で最小の長さを持つプログラムの長さを，$ nの$ \mathcal{U}上でのKolmogorov複雑度といい，$ K_\mathcal{U}(n)と表す． メソッド
引数を受け取って自然数を出力する$ \mathcal{U}上のプログラムの断片をメソッドと言うことにし，$ \mathsf{m}(x)のように表す．
メソッドは引数を受け取る，すなわち外部状態に依存するため，$ \mathcal{U}上で有効なプログラムではない．
有効なプログラムはそれ単体で実行可能でなければならない．
メソッドの引数に定数を埋め込んで呼び出すものはプログラムとして有効になる．
しかしメソッドにも長さはあり，同じ様に$ |\mathsf{m}(x)|と表す．
Thm 1:
任意の$ x, L \in \Nに対して，$ K_\mathcal{U}(x) \leq L及び$ K_\mathcal{U}(x) < Lかどうかは検証可能である．
proof:
$ \leqの場合のみを示す．$ <は同様にやれば示せる．
長さが$ L以下のバイナリ列は$ \sum_{k=1}^L 2^k = 2^{L+1}-2種類存在する．
すなわち$ \mathcal{U}上で有効なプログラムは高々$ 2^{L+1}-2個しか存在しない．
ともあれ，$ 2^{L+1}-2種類のバイナリ列を$ \mathcal{U}に入れて全て計算してみる．
プログラムの停止性の仮定よりこれはいずれ終わることが保証されている．
$ \mathcal{U}(\mathsf{P})\Rightarrow xとなる有効なプログラム$ \mathsf{P}が存在したなら$ K_\mathcal{U}(x) \leq Lとなる．
そうでないなら，$ K_\mathcal{U}(x) \not\leq Lすなわち$ K_\mathcal{U}(x) > Lである．
Lem 2:
任意の$ L \in \Nについて，長さ$ L以下の自然数$ xで$ K_\mathcal{U}(x) \ge Lとなる$ xが存在する．
proof:
長さが$ L以下の自然数は$ \sum_{k=1}^L 2^{k-1} = 2^L - 1個存在する．
長さ$ L未満のバイナリ列は$ \sum_{k=1}^{L-1} 2^k = 2^{L} - 2種類存在する．
すなわち，長さ$ L未満のプログラムは高々$ 2^L - 2個しか存在しない．
$ 2^L - 1 - (2^L - 2) = 1より
長さが$ L未満のプログラムで出力できない，長さが$ L以下の自然数が最低1つは存在する．
example:
長さが$ 2以下の自然数のバイナリ列は$ \sf 11,10,1
長さが$ 2未満のプログラムの候補$ \sf 1,0
よってどう頑張っても，$ \sf 11,10,1のうち最低1つには有効な長さ$ 2未満のプログラムは存在しない．
よって題意が満たされる．
Remark:
Lem2は，存在が示される$ xが具体的にはどれなのか？という問題には全く答えていない．
$ xを特定するには$ K_\mathcal{U}(x)の値を一つずつ計算してチェックする必要がある．
ところが，具体的に$ K_\mathcal{U}(x)が計算可能であると仮定すると，矛盾が発生することをThm3で見る．
Thm 3:
$ K_\mathcal{U}(x)は$ \mathcal{U}上で有限時間で計算可能ではない．
proof:
$ K_\mathcal{U}(x)が$ \mathcal{U}上で有限時間で計算可能だと仮定する．
すなわち，$ \mathcal{U}上でKolmogorov複雑度を計算するメソッド$ \mathsf{kc}(x)が存在するとする． $ K_\mathcal{U}(x) \ge mとなる最初の自然数$ xを返すメソッド$ \mathsf{complex}(m)が構成出来る．
Lem2より，$ xは少なくとも長さが$ m以下の自然数のどれかである．
よって長さが$ 1から$ mまでの自然数$ 1,\dots,2^m-1までを全部列挙して$ \mathsf{kc}(x)に入れていけば，そのような$ xが必ず有限時間で見つかる．
注意したように，Lem2単体では具体的にどれがそのような$ xかはわからず，$ \mathsf{kc}(x)が存在して初めて$ xが特定できる．
$ \mathsf{complex}(|\mathsf{complex}(x)| + n)を出力するプログラムを$ \mathsf{P}_nとする．
$ \mathsf{P}_nは引数を受け取らず自然数を出力するので$ \mathcal{U}上で有効なプログラムである．
$ nは引数ではなく，$ \mathsf{P}_nの中に長さ$ |n|の文字列として埋め込まれている．
$ |\mathsf{P}_n| = |\mathsf{complex}(x)| + |n| + Cである．
$ Cは$ \mathcal{U}上でのメソッドの呼び出し部分など，非本質的な部分の長さ．
今，$ \mathcal{U}(\mathsf{P}_n) \Rightarrow yだったとする．
$ yは$ \mathsf{complex}(|\mathsf{complex}(x)| + n)によって計算されるので定義より$ K_\mathcal{U}(y) \ge |\mathsf{complex}(x)| + n
一方，$ yは$ \mathsf{P}_nで計算されるのでKolmogorov複雑度の定義より$ K_\mathcal{U}(y) \le |\mathsf{P}_n| = |\mathsf{complex}(x)| + |n| + C 整理すると，$ |\mathsf{complex}(x)| + n \le K_\mathcal{U}(y) \le |\mathsf{complex}(x)| + |n| + Cである．
しかし，十分に$ nが大きいとき$ n > |n|であるので，そのような$ nに対して不等式は明らかに矛盾する．
example:
$ C = 0と想定し，$ n = 8とすれば$ |8| = |\mathsf{111}| = 3であるので，
$ |\mathsf{complex}(x)| + 8 \le K_\mathcal{U}(y) \le |\mathsf{complex}(x)| + 3
となって明らかにおかしな事態が発生する．
よって，$ K_\mathcal{U}(x)は$ \mathcal{U}上で有限時間で計算可能ではない．
Cor 4:
Thm3の証明を振り返る．
問題の不等式がギリギリまで成り立つような，
すなわち$ |\mathsf{complex}(x)| + n = K_\mathcal{U}(y) = |\mathsf{complex}(x)| + |n| + Cとなるような，ギリギリの$ n = |n| + Cを考える．
その$ nを$ Lとする．
$ Lより大きいなら有限時間で計算可能とすると破綻するのである．
すなわち，Thm3はより詳細には以下の形で述べることも出来る．
十分に大きな$ Lより大きいKolmogorov複雑度$ K_\mathcal{U}(x)は，$ \mathcal{U}上で有限時間で計算不能．
同じことだが，
十分に大きな$ Lについて，任意の$ xについて$ K(x) > Lかどうかは$ \mathcal{U}上で判定できない．
Thm3及びCor4は，十分に強い無矛盾な$ \sf PAの拡大理論$ T上で形式化することが出来る．
すなわち，以下のことが主張される．
任意の$ xについて$ T \nvdash K(x) > Lとなるような，十分に大きな$ Lが存在する．
proof sketch:
万能計算機やプログラムというフワッとしたものに訴えていた議論を，万能Turingマシンや$ \sf PA上の再帰的関数として再実装すればよい． ただしここで考えていたプログラムは有効なら絶対に停止することを前提にしていたので，その辺りが面倒かも知れない．
remark:
Lem2で$ L+1とすると$ K(x) > Lとなるような$ xが（長さ$ L+1以下の自然数として）存在する．
しかしその$ K(x)が$ Lより大きいことは，$ T上で絶対に証明出来ないのである．
正しいが証明は出来ない，これがこの系が不完全性定理と言われる所以である．