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 μ {\displaystyle \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 μ {\displaystyle \mu } -logic. Then, we will present the other formalizations as variants.
Formal definition Matching μ {\displaystyle \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 , Σ ) {\displaystyle (S,\Sigma )} that has a set S {\displaystyle S} of sorts and an ( S ∗ × S ) {\displaystyle (S^{*}\times S)} -indexed set Σ {\displaystyle \Sigma } of many-sorted symbols, or simply symbols. A symbol σ ∈ Σ s 1 … s n , s {\displaystyle \sigma \in \Sigma _{s_{1}\dots s_{n},s}} means that it takes n {\displaystyle n} arguments of sorts s 1 {\displaystyle s_{1}} , ..., s n {\displaystyle s_{n}} , respectively, and returns a value of sort s {\displaystyle s} . Let ( S , Σ ) {\displaystyle (S,\Sigma )} be a many-sorted signature. Let E V = { E V s } s ∈ S {\displaystyle \mathrm {EV} ={\mathrm {\{EV} _{s}\}}_{s\in S}} and S V = { S V s } s ∈ S {\displaystyle \mathrm {SV} ={\mathrm {\{SV} _{s}\}}_{s\in S}} be two disjoint families of S {\displaystyle S} -indexed sets of variables. We call elements in E V {\displaystyle \mathrm {EV} } element variables, denoted x : s {\displaystyle x:s} , y : s {\displaystyle y:s} , ... and elements in S V {\displaystyle \mathrm {SV} } set variables, denoted X : s {\displaystyle X:s} , Y : s {\displaystyle Y:s} , ...
… excerpt ends here. Continue reading the full article.
