コルモゴロフ複雑性

索引トップ用語の索引ランキングカテゴリー

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/06/22 05:14 UTC 版)

チャイティンの不完全性定理

殆どの文字列は、より「圧縮された」形では表現できないという意味で複雑である。しかしながら、文字列の長さがある閾値を超える場合、その文字列が複雑であることを形式的に証明することは出来ない、ということが言えてしまう。正確な定式化は以下の通り。まず、自然数を扱う特定の公理系 S を固定する。この公理系は次のことが出来る程度には強いものとする。即ち、S に含まれる式 F_A を、文字列の複雑さに関する或る主張 A に関連付けることが出来る。この際、F_Aが S の公理から証明可能なら、これに対応する主張 A も真になるとする。この「定式化」に際しては、ゲーデル数化のような人工的な符号化を用いてもよいし、適用しようとする S をもっと明快に表現するような定式化を用いても良い。

定理：次の式（をS の中で定式化したもの）を公理系 S の中で証明できるように文字列 s を取れないような、定数 L（具体的な値は公理系と記述言語にのみ依存する）が存在する。

K(s)\geq L.

圧縮不能に近い文字列は大量にあることから、殆ど全ての場合にこの式は真である筈なことに注意されたい。

この結果の証明はベリーのパラドックスに似た自己言及的な構成を用いる。以下、背理法による。この定理が偽だと仮定すると、次のことが言える。

主張(X)：任意の整数 n について、ある文字列 s が存在し、体系Sの中で式「K(s)≧n」（がSの中で定式化できると仮定して）を証明できる。

S内の形式的証明全てを実効的に枚挙する何らかの手段を見つけることができる。

  function NthProof(int n)

は入力として n を取り、適当な証明を出力する。この関数は全ての証明を枚挙する。その中には我々にとって差し当たり興味のない証明も混ざるだろう（NthProof()が枚挙する証明の中には例えば平方剰余の相互法則の証明、フェルマーの小定理の証明、フェルマーの最終定理の証明など、様々な既知の証明をS内の形式的言語に翻訳したものが現れるだろう）。この中の幾つかは K(s)≧n という形をした複雑性に関する式の証明である（s と n はS内の言語における定数）。さて、次のプログラムが存在する。

  function NthProofProvesComplexityFormula(int n)

このプログラムは n 番目の証明が式 K(s)≧L を証明しているどうかを判定する。文字列 s と整数 L はそれぞれ以下のプログラムで計算可能である：

  function StringNthProof(int n)

  function ComplexityLowerBoundNthProof(int n)

ここで次のようなプログラムを考えよう。

  function GenerateProvablyComplexString(int n)
     for i = 1 to 無限大:
        if  NthProofProvesComplexityFormula(i) and ComplexityLowerBoundNthProof(i) >= n 
           return StringNthProof(i)
           quit

任意の n について、このプログラムは形式体系S内のありとあらゆる証明を調べ上げて、K(s)≧L（但しL ≧ n ）を満たす文字列と証明を探し出そうとする。主張(X)によりこのプログラムは必ず停止する。このプログラムの長さを U としよう。このとき、ある整数 n₀ があって、U + log₂(n₀) + C < n₀ を満たす。ここで C は、次のプログラムがGenerateProvablyComplexString()を呼び出す前後の固定的な長さである。

   function GenerateProvablyParadoxicalString()
      return GenerateProvablyComplexString(n₀)
      quit

プログラム GenerateProvablyParadoxicalString() は文字列 s を出力するが、このとき L が存在して K(s)≧L（但し L ≧ n₀）を満たし、S内でこれを形式的に証明できる。特に K(s)≧n₀ は真である。ところが、s は長さが U+log₂(n₀)+C であるプログラムでも生成できるので、その複雑性は n₀ よりも小さい。これは矛盾である。よって主張(X)は成り立たないことが証明された。