Matching logic

Matching logic is a family of formal systems that were created mainly to specify and reason about computer programs and their correctness. Compared to classical logics such as first-order logic, matching logic's formulas, called patterns, are interpreted as, not elements, but power sets of the underlying carrier set(s), with the intuition that a pattern is matched by the set of elements that "match" it. This way, matching logic is said to admit a semantics based on pattern matching.

Matching logic was initially coined by Grigore Rosu and finalized with Xiaohong Chen in 2019.^[1] Matching logic is the logical foundation of the K framework.^[2]

The term "matching logic" was coined in 2009.^[3] and has been used to refer to a couple of formal systems since then. In the early days, matching logic was represented in the literature as a formal system to specify and reason about computer programs' configurations. Together with a set of rules, it was used to specify and reason about the dynamic behaviors of computer programs.

The latter was later developed into reachability logic, which is a language-agnostic formal system with a fixed number of rules that provides sound and relatively complete formal verification capability for all programming languages. In these works of literature, matching logic is presented as an independent component of reachability logic.

The first paper that establishes matching logic as a standalone formal logic was published in 2017.^[4] There, matching logic was given an independent definition of its syntax, semantics, and proof system for the first time. In 2019, fixpoint constructors and proof rules were added to matching logic.^[5]

More recently, researchers have shown increasing interest in simplifying matching logic to a bare minimum.^[6] They aim to keep its expressive power intact during this process. All these formalizations exist in today's literature and sometimes appear under the same name "matching logic''.

We list them below in the chronological order:

1. "Matching logic”, which is a many-sorted logic but has no fixpoint operators.^[4]
2. "Matching ${\displaystyle \mu }$-logic", which extends the LMCS’17 formalization with fixpoint operators and proof rules.^[5]
3. "Applicative matching logic", which is a restricted fragment that requires the signatures to include only one sort and only one non-constant symbol that is a binary symbol.^[6]

Since then, the term "matching logic" has been used to refer to any of the above formalizations in the literature. To avoid confusion, we shall present the formalization of the most complete version, matching ${\displaystyle \mu }$-logic. Then, we will present the other formalizations as variants.

Matching ${\displaystyle \mu }$-logic is defined through its syntax and semantics, which are detailed below.

The syntax of matching logic specifies how patterns are constructed using variables, symbols, and logical connectives.

Matching logic is parametric on a many-sorted signature ${\displaystyle (S,\Sigma )}$ that has a set ${\displaystyle S}$ of sorts and an ${\displaystyle (S^{*}\times S)}$-indexed set ${\displaystyle \Sigma }$ of many-sorted symbols, or simply symbols. A symbol ${\displaystyle \sigma \in \Sigma _{s_{1}\dots s_{n},s}}$ means that it takes ${\displaystyle n}$ arguments of sorts ${\displaystyle s_{1}}$, ..., ${\displaystyle s_{n}}$, respectively, and returns a value of sort ${\displaystyle s}$.

Let ${\displaystyle (S,\Sigma )}$ be a many-sorted signature. Let ${\displaystyle \mathrm {EV} ={\mathrm {\{EV} _{s}\}}_{s\in S}}$ and ${\displaystyle \mathrm {SV} ={\mathrm {\{SV} _{s}\}}_{s\in S}}$ be two disjoint families of ${\displaystyle S}$-indexed sets of variables. We call elements in ${\displaystyle \mathrm {EV} }$ element variables, denoted ${\displaystyle x:s}$, ${\displaystyle y:s}$, ... and elements in ${\displaystyle \mathrm {SV} }$ set variables, denoted ${\displaystyle X:s}$, ${\displaystyle Y:s}$, ...

Matching logic formulas are called patterns. The set of ${\displaystyle (S,\Sigma )}$-patterns, or simply patterns, is an ${\displaystyle S}$-indexed set ${\displaystyle \mathrm {Pattern} ={\mathrm {\{Pattern} _{s}\}}_{s\in S}}$. We write ${\displaystyle \varphi _{s}\in \mathrm {Pattern} }$ or ${\displaystyle \varphi \in \mathrm {Pattern} _{s}}$ to denote a pattern of a sort ${\displaystyle s}$. The set of all patterns is inductively defined by the following grammar rules:

• ${\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}}$ for any ${\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}}$. Note that ${\displaystyle s'}$ and ${\displaystyle s}$ need not be the same.
• ${\displaystyle \mu X:s\cdot \varphi _{s}\in \mathrm {Pattern} _{s}}$ if ${\displaystyle \varphi _{s}}$ is positive in ${\displaystyle X:s}$.

Here, ${\displaystyle \varphi _{s}}$ is positive in ${\displaystyle X:s}$ if every occurrence of ${\displaystyle X:s}$ lies within an even number of implication left-hand sides. For example, ${\displaystyle X:s\to Y:s}$ is positive in ${\displaystyle Y:s}$ but not in ${\displaystyle X:s}$. In contrast, ${\displaystyle (X:s\to Y:s)\to X:s}$ is positive in ${\displaystyle X:s}$ but not in ${\displaystyle Y:s}$.

Notations can be defined in the usual way. The following are some standard notations:

• ${\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]}$

Here, ${\displaystyle \varphi _{s}[\neg X:s/X:s]}$ is the result of substituting every occurrence of ${\displaystyle X:s}$ for its negation ${\displaystyle \neg X:s}$. One can verify that ${\displaystyle \nu X:s\cdot \varphi _{s}}$ is well-formed if ${\displaystyle \varphi _{s}}$ is positive in ${\displaystyle X:s}$.

The semantics of matching logic defines how patterns are interpreted over models and valuations.

Matching logic formulas, called patterns, are interpreted not as true/false values, but as sets. Intuitively, a matching logic pattern ${\displaystyle \varphi }$ is interpreted as the set of elements that “match” it.

Let ${\displaystyle (S,\Sigma )}$ be a signature. An ${\displaystyle (S,\Sigma )}$-model, or simply a model, is denoted ${\displaystyle M=(\{{M_{s}}\}_{s\in S},{\{\sigma _{M}\}}_{\sigma \in \Sigma })}$. It consists of:

• A nonempty carrier set ${\displaystyle M_{s}}$ for every ${\displaystyle s\in S}$.
• A function ${\displaystyle \sigma _{M}:M_{s_{1}}\times \dots \times M_{s_{n}}\to {\mathcal {P}}(M_{s})}$ for every ${\displaystyle \sigma \in \Sigma _{s_{1}\dots s_{n},s}}$.

Here, ${\displaystyle {\mathcal {P}}(M_{s})}$ denotes the power set of ${\displaystyle M_{s}}$.

A valuation ${\displaystyle \rho }$ maps every element variable of sort ${\displaystyle s}$ to an element in ${\displaystyle M_{s}}$. It also maps every set element of sort ${\displaystyle s}$ to a subset of ${\displaystyle M_{s}}$. That is, ${\displaystyle \rho (x:s)\in M_{s}}$ and ${\displaystyle \rho (X:s)\subseteq M_{s}}$. Given a model ${\displaystyle M}$ and a valuation ${\displaystyle \rho }$, the interpretation of a pattern is ${\displaystyle \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho }\subseteq M_{s}}$. This interpretation is inductively defined in the following way:

• ${\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 }$, the empty set.
• ${\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 })}$, where “${\displaystyle \setminus }$” denotes set difference.
• ${\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']}}$, where ${\displaystyle \rho [a/x:s']}$ is the valuation that is identical to ${\displaystyle \rho }$ except that it maps to ${\displaystyle x:s'}$ to ${\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}\}}$

By the Knaster-Tarski Fixpoint Theorem, ${\displaystyle \mu X:s\cdot \varphi _{s}}$ is the least fixpoint of the function that maps ${\displaystyle A\subseteq M_{s}}$ to ${\displaystyle \mathrm {\left\vert \varphi _{s}\right\vert } _{M,\rho [A/X:s]}}$.

The following properties hold for common notations:

• ${\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 })}$, where “${\displaystyle \Delta }$” denotes the symmetric difference operator.
• ${\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}\}}$

Matching logic is used with reachability logic^[7] by the K Framework to specify operational semantics and use them directly for formal verification, which forms an alternative approach to Hoare logic.

The fixpoint-free fragment of matching logic can be converted to first-order logic with equality. This conversion allows the K Framework to use existing Satisfiability modulo theories (SMT) solvers. These solvers help to find proofs for theorems.

• Separation logic
• Hoare logic
• Regular expression, which matches sets of strings