フェイギンの定理

フェイギンの定理は、記述的複雑性理論における最も古い成果である。記述的複雑性理論は、計算複雑性理論の一分野であり、複雑性クラスを、問題を解決するアルゴリズムの挙動ではなく、論理に基づいた問題の記述によって特徴づける。この定理は、存在二階述語論理で表現可能なすべての性質の集合が、まさに複雑性クラスNPであると述べている。

これは、1973 年にロナルド・ファギンが博士論文で証明し、1974 年の論文に掲載されています。^{[ 1 ]} 2 次式で要求されるアリティは、1981 年にジェームズ・リンチによって (一方向で) 改善され、 [ 2 ^{]エティエンヌ・}グランジャンによるいくつかの結果により、非決定性ランダムアクセスマシンに対するより厳密な境界が提供されています。^{[ 3 ]}

例えば、グラフが3彩色可能かどうかを判定する問題を考えてみましょう。これはNP完全問題です。ファギンの定理によれば、2階存在式が存在します。${\displaystyle \phi }$グラフが 3 彩色可能であるのは、グラフが有限モデルとして${\displaystyle \phi }$意味的には${\displaystyle \phi }$具体的には、そのような式が1つあります。^{[ 4 ]}

(∃A, B, C)(∀v)[(A(v) ∨ B(v) ∨ C(v)) ∧ (∀w)(E(v, w) → ¬(A(v) ∧ A(w)) ∧ ¬(B(v) ∧ B(w)) ∧ ¬(C(v) ∧ C(w)))]

この式において、A、B、Cはそれぞれ3色で着色された頂点の集合を表し、E(v, w)は頂点vとwが辺を共有することを意味します。そして、この式は隣接する2つの頂点が同じ色を持たないことを示しています。

各頂点に必ず1色だけを割り当てる必要はなく、少なくとも1色だけ割り当てればよいことに注意してください。なぜなら、頂点ごとに複数の色を割り当てても、隣接する2つの頂点が同じ色にならないようにすれば、各頂点に必ず1色だけを割り当てても、隣接する2つの頂点が同じ色にならないようにできるからです。

イマーマンによる1999年の教科書には、この定理の詳細な証明が記載されている。ここではその概略を示す。^{[ 5 ]}

存在量化子を用いて、存在量化子で修飾されたすべての変数の値を非決定的に選択することで、NP においてすべての存在量化子式を認識できることは容易に示せる。したがって、証明の主要部分は、NP のすべての言語が存在量化子式で記述できることを示すことである。そのためには、存在量化子式を用いて計算タブローを任意に選択すればよい。より詳細には、非決定性チューリングマシンの実行トレースの各タイムステップにおいて、このタブローはチューリングマシンの状態、テープ上の位置、各テープセルの内容、およびそのステップでマシンが行う非決定的な選択を符号化する。一階述語論理式は、この符号化された情報を制約することで、有効な実行トレースを記述することができる。有効な実行トレースとは、各タイムステップにおけるテープの内容、チューリングマシンの状態、および位置が前のタイムステップから導かれるトレースである。

証明で用いられる重要な補題は、長さの線形順序を符号化できるということである。${\displaystyle n^{k}}$（例えば、任意のタイムステップにおけるタイムステップとテープ内容の線形順序など）${\displaystyle 2k}$-項関係${\displaystyle R}$宇宙において${\displaystyle A}$サイズの${\displaystyle n}$ これを実現する一つの方法は、線形順序を選択することである。${\displaystyle L}$の${\displaystyle A}$そして定義する${\displaystyle R}$辞書的な順序付けである${\displaystyle k}$-タプルから${\displaystyle A}$に関して​${\displaystyle L}$。

• 文のスペクトル

• Fagin, Ronald (1974). 「一般化された一次スペクトルと多項式時間で認識可能な集合」 . Karp, Richard M. (編) 『計算の複雑性：1973年4月18～19日にニューヨーク市で開催されたアメリカ数学会および産業応用数学会の応用数学シンポジウム議事録』 SIAM–AMS議事録、第7巻、アメリカ 数学会、pp . 43–73。ISBN  978-0-8218-1327-0. MR 0371622 . 
• Grandjean, Étienne (1985). "普遍量化子とランダムアクセスマシンの時間計算量". Mathematical Systems Theory . 18 (2): 171– 187. doi : 10.1007/BF01699468 . MR 0797194 . 
• Grandjean, Étienne; Olive, Frédéric (1998). "非決定性線形時間のモナド論理定義可能性". Computational Complexity . 7 (1): 54–97 . doi : 10.1007/PL00001594 . MR 1628153 . 
• イマーマン、ニール（1999）。『記述的複雑性』ニューヨーク：シュプリンガー・フェルラーク。113-119頁。ISBN  0-387-98600-6。
• Lynch, James (1981年12月). 「複雑性クラスと有限モデルの理論」 . Mathematical Systems Theory . 15 : 127–144 . doi : 10.1007/BF01786976 . S2CID 496247 . 
• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Marx, Maarten; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007).有限モデル理論とその応用. 理論計算機科学テキストシリーズ. EATCSシリーズ. ベルリン: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 .