マッチングロジック

マッチングロジックは、主にコンピュータプログラムとその正しさを規定し推論するために考案された形式体系の一種です。一階述語論理などの古典論理と比較すると、マッチングロジックの式（パターン）は、要素ではなく、基盤となるキャリア集合の冪集合として解釈されます。パターンは、それに「一致する」要素の集合によって一致するという直感に基づいています。このように、マッチングロジックはパターンマッチングに基づく意味論を許容すると言われています。

マッチングロジックは、当初グリゴレ・ロシュ氏によって考案され、2019年にシャオホン・チェン氏によって完成されました。^{[ 1 ]}マッチングロジックは、Kフレームワークの論理的基盤です。^{[ 2 ]}

歴史

初期の開発

「マッチングロジック」という用語は2009年に造語され^{[ 3 ]}、それ以来、いくつかの形式体系を指すために使用されてきました。初期の文献では、マッチングロジックはコンピュータプログラムの構成を規定し、推論するための形式体系として表現されていました。一連の規則と組み合わせることで、コンピュータプログラムの動的な動作を規定し、推論するために使用されました。

後者は後に到達可能性論理へと発展しました。これは言語に依存しない形式体系であり、固定数の規則で構成され、あらゆるプログラミング言語に対して健全かつ比較的完全な形式検証機能を提供します。これらの文献では、マッチング論理は到達可能性論理の独立した構成要素として提示されています。

独立した論理としての形式化

マッチング論理を独立した形式論理として確立した最初の論文は2017年に発表されました。^{[ 4 ]}そこで、マッチング論理の構文、意味論、証明体系は初めて独立した定義を与えられました。2019年には、マッチング論理に固定点構成子と証明規則が追加されました。^{[ 5 ]}

近年、研究者たちはマッチングロジックを必要最小限にまで簡素化することにますます関心を寄せています。^{[ 6 ]}彼らは、このプロセスにおいてマッチングロジックの表現力を損なうことなく、その形式化を維持することを目指しています。これらの形式化はすべて今日の文献に存在し、「マッチングロジック」という同じ名前で登場することもあります。

変種

以下に時系列順に列挙します。

1. 「マッチングロジック」は多ソートロジックだが、固定点演算子を持たない。^{[ 4 ]}
2. 「マッチング論理」は、LMCS'17の形式化を固定点演算子と証明規則で拡張したものです。^{[ 5 ]}${\displaystyle \mu}$
3. 「応用マッチングロジック」は、署名に1つのソートと、バイナリシンボルである1つの非定数シンボルのみを含めることを要求する制限されたフラグメントです。^{[ 6 ]}

それ以来、「マッチング論理」という用語は、文献において上記の形式化のいずれを指す場合にも使用されてきました。混乱を避けるため、ここでは最も完全なバージョンであるマッチング論理の形式化について説明し、その後、他の形式化を変種として紹介します。 ${\displaystyle \mu}$

正式な定義

マッチングロジックは、以下に詳述する構文とセマンティクスを通じて定義されます。 ${\displaystyle \mu}$

構文

マッチングロジックの構文は、変数、シンボル、論理接続詞を使用してパターンを構築する方法を指定します。

署名と変数

マッチングロジックは、ソートの集合と、 -インデックス付きでソートされたシンボル（または単にシンボル）の集合を持つ、多ソートシグネチャに基づいてパラメトリックに実行されます。シンボルとは、それぞれソート、... 、を引数として取り、ソートの値を返すことを意味します。 ${\displaystyle (S,\Sigma )}$ ${\displaystyle S}$ ${\displaystyle (S^{*}\times S)}$ ${\displaystyle \Sigma }$ ${\displaystyle \sigma \in \Sigma _{s_{1}\dots s_{n},s}}$ ${\displaystyle n}$ ${\displaystyle s_{1}}$ ${\displaystyle s_{n}}$ ${\displaystyle s}$

を多ソート署名とする。 と を、添字付き変数集合の互いに素な2つの族とする。要素変数の要素を 、 、…と表記し、集合変数の要素を、 、… と表記する。 ${\displaystyle (S,\Sigma )}$ ${\displaystyle \mathrm {EV} ={\mathrm {\{EV} _{s}\}}_{s\in S}}$ ${\displaystyle \mathrm {SV} ={\mathrm {\{SV} _{s}\}}_{s\in S}}$ ${\displaystyle S}$ ${\displaystyle \mathrm {EV} }$ ${\displaystyle x:s}$ ${\displaystyle y:s}$ ${\displaystyle \mathrm {SV} }$ ${\displaystyle X:s}$ ${\displaystyle Y:s}$

パターン

マッチングロジック式はパターンと呼ばれます。 -パターン、または単にパターンの集合は、 -添字付き集合です。ある種のパターンを表すには、 または と書きます。すべてのパターンの集合は、以下の文法規則によって帰納的に定義されます。 ${\displaystyle (S,\Sigma )}$ ${\displaystyle S}$ ${\displaystyle \mathrm {パターン} ={\mathrm {\{パターン} _{s}\}}_{s\in S}}$ ${\displaystyle \varphi _{s}\in \mathrm {パターン} }$ ${\displaystyle \varphi \in \mathrm {パターン} _{s}}$ ${\displaystyle s}$

• ${\displaystyle x:s\in \mathrm {Pattern} _{s}}$ 。
• ${\displaystyle X:s\in \mathrm {Pattern} _{s}}$ 。
• ${\displaystyle \sigma (\varphi _{s_{1}},\dots ,\varphi _{s_{n}})\in \mathrm {Pattern} _{s}}$ 任意の。${\displaystyle \sigma \in \Sigma {s_{1}\dots s_{n},s}}$
• ${\displaystyle \bot _{s}\in \mathrm {Pattern} _{s}}$ 。
• ${\displaystyle \varphi _{s}\to \varphi '_{s}\in \mathrm {Pattern} _{s}}$ 。
• ${\displaystyle \exists x:s'\cdot \varphi _{s}\in \mathrm {Pattern} _{s}}$ とは同じである必要はないことに注意してください。${\displaystyle s'}$ ${\displaystyle s}$
• ${\displaystyle \mu X:s\cdot \varphi _{s}\in \mathrm {Pattern} _{s}}$ が正の場合。${\displaystyle \varphi _{s}}$ ${\displaystyle X:s}$

ここで、 は、のすべての出現が偶数個の含意の左辺内に存在する場合、 において正となります。例えば、は において正ですが、 では正ではありません。一方、は において正ですが、 では正ではありません。 ${\displaystyle \varphi _{s}}$ ${\displaystyle X:s}$ ${\displaystyle X:s}$ ${\displaystyle X:s\to Y:s}$ ${\displaystyle Y:s}$ ${\displaystyle X:s}$ ${\displaystyle (X:s\to Y:s)\to X:s}$ ${\displaystyle X:s}$ ${\displaystyle Y:s}$

一般的な表記

表記法は通常の方法で定義できます。以下に標準的な表記法をいくつか示します。

• ${\displaystyle \neg \varphi _{s}\equiv \varphi _{s}\to \bot _{s}}$
• ${\displaystyle \top _{s}\equiv \neg \bot _{s}}$
• ${\displaystyle \varphi _{s}\lor \varphi '_{s}\equiv \neg \varphi _{s}\to \varphi '_{s}}$
• ${\displaystyle \varphi _{s}\land \varphi '_{s}\equiv \neg (\neg \varphi _{s}\land \neg \varphi '_{s})}$
• ${\displaystyle \varphi _{s}\leftrightarrow \varphi _{s}'\equiv (\varphi _{s}\to \varphi '_{s})\land (\varphi _{s}\to \varphi '_{s})}$
• ${\displaystyle \forall x:s'\cdot \varphi _{s}\equiv \neg \exists x:s'\cdot \neg \varphi _{s}}$
• ${\displaystyle \nu X:s\cdot \varphi _{s}\equiv \neg \mu X:s\cdot \neg \varphi _{s}[\neg X:s/X:s]}$

ここで、は のすべての出現をその否定に置き換えた結果です。が において正であれば、 が整形式であることを確認できます。 ${\displaystyle \varphi _{s}[\neg X:s/X:s]}$ ${\displaystyle X:s}$ ${\displaystyle \neg X:s}$ ${\displaystyle \nu X:s\cdot \varphi _{s}}$ ${\displaystyle \varphi _{s}}$ ${\displaystyle X:s}$

セマンティクス

マッチング ロジックのセマンティクスは、モデルと評価に基づいてパターンがどのように解釈されるかを定義します。

パターンの解釈

パターンと呼ばれるマッチングロジック式は、真偽値ではなく集合として解釈されます。直感的に言えば、マッチングロジックパターンは、それに「一致する」要素の集合として解釈されます。 ${\displaystyle \varphi }$

をシグネチャとする。-モデル、あるいは単にモデルは と表記される。これは以下の要素から構成される。 ${\displaystyle (S,\Sigma )}$ ${\displaystyle (S,\Sigma )}$ ${\displaystyle M=(\{{M_{s}}\}_{s\in S},{\{\sigma _{M}\}}_{\sigma \in \Sigma })}$

• すべての の空でないキャリア セット。${\displaystyle M_{s}}$ ${\displaystyle s\in S}$
• あらゆる に対する関数。${\displaystyle \sigma _{M}:M_{s_{1}}\times \dots \times M_{s_{n}}\to {\mathcal {P}}(M_{s})}$ ${\displaystyle \sigma \in \Sigma _{s_{1}\dots s_{n},s}}$

ここで、は の冪集合を表します。 ${\displaystyle {\mathcal {P}}(M_{s})}$ ${\displaystyle M_{s}}$

評価は、 のすべての要素変数を の要素にマッピングします。また、 のすべての集合要素をのサブセットにマッピングします。つまり、および です。モデルと評価 が与えられた場合、パターンの解釈は です。この解釈は、次のように帰納的に定義されます。 ${\displaystyle \rho }$ ${\displaystyle s}$ ${\displaystyle M_{s}}$ ${\displaystyle s}$ ${\displaystyle M_{s}}$ ${\displaystyle \rho (x:s)\in M_{s}}$ ${\displaystyle \rho (X:s)\subseteq M_{s}}$ ${\displaystyle M}$ ${\displaystyle \rho }$ ${\displaystyle \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }\subseteq M_{s}}$

• ${\displaystyle \mathrm {} \left\vert {x:s}\right\vert _{M,\rho }={\{\rho (x:s)}\}}$
• ${\displaystyle \mathrm {} \left\vert X:s\right\vert _{M,\rho }=\rho (X:s)}$
• ${\displaystyle \mathrm {\left\vert \sigma (\varphi _{s_{1}},\dots ,\varphi _{s_{n}})\right\vert } _{M,\rho }=\bigcup _{a_{1}\in \mathrm {\left\vert \varphi _{s_{1}}\right\vert } _{M,\rho }}\dots \bigcup _{a_{n}\in \mathrm {\left\vert \varphi _{s_{n}}\right\vert } _{M,\rho }}\sigma _{M}(a_{1},\dots ,a_{n})}$
• ${\displaystyle \mathrm {} \left\vert \bot _{x}\right\vert _{M,\rho }=\emptyset }$ 、空集合。
• ${\displaystyle \mathrm {\left\vert \varphi _{s}\to \varphi '_{s}\right\vert } _{M,\rho }=M_{s}\setminus (\mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }\setminus \mathrm {\left\vert \varphi '_{s}\right\vert } _{M,\rho })}$ ここで、「」は集合差を表します。${\displaystyle \setminus }$
• ${\displaystyle \mathrm {} \left\vert \exists x:s'\cdot \varphi _{s}\right\vert _{M,\rho }=\bigcup _{a\in M_{s'}}\mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho [a/x:s']}}$ 、は にマッピングされることを除いてと同一の評価です。${\displaystyle \rho [a/x:s']}$ ${\displaystyle \rho }$ ${\displaystyle x:s'}$ ${\displaystyle a}$
• ${\displaystyle \mathrm {} \left\vert \mu X:s\cdot \varphi _{s}\right\vert _{M,\rho }=\bigcap \{{A\subseteq M_{s}\mid \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho [A/X:s]}\subseteq A}\}}$

不動点とプロパティ

クナスター・タルスキー不動点定理により、は にマッピングされる関数の最小の不動点です。 ${\displaystyle \mu X:s\cdot \varphi _{s}}$ ${\displaystyle A\subseteq M_{s}}$ ${\displaystyle \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho [A/X:s]}}$

一般的な表記法には次の特性が当てはまります。

• ${\displaystyle \mathrm {\left\vert \neg \varphi _{s}\right\vert } _{M,\rho }=M_{s}\setminus \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }}$
• ${\displaystyle \mathrm {\left\vert \top _{s}\right\vert } _{M,\rho }=M_{s}}$
• ${\displaystyle \mathrm {\left\vert \varphi _{s}\lor \varphi '_{s}\right\vert } _{M,\rho }=\mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }\cup \mathrm {\left\vert \varphi '_{s}\right\vert } _{M,\rho }}$
• ${\displaystyle \mathrm {\left\vert \varphi _{s}\land \varphi '_{s}\right\vert } _{M,\rho }=\mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }\cap \mathrm {\left\vert \varphi '_{s}\right\vert } _{M,\rho }}$
• ${\displaystyle \mathrm {\left\vert \varphi _{s}\leftrightarrow \varphi '_{s}\right\vert } _{M,\rho }=M_{s}\setminus (\mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }\Delta \mathrm {\left\vert \varphi '_{s}\right\vert } _{M,\rho })}$ ここで、「」は対称差分演算子を表します。${\displaystyle \Delta }$
• ${\displaystyle \mathrm {} \left\vert \forall x:s'\cdot \varphi _{s}\right\vert _{M,\rho }=\bigcap _{a\in M_{s'}}\mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho [a/x:s']}}$
• ${\displaystyle \mathrm {} \left\vert \nu X:s\cdot \varphi _{s}\right\vert _{M,\rho }=\bigcup \{{A\subseteq M_{s}\mid A\subseteq \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho [A/X:s]}\subseteq A}\}}$

アプリケーション

マッチングロジックは、Kフレームワークによって到達可能性ロジック^{[ 7 ]}とともに使用され、操作的意味論を指定して形式検証に直接使用することができ、ホーアロジックの代替アプローチを形成します。

マッチング論理の不動点フリーフラグメントは、等式を含む一階述語論理に変換できます。この変換により、Kフレームワークは既存の充足可能性法理論（SMT）ソルバーを使用できるようになります。これらのソルバーは、定理の証明を見つけるのに役立ちます。

参照

• 分離ロジック
• ホーア論理
• 文字列のセットに一致する正規表現

参考文献

1. Chen, Xiaohong; Roșu, Grigore (2019-01-19). 「Matching μ-Logic」イリノイ大学研究技術レポート(コンピュータサイエンス).
2. ロシュ、グリゴレ;フロリン・シェルバヌータ、トライアン（2010 年 8 月）。「K セマンティック フレームワークの概要」。論理と代数プログラミングのジャーナル。79 (6): 397–434。
3. Rosu, Grigore; Schulte, Wolfram (2009). 「マッチングロジック - 拡張レポート」イリノイ大学アーバナ・シャンペーン校.
4. Rosu, Grigore (2017-12-20). 「マッチングロジック」 .コンピュータサイエンスにおける論理的手法. 13 (4). arXiv : 1705.06312 . doi : 10.23638/LMCS-13(4:28)2017 . ISSN 1860-5974 . 
5. Chen, Xiaohong; Roşu, Grigore (2021-06-08). 「Matching μ-logic」 . Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science . LICS '19. Vancouver, Canada: IEEE Press: 1–13 .
6. Chen, Xiaohong; Lucanu, Dorel; Roşu, Grigore (2021-04-01). 「マッチングロジックの説明」 . Journal of Logical and Algebraic Methods in Programming . 120 100638. doi : 10.1016/j.jlamp.2021.100638 . hdl : 2142/107794 . ISSN 2352-2208 . 
7. ロシュ、グリゴレ; ̧Řtefănescu、アンドレイ;チョバカ、シュテファン。ムーア、ブランドン M. (2012)。「到達可能性ロジック」。イリノイ大学技術レポート。