固定小数点ロジック

数理論理学において、固定小数点論理は、再帰を表現するために導入された古典的な述語論理の拡張です。その開発は、記述的複雑性理論と、データベース クエリ言語、特にDatalogとの関係によって促進されてきました。

最小固定小数点論理は、1974年にYiannis N. Moschovakisによって初めて体系的に研究され、 ^{[1] 1979年に}Alfred AhoとJeffrey Ullmanが表現力豊かなデータベースクエリ言語として固定小数点論理を提案したときにコンピュータ科学者に紹介されました 。^[2]

関係シグネチャ Xの場合、FO[PFP]( X ) は、という形式の式を形成するために使用される、 1 階接続詞と述語、2 階変数、および部分固定小数点演算子を使用してXから形成される式の集合です。ここで、 は2 階変数、1 階変数のタプル、項のタプルであり、との長さはのアリティと一致します。 ${\displaystyle \operatorname {PFP} }$${\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}$${\displaystyle P}$${\displaystyle {\vec {x}}}$${\displaystyle {\vec {t}}}$${\displaystyle {\vec {x}}}$${\displaystyle {\vec {t}}}$${\displaystyle P}$

kを整数、 をk個の変数のベクトル、P をk個の引数を持つ 2 階変数、φ をxとP を変数とする FO(PFP,X) 関数とします。 および（φ を2 階変数Pに代入したもの）となるように反復的に定義できます。この場合、不動点が存在するか、s のリストが循環的になります。^[3]${\displaystyle x,y}$${\displaystyle (P_{i})_{i\in N}}$${\displaystyle P_{0}(x)=false}$${\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}$${\displaystyle P_{i-1}}$${\displaystyle (P_{i})}$

${\displaystyle [\operatorname {PFP} _{P,x}\varphi (y)]}$は、不動点がある場合はyの不動点の値として定義され、ない場合は false として定義されます。 ^[4] Pはk個の引数を持つプロパティであるため、には最大で 個の値があり、多項式空間カウンターを使用してループがあるかどうかを確認できます。^[5]${\displaystyle (P_{i})}$${\displaystyle 2^{n^{k}}}$${\displaystyle P_{i}}$

順序付けられた有限構造において、ある性質がFO(PFP, X )で表現可能であるのは、それがPSPACE内にある場合のみであることが証明されている。^[6]

部分不動点の計算に含まれる反復述語は一般に単調ではないため、不動点は常に存在するとは限りません。最小不動点論理FO(LFP,X) は、 FO(PFP,X) 内の式の集合であり、部分不動点は、Pの正の発生 (つまり、偶数回の否定が先行する発生) のみを含む式φに対してのみ取られます。これにより、不動点構成の単調性が保証されます (つまり、2 次変数がPの場合、常に を意味します)。 ${\displaystyle P_{i}(x)}$${\displaystyle P_{i+1}(x)}$

単調性のため、Pの真理値表にはベクトルのみが追加され、可能なベクトルのみが存在するため、反復の前に必ず不動点が見つかります。Immerman ^[7]とVardi ^{[8]によって独立に示された}Immerman -Vardiの定理は、FO(LFP, X )がすべての順序付き構造上のPを特徴付けることを示しています。 ${\displaystyle n^{k}}$${\displaystyle n^{k}}$

最小固定点論理の表現力はデータベースクエリ言語Datalogの表現力と完全に一致しており、順序付けられた構造上ではDatalogが多項式時間で実行可能なクエリを正確に表現できることを示しています。^[9]

固定小数点構造の単調性を保証する別の方法は、が成立しなくなったタプルを削除せずに、反復の各段階でに新しいタプルを追加するだけです。正式には、をとして定義します。 ${\displaystyle P}$${\displaystyle P}$${\displaystyle \operatorname {IFP} (\phi _{P,x})}$${\displaystyle \operatorname {PFP} (\psi _{P,x})}$${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$

このインフレーション固定点は、最小固定点が定義されている場合、最小固定点と一致する。一見すると、インフレーション固定点論理はより広い範囲の固定点引数をサポートするため、最小固定点論理よりも表現力が豊かであるように思われるが、実際には、すべてのFO[IFP]( X )式はFO[LFP]( X )式と同等である。^[10]

これまでに紹介した固定小数点演算子はすべて単一の述語の定義のみを反復処理しましたが、多くのコンピュータプログラムは、複数の述語を同時に反復処理すると考えるのが自然です。固定小数点演算子のアリティを増やすか、またはそれらをネストすることで、すべての同時最小、インフレーション、または部分固定小数は、実際に上記の対応する単一反復構造を使用して表現できます。^[11]

推移的閉包論理では、任意の述語に対する帰納法を許可するのではなく、推移的閉包のみを直接表現できます。

FO[TC]( X ) は、1 階の接続詞と述語、2 階の変数、および推移閉包演算子を使用してXから形成される式の集合であり、これらの演算子は形式 の式を形成するために使用されます。ここで、およびは、互いに異なる 1 階の変数の組、項の組であり、、、およびの長さは一致します。 ${\displaystyle \operatorname {TC} }$${\displaystyle [\operatorname {TC} _{{\vec {x}},{\vec {y}}}\varphi ]{\vec {s}}{\vec {t}}}$${\displaystyle {\vec {x}}}$${\displaystyle {\vec {y}}}$${\displaystyle {\vec {t}}}$${\displaystyle {\vec {s}}}$${\displaystyle {\vec {x}}}$${\displaystyle {\vec {y}}}$${\displaystyle {\vec {s}}}$${\displaystyle {\vec {t}}}$

TC は次のように定義されます。kを正の整数、をk 個の変数のベクトルとします。この場合、となるn個の変数のベクトルが存在し、すべての に対して が真であれば、は真です。ここで、φ はFO(TC) で記述された式であり、変数uとv がxとyに置き換えられることを意味します。 ${\displaystyle u,v,x,y}$${\displaystyle {\mathsf {TC}}(\phi _{u,v})(x,y)}$${\displaystyle (z_{i})}$${\displaystyle z_{1}=x,z_{n}=y}$${\displaystyle i<n}$${\displaystyle \phi (z_{i},z_{i+1})}$${\displaystyle \phi (x,y)}$

順序構造上で、FO[TC]は複雑性クラスNLを特徴づける。^[12]この特徴づけは、NLが補集合に関して閉じている（NL = co-NL）というImmermanの証明の重要な部分である。^[13]

FO[DTC]( X ) は、推移閉包演算子が決定論的である FO(TC,X) として定義されます。つまり、 を適用すると、すべてのuに対して、となるv が最大で 1 つ存在することがわかります。 ${\displaystyle \operatorname {DTC} (\phi _{u,v})}$${\displaystyle \phi (u,v)}$

はの構文糖衣であると仮定できます。 ${\displaystyle \operatorname {DTC} (\phi _{u,v})}$${\displaystyle \operatorname {TC} (\psi _{u,v})}$${\displaystyle \psi (u,v)=\phi (u,v)\wedge \forall x(x=v\vee \neg \phi (u,x))}$

順序構造に対して、FO[DTC]は複雑性クラスLを特徴付ける。^[12]

これまでに定義した固定小数点演算は、固定小数点に到達するまで、式で言及されている述語の帰納的定義を無期限に繰り返します。実装では、計算時間を制限するために反復回数を制限する必要がある場合があります。結果として得られる演算子は、複雑性クラスを特徴付けるためにも使用できるため、理論的な観点からも興味深いものです。

反復を伴う一次関数を定義します。ここでは整数から整数への関数（のクラス）があり、関数の異なるクラスに対しては異なる複雑性クラスが得られます。 ${\displaystyle {\mathsf {FO}}[t(n)]}$${\displaystyle t(n)}$${\displaystyle t(n)}$${\displaystyle {\mathsf {FO}}[t(n)]}$

このセクションでは、 は平均、 は平均と書きます 。まず、量指定子ブロック (QB) を定義する必要があります。量指定子ブロックは、が量指定子のない FO 式で、 がまたは であるリストです。Qが量指定子ブロックの場合、反復演算子を呼び出します。これは、 Q が回数記述されると定義されます。ここで、リストには量指定子がありますが、 k 個の変数のみであり、それらの変数はそれぞれ 回使用されることに注意してください。^[14]${\displaystyle (\forall xP)Q}$${\displaystyle (\forall x(P\Rightarrow Q))}$${\displaystyle (\exists xP)Q}$${\displaystyle (\exists x(P\wedge Q))}$${\displaystyle (Q_{1}x_{1},\phi _{1})...(Q_{k}x_{k},\phi _{k})}$${\displaystyle \phi _{i}}$${\displaystyle Q_{i}}$${\displaystyle \forall }$${\displaystyle \exists }$${\displaystyle [Q]^{t(n)}}$${\displaystyle t(n)}$${\displaystyle k*t(n)}$${\displaystyle t(n)}$

ここで、指数がクラス である反復演算子を持つ FO 式を と定義し、次の等式を得ることができます。 ${\displaystyle {\mathsf {FO}}[t(n)]}$${\displaystyle t(n)}$

• ${\displaystyle {\mathsf {FO}}[(\log n)^{i}]}$はFO均一AC ⁱに等しく、実際は深さ のFO均一ACである。^[15]${\displaystyle {\mathsf {FO}}[t(n)]}$${\displaystyle t(n)}$
• ${\displaystyle {\mathsf {FO}}[(\log n)^{O(1)}]}$NCに等しい。^[16]
• ${\displaystyle {\mathsf {FO}}[n^{O(1)}]}$はPTIMEに等しい。これはFO(IFP)と書く別の方法でもある。^[17]
• ${\displaystyle {\mathsf {FO}}[2^{n^{O(1)}}]}$はPSPACEに等しい。これはFO(PFP)と書く別の方法でもある。^[18]

• エビングハウス、ハインツ＝ディーター。フルム、ヨルグ (1999)。有限モデル理論。数理論理学の視点 (第 2 版)。スプリンガー。土井：10.1007/978-3-662-03182-7。ISBN 978-3-662-03184-1。
• ニール、イマーマン（1999）。記述的複雑性。シュプリンガー。ISBN 0-387-98600-6. OCLC  901297152.