Loading article…
数理論理学において、モナド二階論理（MSO）は、二階量化が集合上の量化に限定されている二階論理の一部である。 [1]これは、木幅が制限されたグラフ上でモナド二階論理式を評価するアルゴリズムを提供するクールセルの定理のため、グラフの論理において特に重要である。また、オートマトン理論においても根本的に重要であり、ビュッヒ・エルゴット・トラクテンブロートの定理により正規言語の論理的特徴付けが行われている。
2 階論理では、述語の量化が可能です。ただし、MSO は、 2 階の量化がモナド述語 (単一の引数を持つ述語) に限定されているフラグメントです。モナド述語は、表現力においてセット (述語が真となる要素のセット) と同等であるため、これは「セット」の量化として説明されることがよくあります。
バリエーション
モナドの二階述語論理には 2 つのバリエーションがあります。グラフなどの構造やクールセルの定理で考慮されるバリエーションでは、式には非モナド述語 (この場合はバイナリ エッジ述語) が含まれる場合がありますが、量化はモナド述語に対してのみ制限されます。オートマトン理論や Büchi–Elgot–Trakhtenbrot 定理で考慮されるバリエーションでは、式自体の述語も含め、すべての述語は、等式 ( ) と順序関係 ( ) を除いてモナドである必要があります。
評価の計算の複雑さ
存在モナド二階論理 (EMSO) は MSO の一部であり、集合上のすべての量指定子は、式の他の部分を除いて、存在量指定子でなければなりません。一階量指定子には制限がありません。存在 (非モナド) 二階論理が複雑性クラスNPの記述的複雑性を正確に捉えるというFagin の定理との類推により、存在モナド二階論理で表現できる問題のクラスは、モナド NP と呼ばれています。モナド論理への制限により、非モナド二階論理では証明されていない分離をこの論理で証明することができます。たとえば、グラフの論理では、グラフが切断されているかどうかをテストすることはモナド NP に属します。これは、テストが、グラフの残りの部分に接続する辺を持たない頂点の適切なサブセットの存在を記述する式で表すことができるためです。しかし、グラフが連結されているかどうかをテストする相補的な問題は、モナドNPには属さない。[2] [3]相補的な問題の類似したペアの存在（そのうちの1つだけが存在する2階の論理式を持つ問題（モナド論理式に制限されない））は、NPとcoNPの不等式と同等であり、計算複雑性に関する未解決の問題である。
対照的に、ブールMSO式が入力有限木によって満たされるかどうかをチェックしたい場合、ブールMSO式を木オートマトン[4]に変換し、木上でオートマトンを評価することにより、この問題は木内で線形時間で解決できます。ただし、クエリの観点から見ると、このプロセスの複雑さは一般に非基本的です。[5]クールセルの定理のおかげで、グラフの木幅が定数で制限されている場合、入力グラフ上でブールMSO式を線形時間で評価することもできます。
自由変数を持つMSO式では、入力データが木であるか、木幅が制限されている場合、すべての解の集合を生成する効率的な列挙アルゴリズムがあり、 [6]入力データが線形時間で前処理され、各解が各解のサイズに線形な遅延で生成されることを保証します。つまり、クエリのすべての自由変数が1階変数である（つまり、集合を表さない）一般的なケースでは、一定遅延です。その場合、MSO式の解の数を数える効率的なアルゴリズムもあります。[7]
決定可能性と充足可能性の複雑さ
モナド二階述語論理の充足可能性問題は、この論理が一階述語論理を包含するため、一般に決定不可能である。
無限完全二分木のモナド的二階理論（S2S）は決定可能である。[8] この結果から、以下の理論は決定可能である。
- 木のモナドの二次理論。
- 後継者不足のモナド的二次理論(S1S)。
- WS2S と WS1S は、量化を有限部分集合に制限します (弱いモナド二階論理)。バイナリ数 (部分集合で表される) の場合、WS1S でも加算を定義できることに注意してください。
これらの理論（S2S、S1S、WS2S、WS1S）のそれぞれにおいて、意思決定問題の複雑さは非基本的である。[5] [9]
検証における木上のMSOの充足可能性の使用
モナド二階木の論理は形式検証に応用されている。MSO充足可能性の決定手順[10][ 11] [12]は、リンクされたデータ構造を操作するプログラムの特性を証明するために使用され、[13]形状解析の一形態として、またハードウェア検証における記号推論に使用されている。[14]
参照
参考文献
- ^ Courcelle, Bruno ; Engelfriet, Joost (2012-01-01). グラフ構造とモナディック2階論理: 言語理論的アプローチ。ケンブリッジ大学出版局。ISBN 978-0521898331. 2016年9月15日閲覧。
- ^ Fagin、Ronald (1975)、「Monadic generalized spectra」、Zeitschrift für Mathematische Logik und Grundlagen der Mathematik、21 : 89–96、doi :10.1002/malq.19750210112、MR 0371623。
- ^ Fagin, R. ; Stockmeyer, L. ; Vardi, MY (1993)、「モナディック NP とモナディック コ NP について」、第 8 回年次構造複雑性理論会議議事録、電気電子技術者協会、doi :10.1109/sct.1993.336544、S2CID 32740047。
- ^ Thatcher, JW; Wright, JB (1968-03-01). 「一般化有限オートマトン理論と2階論理の決定問題への応用」.数学システム理論. 2 (1): 57–81. doi :10.1007/BF01691346. ISSN 1433-0490. S2CID 31513761.
- ^ ab Meyer, Albert R. (1975). Parikh, Rohit (ed.). 「後継者の弱いモナドの2階理論は初等再帰的ではない」. Logic Colloquium . Lecture Notes in Mathematics. Springer Berlin Heidelberg: 132–154. doi :10.1007/bfb0064872. ISBN 9783540374831。
- ^ Bagan, Guillaume (2006). Ésik, Zoltán (ed.). 「ツリー分解可能構造の MSO クエリは線形遅延で計算可能」.コンピュータ サイエンス ロジック. コンピュータ サイエンスの講義ノート. 4207. Springer Berlin Heidelberg: 167–181. doi :10.1007/11874683_11. ISBN 9783540454595。
- ^ アーンボーグ、ステファン;ラガーグレン、イェンス。ゼーセ、デトレフ (1991-06-01)。 「木分解可能なグラフの簡単な問題」。アルゴリズムのジャーナル。12 (2): 308–340。土井：10.1016/0196-6774(91)90006-K。ISSN 0196-6774。
- ^ ラビン、マイケル O. (1969)。 「無限木上の第 2 次理論とオートマトンの選択可能性」。アメリカ数学会誌。141 : 1–35。doi :10.2307/1995086。ISSN 0002-9947。JSTOR 1995086 。
- ^ Stockmeyer, Larry; Meyer, Albert R. (2002-11-01). 「論理における小さな問題の回路複雑度の宇宙論的下限」Journal of the ACM . 49 (6): 753–784. doi :10.1145/602220.602223. ISSN 0004-5411. S2CID 15515064.
- ^ ヘンリクセン、ジェスパー G.ジェンセン、ジェイコブ。ヨルゲンセン、マイケル。クラールンド、ニルス。ロバート、ペイジ。ラウエ、タイス。サンドホルム、アンダース (1995)。ブリンクスマ、E.クリーブランド、WR;ラーセン、KG;マルガリア、T . ;ステフェン、B. (編)。 「Mona: モナド二次論理の実践」。システムの構築と分析のためのツールとアルゴリズム。コンピューターサイエンスの講義ノート。1019 .ベルリン、ハイデルベルク：シュプリンガー：89–110。土井: 10.1007/3-540-60630-0_5。ISBN 978-3-540-48509-4。
- ^ フィエドル、トマーシュ;ホーリク、ルカーシュ。レンガル、オンドジェ;ヴォジナル、トマーシュ (2019-04-01)。 「WS1S のネストされたアンチチェーン」。アクタ・インフォマティカ。56 (3): 205–228。土井：10.1007/s00236-018-0331-z。ISSN 1432-0525。S2CID 57189727。
- ^ Traytel, Dmitriy; Nipkow, Tobias (2013-09-25). 「正規表現の派生語に基づく単語のMSOの検証済み決定手順」ACM SIGPLAN Notices . 48 (9): 3–f12. doi :10.1145/2544174.2500612. hdl : 20.500.11850/106053 . ISSN 0362-1340.
- ^ Møller, Anders; Schwartzbach, Michael I. (2001-05-01). 「ポインターアサーションロジックエンジン」。プログラミング言語の設計と実装に関する ACM SIGPLAN 2001 会議の議事録。PLDI '01。ユタ州スノーバード、米国: 計算機協会。pp. 221–231。doi : 10.1145 /378795.378851。ISBN 978-1-58113-414-8. S2CID 11476928。
- ^ Basin, David; Klarlund, Nils (1998-11-01). 「ハードウェア検証におけるオートマトンベースの記号推論」.システム設計における形式手法. 13 (3): 255–288. doi :10.1023/A:1008644009416. ISSN 0925-9856.