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. Matching logic is the logical foundation of the K framework.

History

Early development

The term "matching logic" was coined in 2009. 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.

Formalization as a standalone logic

The first paper that establishes matching logic as a standalone formal logic was published in 2017. 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.

More recently, researchers have shown increasing interest in simplifying matching logic to a bare minimum. 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''.

Variants

We list them below in the chronological order:
# "Matching logic”, which is a many-sorted logic but has no fixpoint operators.
# "Matching $\mu$-logic", which extends the LMCS’17 formalization with fixpoint operators and proof rules.
# "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.

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 $\mu$-logic. Then, we will present the other formalizations as variants.

Formal definition

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

Syntax

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

Signatures and variables

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

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

Patterns

Matching logic formulas are called ''patterns''. The set of $(S,\Sigma)$-patterns, or simply patterns, is an $S$-indexed set $\mathrm = _$. We write $\varphi_s \in \mathrm$ or $\varphi \in \mathrm_s$ to denote a pattern of a sort $s$. The set of all patterns is inductively defined by the following grammar rules:
* $x : s \in \mathrm_s$.
* $X : s \in \mathrm_s$.
* $\sigma(\varphi_,\dots,\varphi_) \in \mathrm_s$ for any $\sigma \in \Sigma$.
* $\bot_s \in \mathrm_s$.
* $\varphi_s \to \varphi'_s \in \mathrm_s$.
* $\exists x : s' \cdot \varphi_s \in \mathrm_s$. Note that $s'$ and $s$ need not be the same.
* $\mu X : s \cdot \varphi_s \in \mathrm_s$ if $\varphi_s$ is positive in $X : s$.

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

Common notations

Notations can be defined in the usual way. The following are some standard notations:
* $\neg \varphi_s \equiv \varphi_s \to \bot_s$
* $\top_s \equiv \neg \bot_s$
* $\varphi_s \lor \varphi'_s \equiv \neg\varphi_s \to \varphi'_s$
* $\varphi_s \land \varphi'_s \equiv \neg(\neg \varphi_s \land \neg\varphi'_s)$
* $\varphi_s \leftrightarrow \varphi_s' \equiv (\varphi_s \to \varphi'_s) \land (\varphi_s \to \varphi'_s)$
* $\forall x : s' \cdot \varphi_s \equiv \neg \exists x : s' \cdot \neg \varphi_s$
* \nu X : s \cdot \varphi_s \equiv \neg \mu X : s \cdot \neg \varphi_s neg X : s / X : s/math>

Here, \varphi_s neg X : s / X : s/math> is the result of substituting every occurrence of $X : s$ for its negation $\neg X : s$. One can verify that $\nu X : s \cdot \varphi_s$ is well-formed if $\varphi_s$ is positive in $X : s$.

Semantics

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

Interpretation of patterns

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

Let $(S,\Sigma)$ be a signature. An $(S,\Sigma)$-model, or simply a model, is denoted $M = (\_, _)$. It consists of:
* A nonempty carrier set $M_s$ for every $s \in S$.
* A function $\sigma_M : M_ \times \dots \times M_ \to \mathcal(M_s)$ for every $\sigma \in \Sigma_$.

Here, $\mathcal(M_s)$ denotes the power set of $M_s$.

A valuation $\rho$ maps every element variable of sort $s$ to an element in $M_s$. It also maps every set element of sort $s$ to a subset of $M_s$. That is, $\rho(x : s) \in M_s$ and $\rho(X : s) \subseteq M_s$. Given a model $M$ and a valuation $\rho$, the interpretation of a pattern is $\mathrm_ \subseteq M_s$. This interpretation is inductively defined in the following way:
* $\mathrm \left\vert \right\vert _ =$
* $\mathrm\left\vert X : s \right\vert _ = \rho(X : s)$
* $\mathrm\left\vert \sigma(\varphi_,\dots,\varphi_) \right\vert _ = \bigcup_ \dots \bigcup_ \sigma_M(a_1,\dots,a_n)$
* $\mathrm\left\vert \bot_x \right\vert _ = \emptyset$, the empty set.
* $\mathrm\left\vert \varphi_s \to \varphi'_s \right\vert _ = M_s \setminus (\mathrm\left\vert \varphi_s \right\vert _ \setminus \mathrm\left\vert \varphi'_s \right\vert _)$, where “$\setminus$” denotes set difference.
* $\mathrm\left\vert \exists x : s' \cdot \varphi_s \right\vert _ = \bigcup_ \mathrm\left\vert \varphi_s \right\vert _$, where \rho / x : s'/math> is the valuation that is identical to $\rho$ except that it maps to $x : s'$ to $a$.
* $\mathrm\left\vert \mu X : s \cdot \varphi_s \right\vert _ = \bigcap \$

Fixpoints and properties

By the Knaster-Tarski Fixpoint Theorem, $\mu X : s \cdot \varphi_s$ is the least fixpoint of the function that maps $A \subseteq M_s$ to $\mathrm\left\vert \varphi_s \right\vert_$.

The following properties hold for common notations:
* $\mathrm\left\vert \neg \varphi_s \right\vert _ = M_s \setminus \mathrm\left\vert \varphi_s \right\vert _$
* $\mathrm\left\vert \top_s \right\vert _ = M_s$
* $\mathrm\left\vert \varphi_s \lor \varphi'_s \right\vert _ = \mathrm\left\vert \varphi_s \right\vert _ \cup \mathrm\left\vert \varphi'_s \right\vert _$
* $\mathrm\left\vert \varphi_s \land \varphi'_s \right\vert _ = \mathrm\left\vert \varphi_s \right\vert _ \cap \mathrm\left\vert \varphi'_s \right\vert _$
* $\mathrm\left\vert \varphi_s \leftrightarrow \varphi'_s \right\vert _ = M_s \setminus (\mathrm\left\vert \varphi_s \right\vert _ \Delta \mathrm\left\vert \varphi'_s \right\vert _)$, where “$\Delta$” denotes the symmetric difference operator.
* $\mathrm\left\vert \forall x : s' \cdot \varphi_s \right\vert _ = \bigcap_ \mathrm\left\vert \varphi_s \right\vert _$
* $\mathrm\left\vert \nu X : s \cdot \varphi_s \right\vert _ = \bigcup \$

Applications

Matching logic is used with reachability logic 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.

See also

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

References

{{Reflist

Logic