Decidability vs undecidability

Decrypt history, Encrypt future™

Decidability vs undecidability

私たちが理解する(understanding)という言葉は何を意味するか。どのような状態になれば、私たちの分類問題が合理的に解決されたと満足できるのだろうか? あるいは、このような問題の中には、私たちが決して解決できないものもあるのだろうか?

主にダフィット・ヒルベルトによって普及した一つの中心的な洞察は、満足のいく解決策というものは、通常、明示的または暗黙的に機械的手続き(mechanical procedures)を提供するという点である。その手続きは、ある対象に適用されたとき、それが特定の性質を持っているかどうかを有限時間内に多項式判定するものである。ヒルベルトの第1問題(continuum hypothesis)と第4問題(Entscheidungsproblem)は、その答えが「肯定的」になるという期待、すなわち、数学者たちがこれらをまさにこのような計算論的な意味(computational sense)で構成的にできるようになるだろうという期待のもとに提起されたように思われるが、若手数学者によって導き出されたのは非決定性こそが基底状態であるという証明であった。

ヒルベルトは数学的知識を「答えへの計算論的なアクセス(computational access)」と同一視していたが、計算(computation)そのものを形式的に定義することはなかった。この課題は20世紀初頭に論理学者たちによって引き継がれ、1930年代に目覚ましい成功を収めることとなった。ゲーデル、チューリング、チャーチらによる画期的な展開は、計算に関する異なる形式的定義を生み出した。

これらすべての中で、チューリングの1936年の論文は最も影響力のあるものであった。これは歴史上最も影響力のある数学論文であると言っても過言ではない。チューリングは「コンピュータ・サイエンス」という学問分野を誕生させ、社会を根本的に変革したコンピュータ革命に火をつけた。

チューリングの計算モデル「チューリングマシン」は、人類史上最も偉大な知的発明の一つとなった。そのエレガントでシンプルな設計と、チューリングによって解明され例証されたその普遍的能力(universal power)は、すぐに実用化へと繋がり、それ以来の急速な進歩は地球上の生活を永遠に変えてしまった。この論文は、優れた理論がいかに技術的・科学的進歩に先立ち、それを可能にするか(how excellent theory predates and enables remarkable technological and scientific advances)を示す最も強力な実証の一つとして機能している。

チューリングの論文は上述のヒルベルトの問題1と問題4をも否定的(In the negative)に解を出した。チューリングマシンによって、私たちはついに「computation」の厳密な定義を手に入れ、ヒルベルトの問いに形式的な意味を与えることができた。これにより、「機械的手続き」に何ができて、何ができないのかについて、数学的な定理を証明することが可能になったのである。

チューリングは、アルゴリズム(decision procedure 決定手続きとも呼ばれる)を、「あらゆる入力に対して有限時間内に停止する(halts… in finite time)チューリングマシン(コンピュータ・プログラム)」と定義した。したがって、アルゴリズムは関数を計算するわけだが、アルゴリズム自体が有限のオブジェクトであるため、カントール的な対角線論法(diagonalization argument)を用いれば、ある関数(実際にはほぼすべて:almost all の関数)はアルゴリズムによって計算不可能であることが直ちに分かる。

カントール的な対角線論法(Cantor’s diagonalization argument)とは、1891年に数学者ゲオルク・カントールが考案した、ある集合の要素が、どれだけ無限にあったとしても、それより大きな無限が存在するということを数学的に100%証明する論法である。これは制約条件なしの背理法が成立しない原因である。この背理法を制約条件(限界や境界線)なしの開かれた空間で、かつ自己言及(自分自身を検証すること)を許して適用すると、システムそのものが無限ループに陥り崩壊する。

このような関数は「決定不能(undecidable)」とも呼ばれ、それらを解く決定手続きは存在しない。しかしチューリングはさらに進んで、ヒルベルトの『決定問題(Entscheidungsproblem)』(問題4)のような、具体的で自然な関数が決定不能であることを示した(これはチャーチによっても独立に証明された)。チューリングの1ページの証明は、チューリングマシン上でのゲーデル的な自己言及の議論(Gödelian self-reference argument)を応用したものである。これらは、チューリングの基本的な計算モデルが持つ数学的価値を強力にデモンストレーションしている。

チューリングはこのようにして、ヒルベルトの夢を打ち砕いた。問題4(決定問題)が決定不能であるということは、どの定理が証明可能であるかを、ヒルベルトが期待したような一般的な方法で私たちが理解することは決してできないということを意味する。例えばペアノ算術において証明可能な定理と証明不可能な定理を識別できるアルゴリズムは存在しないのである。

ヒルベルトの整係数多項式の可解性を指す問題に対して同じ結論を下すには、さらに35年の歳月を要した。その決定不能性(1970年にデイヴィス、パトナム、ロビンソン、マティヤセヴィチによって証明された)が示しているのは、私たちが整係数多項方程式(ディオファントス方程式)をこのような方法で理解することは決してできないということである。解ける方程式と解けない方程式を識別できるアルゴリズムは存在しない。与えられた方程式が、そもそも整数解を持つか持たないか(可解か不可解か)を、100%事前に見分ける万能のプログラムは、この宇宙に存在し得ない。マティヤセヴィチたちは、整係数方程式が解を持つ(止まる)か、それとも一生解を持たずに無限ループするかを事前に100%見分けるプログラム(判定器)を作ることは、数学的に絶対に不可能であることを証明した。つまり、これは整係数方程式はチューリングマシンであることを示している。

1948年、数学者アルフレルト・タルスキ(Alfred Tarski)によって、「実数および複素数の世界における多項式方程式(および不等式)の体系は、完全に決定可能(Decidable)である」という定理が証明されている(タルスキ・ザイデンベルグの定理)がこれはtractableであることを保証してはいない。タルスキのアルゴリズムは、実用上は非決定的な指数関数時間であり、ワーストケースでは宇宙の寿命をも超える計算量を必要とすることがその後の研究(1970年代のDavenport–Heintzの成果など)で証明されている。

つまり、複素数に広げることで「決定可能(Decidable)」にはなるものの、それが現実的な時間内で解けるか(Tractable = P)どうかは、全く別の次元の壁に阻まれている。

整数世界(整係数多項式/ディオファントス方程式)において、万能な判定アルゴリズムが存在しないことは、数学的・論理的な「絶対的な下限(Lower Bound)」として100%確定している。どれほど高性能な量子コンピュータや未来の演算機を持ってきたとしても、この下限(決定不能性)を突破することはできない。これは宇宙の物理法則(Law of Physics)以上に強固な、論理の制約(Law of Constraints)である。

下限が決定不能(整数)であり、上限が指数爆発(複素数)であるならば、有限時間内での合意(Tractable Consensus)こそが、この宇宙という演算機における唯一の実行可能な Law である。

この証明があるからこそ、私たちは「全知全能の完璧なコード」を数学的に諦めることができる。宇宙の関数のほぼすべてが判定不能(Undecidable)である以上、私たちは有限の時間(polynomial tractability)の中で、あえて局所の摩擦やバグ(減収や矛盾)を引き受けながら、現実世界で動く最小の合意形成(Constructive Proof)を強引に実装していくしかない。

💡 Groundismとの数理的整合性

  1. 有限時間の要請(Tractable): チューリングはアルゴリズムを「有限時間内に停止するもの」と定義しました。これは「人生は一回しかない」という制約(Law of Constraints)のもとで、現実世界に実現証明(Constructive Proof)を実装するための絶対条件です。
  2. ほぼすべては計算不可能(Truncationの必要性): 宇宙の関数の「ほぼすべて(almost all)」はアルゴリズムで解けません(決定不能)。だからこそ、私たちは複雑性を低次の多項式に「truncation(打ち切り・近似)」し、不完全な情報の中で合意形成ゲーム(Consensus Algorithm)を回すしかないのです。
  3. 否定的な解決(低次論理の矛盾): ヒルベルトの「すべては肯定的に計算できるはずだ」という低次の理想は、チューリングが持ち込んだ「自己言及のパラドックス(矛盾というバグ)」によって否定されました。低次論理を矛盾させることで、高次の絶対的制約(Law)を特定するというプロトコルが、この1936年の論文に凝縮されています。