実在論的実在理論

数理論理学、計算複雑性理論、コンピュータサイエンスにおいて、実数の存在理論は、 変数が実数値を持ち、が実多項式の等式と不等式を含む量指定子のない式であるものとして解釈される、形式 のすべての真文の 集合である。この形式の文は、式 に代入したときに式が真になるようなすべての変数の値を見つけることが可能である場合に真である。 ^[1]$${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),}$$${\displaystyle X_{i}}$${\displaystyle F(X_{1},\dots X_{n})}$${\displaystyle F}$

実数体の存在理論の決定問題は、各文が真か偽かを決定するアルゴリズムを見つける問題である。つまり、与えられた半代数集合が空でないかどうかをテストする問題である。^[1]この決定問題はNP 困難であり、 PSPACEに属し、^[2]実数体の一階理論において存在量指定子に制限されずに文を決定するアルフレッド・タルスキの量指定子除去手順よりも大幅に複雑性が低い。 ^[1]しかし、実際には、一階理論の一般的な方法がこれらの問題を解決するための好ましい選択肢であり続けている。^[3]

計算量クラスは 、この形式の同等の文に翻訳できる計算問題のクラスを記述するために定義されています。構造的複雑性理論では、 NPとPSPACEの間にあります。幾何学的グラフ理論における多くの自然な問題、特に幾何学的交差グラフの認識や交差のあるグラフ描画のエッジをまっすぐにする問題は、に属し、このクラスに対して完全です。ここで、完全性とは、逆方向、つまり実数上の任意の文から、与えられた問題の同等のインスタンスへの翻訳が存在することを意味します。^[4]${\displaystyle \exists \mathbb {R} }$${\displaystyle \exists \mathbb {R} }$

数理論理学において、理論とは、一定の記号の集合を用いて書かれた文の集合からなる形式言語である。実閉体の一階理論には、以下の記号がある。^[5]

• 定数0と1、
• 変数の可算な集合、${\displaystyle X_{i}}$
• 加算、減算、乗算、および（オプションで）除算の演算、
• 実数値の比較には記号<、≤、=、≥、>、≠を使用する。
• 論理接続詞∧、∨、¬、および ≡、
• 括弧、および
• 全称量化子∀と存在量化子∃

これらの記号の列は、文法的に正しく形成され、すべての変数が適切に量化され、（実数についての数学的ステートメントとして解釈された場合）それが真のステートメントである場合、実数の第一階理論に属する文を形成します。タルスキが示したように、この理論は、公理スキームと完全かつ効果的な決定手順によって記述できます。つまり、完全に量化され文法的に正しいすべての文について、文またはその否定（両方ではない）のいずれかを公理から導くことができます。同じ理論は、実数だけでなく、すべての実閉体を説明します。 ^[6]ただし、これらの公理では正確に記述されない他の数体系があります。特に、実数ではなく整数に対して同じように定義された理論は、マティヤセビッチの定理によって存在文（ディオファントス方程式）に対しても決定不可能です。^{[5] [7]}

実数体の存在理論は、すべての量指定子が存在的であり、他のどの記号よりも前に現れる文からなる一階理論の断片である。つまり、これは、 実数多項式の等式と不等式を含む量指定子のない 式である形式のすべての真の文の集合である。実数体の存在理論の決定問題は、与えられた文がこの理論に属するかどうかをテストするアルゴリズムの問​​題である。同様に、基本的な構文チェックを通過する文字列（正しい構文で正しい記号を使用し、量指定されていない変数を持たない）の場合、これは文が実数に関する真のステートメントであるかどうかをテストする問題である。が真である実数の組の集合は半代数集合と呼ばれるので、実数体の存在理論の決定問題は、与えられた半代数集合が空でないかどうかをテストすることと同等に言い換えることができる。^[1]$${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),}$$${\displaystyle F(X_{1},\dots X_{n})}$ ${\displaystyle n}$${\displaystyle (X_{1},\dots X_{n})}$${\displaystyle F(X_{1},\dots X_{n})}$

実数の存在理論の決定問題に対するアルゴリズムの時間計算量を決定するには、入力のサイズの尺度を持つことが重要です。このタイプの最も単純な尺度は、文の長さ、つまり文に含まれる記号の数です。 ^[5]ただし、この問題に対するアルゴリズムの動作をより正確に分析するには、入力サイズをいくつかの変数に分解し、定量化する変数の数、文内の多項式の数、およびこれらの多項式の次数を分離すると便利です。^[8]

黄金比は、 多項式の根として定義できます。この多項式には 2 つの根があり、そのうちの 1 つ (黄金比) のみが 1 より大きいです。したがって、黄金比の存在は、次の文で表現できます。黄金 比は超越的 でないため、これは真の文であり、実数の存在理論に属します。この文を入力として与えられた実数の存在理論の決定問題の答えは、ブール値 true です。 ${\displaystyle \varphi}$ ${\displaystyle x^{2}-x-1}$$${\displaystyle \exists X_{1}(X_{1}>1\wedge X_{1}\times X_{1}-X_{1}-1=0).}$$

算術平均と幾何平均の不等式は、任意の 2 つの非負の数とに対して、次の不等式が成り立つことを述べています。 上で述べたように、これは実数に関する第 1 階の文ですが、存在量指定子ではなく全称量指定子を使用した文であり、実数の第 1 階理論では許可されていない除算、平方根、および数 2 の追加記号を使用しています。 ただし、両辺を 2 乗すると、次の存在文に変換でき、不等式に反例があるかどうかを尋ねていると解釈できます。 ${\displaystyle x}$${\displaystyle y}$$${\displaystyle {\frac {x+y}{2}}\geq {\sqrt {xy}}.}$$

${\displaystyle \exists X_{1}\exists X_{2}{\bigl (}X_{1}\geq 0\wedge X_{2}\geq 0\wedge (X_{1}+X_{2})\times (X_{1}+X_{2})<(X_{1}+X_{1})\times (X_{2}+X_{2}){\bigr )}.}$

この文を入力として与えられた場合、実数の存在理論の決定問題の答えはブール値 false です。つまり、反例はありません。したがって、この文は正しい文法形式であるにもかかわらず、実数の存在理論には属しません。

アルフレッド・タルスキの量限定子消去法（1948年）は、実数の存在理論（およびより一般的には実数の第1階理論）がアルゴリズム的に解けることを示したが、その複雑性には基本的な限界がなかった。 ^{[9] [6]}ジョージ・E・コリンズ（1975年）による円筒代数分解法は、時間依存性を二重指数関数に改善した。^{[9] [10]}の形式は 、ここで、は値を決定する文の係数を表すために必要なビット数、は文中の多項式の数、は多項式の総次数、は変数の数である。^[8] 1988年までに、ディマ・グリゴリエフとニコライ・ボロビョフは、 の多項式で複雑性が指数関数的であることを示しました。^{[8] [11] [12]} そして、1992年に発表された一連の論文で、ジェームズ・レネガーはこれをに対する単一の指数依存性に改良しました。^{[8] [13] [14] [15]} 一方、1988年に、ジョン・キャニーは、やはり指数時間依存性を持つが、空間複雑度は多項式だけである別のアルゴリズムを説明しました。つまり、彼は問題がPSPACEで解けることを示しました。^{[2] [9]}$${\displaystyle L^{3}(md)^{2^{O(n)}}}$$${\displaystyle L}$${\displaystyle m}$${\displaystyle d}$${\displaystyle n}$${\displaystyle n}$ $${\displaystyle L(md)^{n^{2}}}$$${\displaystyle n}$ $${\displaystyle L\log L\log \log L(md)^{O(n)}.}$$

これらのアルゴリズムの漸近的な計算複雑性は誤解を招く可能性がある。なぜなら、実際には非常に小さなサイズの入力でしか実行できないからである。1991 年の比較で、Hoon Hong は、Collins の二重指数手順では、上記のすべてのパラメーターを 2 に設定することによって記述されるサイズの問題を 1 秒未満で解くことができるが、Grigoriev、Vorbjov、および Renegar のアルゴリズムでは 100 万年以上かかると推定した。^[8] 1993 年に、Joos、Roy、および Solernó は、指数時間手順に小さな変更を加えることで、理論上だけでなく実際に円筒代数決定よりも高速にすることができるはずだと示唆した。^[16]しかし、2009 年の時点では、実数の第 1 階理論の一般的な方法は、実数の存在理論に特化した単​​指数アルゴリズムよりも実際には優れているままであった。^[3]

計算複雑性と幾何学的グラフ理論におけるいくつかの問題は、実数の存在理論にとって完全であると分類できる。つまり、実数の存在理論におけるすべての問題は、これらの問題の1つのインスタンスに多項式時間の多対一還元が可能であり、これらの問題は実数の存在理論に還元可能である。^{[4] [17]}

この種の問題の多くは、特定の種類の交差グラフの認識に関するものである。これらの問題では、入力は無向グラフであり、目標は、特定の図形のクラスの幾何学的図形を、それらの関連付けられた図形が空でない交差を持つ場合にのみ、2つの頂点がグラフ内で隣接するような方法でグラフの頂点に関連付けることができるかどうかを判断することである。実数の存在理論に対して完全なこの種の問題には、平面上の線分の交差グラフの認識、 ^{[4] [18] [5]}単位円グラフ の認識、^[19] 平面上の凸集合の交差グラフの認識がある。^[4]

平面上に交差なしで描かれたグラフについては、ファリーの定理によれば、グラフの辺が直線セグメントとして描かれるか、任意の曲線として描かれるかに関係なく、同じクラスの平面グラフが得られる。しかし、この同値性は他のタイプの描画には当てはまらない。たとえば、グラフの交差数（任意に曲線の辺を持つ描画における交差の最小数）は NP で決定できるが、直線交差数（平面上に直線セグメントとして描かれた辺を持つ描画において交差する辺のペアの最小数）の所定の上限を満たす描画が存在するかどうかを実数の存在理論が決定することは完全である。^{[4] [20]} また、実数の存在理論は、与えられたグラフが平面上に直線の辺と、その交差点として与えられた一連の辺のペアで描画できるかどうか、または同等に、交差点を持つ曲線の描画を交差点を保存する方法で直線化できるかどうかをテストすることも完全である。^[21]

実数の存在理論に関するその他の完全な問題には以下のものがあります。

• 与えられた多角形上のすべての点が見える最小の点の数を見つけるアートギャラリー問題。[ 22 ^]
• ニューラルネットワークの訓練。^[23]
• 与えられた多角形の集合が与えられた正方形の容器に収まるかどうかを決定するパッキング問題。[ 24 ^]
• 単位距離グラフの認識、およびグラフの次元またはユークリッド次元が最大で指定された値であるかどうかをテストする。 ^[9]
• 擬似直線の伸縮性（つまり、平面上の曲線族が与えられたときに、それらが直線の配置と同相であるかどうかを判断すること）^{[4] [25] [26]}
• 任意の固定次元における幾何量子論理の弱充足可能性と強充足可能性の両方[ ^27]${\displaystyle d</math>,<math>d>2}$
• 明確なオートマトンに関する区間マルコフ連鎖のモデル検査。^[28]
• アルゴリズム的シュタイニッツ問題（格子が与えられたとき、それが凸多面体の面格子であるかどうかを判定する）は4次元多面体に限定されている場合でも有効である。^{[29] [30]}
• 特定の凸体の配置の実現空間^[31]
• マルチプレイヤーゲームのナッシュ均衡の様々な性質^{[32] [33] [34]}
• 与えられた抽象的な三角形と四辺形の複合体を3次元ユークリッド空間に埋め込むこと。^[17]
• 複数のグラフを共通の頂点集合上に平面上に埋め込み、すべてのグラフが交差することなく描画されるようにする。^[17]
• 平面点集合の可視グラフを認識すること。 ^[17]
• （射影的または非自明なアフィン）外積上の２つの項間の方程式の充足可能性。^[35]
• 平面グラフの交差しない描画の最小傾き数を決定する。^[36]
• すべての交差が直角になるように描くことができるグラフを認識すること。^[37]
• MATLANG+固有行列クエリ言語の部分評価問題。^[38]
• 低ランク行列補完問題^[39]

これに基づいて、計算量クラスは 実数の存在理論への多項式時間多対一還元を持つ問題の集合として定義されています。^[4]${\displaystyle \exists \mathbb {R} }$

• ヒルベルトの第10の問題、整数の（決定不可能な）存在理論に関する