Matching Logic

Matching logic is a first-order logic (FOL) variant designed for specifying and reasoning about structure by means of patterns and pattern matching. Published in Logical Methods in Computer Science (Vol. 13, Issue 4, pp. 1--61, 2017), this paper by Grigore Rosu introduces a logic whose sentences, called patterns, are constructed using variables, symbols, connectives, and quantifiers, but with a crucial departure from FOL: no distinction is made between function symbols and predicate symbols. In classical FOL, function symbols map elements to elements and predicate symbols map elements to truth values, creating a fundamental dichotomy in the syntax and semantics. Matching logic dissolves this distinction by allowing all symbols to be interpreted uniformly as functions from the carrier set to the power set of the carrier set. This seemingly simple generalization has far-reaching consequences, enabling matching logic to uniformly capture several important logical frameworks within a single, coherent formalism.

The semantics of matching logic departs from FOL in a fundamental way. In FOL models, terms evaluate to elements and formulas evaluate to truth values. In matching logic models, every pattern evaluates to a set of elements -- the set of values that "match" the pattern. Formally, given a matching logic model $M$ with carrier set $M_s$ for each sort $s$, the interpretation of a pattern $\varphi$ with respect to a valuation $\rho$ is a subset $\llbracket \varphi \rrbracket_{M,\rho} \subseteq M_s$. Variables $x$ evaluate to the singleton $\{\rho(x)\}$, and symbols $\sigma$ of arity $s_1 \times \ldots \times s_n \to s$ are interpreted as functions $\sigma_M : M_{s_1} \times \ldots \times M_{s_n} \to \mathcal{P}(M_s)$. Application patterns $\sigma(\varphi_1, \ldots, \varphi_n)$ are interpreted by collecting all possible results: $\llbracket \sigma(\varphi_1, \ldots, \varphi_n) \rrbracket = \bigcup \{ \sigma_M(a_1, \ldots, a_n) \mid a_i \in \llbracket \varphi_i \rrbracket \}$. The logical connectives are interpreted as set operations: negation as complement, conjunction as intersection, disjunction as union, and the universal and existential quantifiers as intersection and union over all valuations, respectively.

A central contribution of the paper is the definition of several derived constructs that emerge naturally from the basic matching logic syntax and semantics. The definedness symbol $\lceil \varphi \rceil$ is defined as a pattern that evaluates to the entire carrier set $M_s$ if and only if $\varphi$ matches at least one element (i.e., $\llbracket \varphi \rrbracket \neq \emptyset$), and to the empty set otherwise. Dually, the totality symbol $\lfloor \varphi \rfloor$ evaluates to the full set if and only if $\varphi$ matches every element. From definedness and totality, equality can be defined: $\varphi_1 = \varphi_2$ is an abbreviation for $\lfloor \varphi_1 \leftrightarrow \varphi_2 \rfloor$, meaning two patterns are equal when they match exactly the same elements in every state. Similarly, membership $x \in \varphi$ is defined as $\lceil x \wedge \varphi \rceil$, capturing when an element belongs to the set of values matching a pattern. These derived notions arise purely from the matching logic primitives, without requiring any additional axioms or special constructs.

Matching logic uniformly generalizes several logical frameworks important for program analysis: propositional logic, algebraic specification, first-order logic with equality, modal logic S5 with the global modality, and separation logic.

The paper demonstrates that matching logic subsumes several important logical frameworks as special cases. Propositional logic is captured by considering only propositional patterns (those using connectives and constants). Algebraic specification and equational logic are recovered when symbols are restricted to total functions (singleton-valued interpretations), where term equality coincides with the matching logic equality derived construct. First-order logic with equality is captured by distinguishing between functional patterns (those forced to be singleton-valued via totality axioms) and predicate patterns (those forced to evaluate to either the full set or the empty set via FOL-predicativity axioms). Modal logic S5 with the global modality is captured by interpreting the modality as definedness: $\Diamond \varphi \equiv \lceil \varphi \rceil$, where $\lceil \varphi \rceil$ evaluates to the full set when $\varphi$ is non-empty. Separation logic is captured by encoding the separating conjunction $\ast$ as a binary symbol with the appropriate heap-separating interpretation: $\varphi_1 \ast \varphi_2$ means the heap can be split into two disjoint parts matching $\varphi_1$ and $\varphi_2$ respectively. Crucially, these embeddings preserve the full deductive power of the original logics.

The paper presents a sound and complete proof system for matching logic. The proof system consists of FOL reasoning principles (modus ponens: from $\varphi$ and $\varphi \to \psi$, derive $\psi$; universal generalization: from $\varphi$, derive $\forall x.\, \varphi$; and specialization axioms for propositional tautologies and quantifiers) augmented with two matching logic-specific axioms: Propagation, which states that $C[\bot] = \bot$ for any context $C$ (where $\bot$ denotes the empty pattern), meaning that applying a symbol to an empty pattern yields an empty pattern; and Existence, which states that $\exists x . x$ holds, ensuring that the carrier sets are non-empty. A pattern $\varphi$ is valid, written $\models \varphi$, when $\llbracket \varphi \rrbracket_{M,\rho} = M_s$ for all models $M$ and valuations $\rho$. The soundness theorem states that every provable pattern is valid, and the completeness theorem states that every valid pattern is provable. The completeness proof follows a Henkin-style construction, building a canonical model from a maximally consistent set of patterns.

The paper develops an extensive theory of matching logic specifications. A matching logic specification is a pair $(\Sigma, \Gamma)$ where $\Sigma$ is a signature (sorts and symbols) and $\Gamma$ is a set of axioms (patterns). A model of a specification satisfies all the axioms. The paper shows how to axiomatize various structures using matching logic specifications: partial algebras (where operations may be undefined on some inputs), order-sorted algebras (with subsort relationships), and constrained constructor patterns (which provide a way to specify data types with constraints). The specification theory of matching logic is shown to be strictly more expressive than that of equational logic or even FOL with equality, because matching logic can express structural constraints about pattern matching and definedness that have no direct counterpart in classical logics.

The paper also discusses the application of matching logic to program verification and its role as the logical foundation of the K Framework. In the K Framework, the operational semantics of programming languages is defined using rewrite rules over configurations, and these rules can be expressed as matching logic patterns. Specifically, a rewrite rule $l \Rightarrow r$ in K corresponds to a matching logic pattern asserting that any configuration matching $l$ can transition to a configuration matching $r$. This embedding allows the K Framework's program analysis tools -- including its symbolic execution engine and deductive verifier -- to operate directly on matching logic proofs. The paper notes that matching logic patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that. This flexibility makes matching logic particularly well-suited for reasoning about programs in languages with complex state structures.

The paper concludes by situating matching logic within the broader landscape of logics for computation and by discussing future extensions. The author notes that matching logic has been further extended to matching $\mu$-logic (by Xiaohong Chen and Grigore Rosu, 2019), which adds a least fixpoint $\mu$-binder, enabling the expression of recursive patterns and capturing additional logics such as modal $\mu$-calculus, temporal logics (LTL, CTL, CTL*), and reachability logic. Together, matching logic and its extensions provide the complete logical foundation for Pi2 Labs's Proof of Proof technology: the mathematical proofs generated during verified computation are matching logic proofs, and the universal proof checker at the heart of Proof of Proof checks the validity of these proofs using the matching logic proof calculus. This connection between a foundational logic and a practical verifiable computing system represents a rare instance of deep theoretical work finding direct application in industrial-scale software infrastructure.