Matching μ-Logic

This paper, authored by Xiaohong Chen and Grigore Rosu and published at LICS 2019 (the 34th Annual ACM/IEEE Symposium on Logic in Computer Science), makes two fundamental contributions to the theory of matching logic. First, it proposes a sound and complete proof system $\mathsf{H}$ for matching logic in its full generality, resolving a significant open problem since previous completeness results were limited to specific theories providing equality and membership. Second, it introduces matching $\mu$-logic, an extension of matching logic with a least fixpoint $\mu$-binder. The $\mu$-binder $\mu X.\, \varphi$ allows the definition of recursive patterns, enabling matching $\mu$-logic to capture as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal $\mu$-logic, dynamic logic, various temporal logics (including infinite-trace and finite-trace linear temporal logic, and computation tree logic), and notably reachability logic --- the logic underlying program verification in the K framework. Matching $\mu$-logic thus serves as a unifying foundation for specifying and reasoning about fixpoints, induction, programming language semantics, and program verification.

Matching logic was introduced by Grigore Rosu as a logic for specifying and reasoning about mathematical structures by means of patterns and pattern matching. Unlike classical first-order logic, where formulas evaluate to truth values, matching logic patterns are interpreted as the sets of elements that they match. This set-valued semantics provides a natural framework for expressing both structural properties (like "the term has the form $f(x, y)$") and logical properties (like "for all $x$, $P(x)$ holds") within a single formalism. Matching logic was originally developed as the logical foundation for the K framework, a rewrite-based framework for defining programming language semantics, but its scope extends far beyond programming languages.

Prior to this paper, the proof theory of matching logic was incomplete in general. Sound and complete deduction had been established only for matching logic theories that include specific axioms defining equality and membership, which restricted the class of models to which the completeness result applied. This limitation was problematic because many important applications of matching logic --- including its use as a foundation for the K framework --- require reasoning in theories that do not necessarily include equality and membership axioms. The first contribution of this paper addresses this gap by proposing the proof system $\mathsf{H}$, which is sound and complete for all matching logic theories. The second contribution, the extension to matching $\mu$-logic, is motivated by the observation that many important logical systems used in program verification and formal methods are based on fixpoints, and that matching logic's pattern-based formalism is naturally suited to incorporate fixpoint reasoning.

The syntax of matching logic is parametric in a signature $(EV, SV, \Sigma)$ consisting of a set $EV$ of element variables $x, y, z, \ldots$, a set $SV$ of set variables $X, Y, Z, \ldots$, and a set $\Sigma$ of constant symbols $\sigma$. Patterns $\varphi$ are defined by the grammar:

$\varphi \;::=\; x \;\mid\; X \;\mid\; \sigma \;\mid\; \varphi_1 \; \varphi_2 \;\mid\; \bot \;\mid\; \varphi_1 \to \varphi_2 \;\mid\; \exists x.\, \varphi$

Here, $x$ is an element variable (matching a single element), $X$ is a set variable (matching a set of elements), $\sigma$ is a constant symbol, $\varphi_1 \; \varphi_2$ is application (a crucial construct that generalizes both function application and symbol application), $\bot$ is the empty pattern, $\to$ is implication, and $\exists x.\, \varphi$ is existential quantification. The remaining standard connectives are derived: $\neg \varphi \equiv \varphi \to \bot$, $\varphi_1 \vee \varphi_2 \equiv \neg \varphi_1 \to \varphi_2$, $\varphi_1 \wedge \varphi_2 \equiv \neg(\neg \varphi_1 \vee \neg \varphi_2)$, $\top \equiv \neg \bot$, and $\forall x.\, \varphi \equiv \neg \exists x.\, \neg \varphi$.

The semantics of matching logic is given by matching logic models $(M, \cdot_M)$, where $M$ is a non-empty carrier set and $\cdot_M$ assigns to each constant symbol $\sigma$ a subset $\sigma_M \subseteq M$. An $M$-valuation $\rho$ maps element variables to elements of $M$ and set variables to subsets of $M$. The interpretation $\llbracket \varphi \rrbracket_{M, \rho} \subseteq M$ of a pattern $\varphi$ is defined inductively:

$\llbracket x \rrbracket_{M,\rho} = \{\rho(x)\} \qquad \llbracket X \rrbracket_{M,\rho} = \rho(X) \qquad \llbracket \sigma \rrbracket_{M,\rho} = \sigma_M$ $\llbracket \varphi_1\; \varphi_2 \rrbracket_{M,\rho} = \{b \in M \mid \exists a \in \llbracket \varphi_1 \rrbracket_{M,\rho},\; (a, b) \in \llbracket \varphi_2 \rrbracket_{M,\rho}\} \text{ (application)}$ $\llbracket \bot \rrbracket_{M,\rho} = \emptyset \qquad \llbracket \varphi_1 \to \varphi_2 \rrbracket_{M,\rho} = (M \setminus \llbracket \varphi_1 \rrbracket_{M,\rho}) \cup \llbracket \varphi_2 \rrbracket_{M,\rho}$ $\llbracket \exists x.\, \varphi \rrbracket_{M,\rho} = \bigcup_{a \in M} \llbracket \varphi \rrbracket_{M, \rho[x \mapsto a]}$

A pattern $\varphi$ is valid in a model $M$ (written $M \vDash \varphi$) if $\llbracket \varphi \rrbracket_{M,\rho} = M$ for all valuations $\rho$, meaning that every element of $M$ matches $\varphi$. A pattern is satisfiable if $\llbracket \varphi \rrbracket_{M,\rho} \neq \emptyset$ for some model and valuation.

The proof system $\mathsf{H}$ is a Hilbert-style deduction system for matching logic consisting of axiom schemas and inference rules. The axioms include the standard propositional tautologies (since matching logic subsumes propositional logic through the pattern algebra), the axioms for the existential quantifier (adapted from first-order logic), and crucially, a set of axioms that govern the interaction between application and the logical connectives. The key axioms specific to matching logic include:

• Propagation of $\bot$: $\bot \; \varphi \leftrightarrow \bot$ and $\varphi \; \bot \leftrightarrow \bot$
• Propagation of $\vee$: $(\varphi_1 \vee \varphi_2) \; \varphi_3 \leftrightarrow (\varphi_1 \; \varphi_3) \vee (\varphi_2 \; \varphi_3)$
• Propagation of $\exists$: $(\exists x.\, \varphi_1) \; \varphi_2 \leftrightarrow \exists x.\, (\varphi_1 \; \varphi_2)$ when $x \notin \text{FV}(\varphi_2)$
• Framing: from $\varphi_1 \to \varphi_2$, derive $C[\varphi_1] \to C[\varphi_2]$ for any context $C$

The inference rules include modus ponens ($\varphi_1, \varphi_1 \to \varphi_2 \vdash \varphi_2$), universal generalization ($\varphi \vdash \forall x.\, \varphi$ when $x$ is not free in any hypothesis), and the set variable generalization rule. The soundness of $\mathsf{H}$ is proved by showing that every axiom is valid in all matching logic models and that the inference rules preserve validity. The completeness is proved by a Henkin-style construction: from a consistent theory $\Gamma$ and a pattern $\varphi$ not derivable from $\Gamma$, a model is constructed in which all patterns in $\Gamma$ are valid but $\varphi$ is not. The completeness proof requires careful handling of the set-valued semantics and the interaction between element variables and set variables.

Matching $\mu$-logic extends matching logic with the least fixpoint operator $\mu X.\, \varphi$, where $X$ is a set variable and $\varphi$ is a pattern in which $X$ occurs positively (i.e., under an even number of negations). The positivity requirement ensures the existence of the least fixpoint by the Knaster-Tarski theorem. The syntax of matching $\mu$-logic extends the matching logic grammar with:

$\varphi \;::=\; \cdots \;\mid\; \mu X.\, \varphi \qquad (X \text{ positive in } \varphi)$

The semantics of the $\mu$-binder is the standard least fixpoint semantics:

$\llbracket \mu X.\, \varphi \rrbracket_{M,\rho} = \bigcap \{A \subseteq M \mid \llbracket \varphi \rrbracket_{M, \rho[X \mapsto A]} \subseteq A\}$

That is, $\mu X.\, \varphi$ is interpreted as the intersection of all pre-fixpoints of the operator $F(A) = \llbracket \varphi \rrbracket_{M, \rho[X \mapsto A]}$. The greatest fixpoint $\nu X.\, \varphi$ is defined dually: $\nu X.\, \varphi \equiv \neg \mu X.\, \neg \varphi[\neg X / X]$. The proof system for matching $\mu$-logic extends $\mathsf{H}$ with the pre-fixpoint axiom and the Knaster-Tarski (Park) induction rule:

• Pre-fixpoint: $\varphi[\mu X.\, \varphi / X] \to \mu X.\, \varphi$
• Knaster-Tarski: from $\varphi[\psi/X] \to \psi$, derive $\mu X.\, \varphi \to \psi$

The pre-fixpoint axiom says that $\mu X.\, \varphi$ is a pre-fixpoint (unfolding the definition is valid), and the Knaster-Tarski rule says that $\mu X.\, \varphi$ is the least pre-fixpoint (any other pre-fixpoint contains it). Together, these capture the complete deductive theory of least fixpoints.

The paper's most striking result is the demonstration that matching $\mu$-logic captures numerous important logics as special instances. Each logic is obtained by choosing an appropriate matching logic signature and axioms, and then expressing the logic's formulas as matching $\mu$-logic patterns:

• First-order logic (FOL): Classical FOL is a special case where all patterns are interpreted as either $\emptyset$ or $M$ (i.e., patterns are "predicate-like"). This is achieved by adding a definedness axiom: $\lceil x \rceil = \top$, which forces every singleton to be "total." Under this axiom, matching logic collapses to FOL, and the $\mu$-binder gives FOL extended with least fixpoints (LFP).
• Modal $\mu$-logic: By adding a modal signature with a binary relation symbol $R$ (the accessibility relation), the modal operators $\Box \varphi \equiv \forall y.\, (R(x, y) \to \varphi[y/x])$ and $\Diamond \varphi \equiv \exists y.\, (R(x, y) \wedge \varphi[y/x])$ can be defined. The $\mu$-binder then gives the full modal $\mu$-calculus, which subsumes all standard modal and temporal logics.
• Linear temporal logic (LTL): Both infinite-trace LTL and finite-trace LTL are instances. The temporal operators are defined using fixpoints: $\Diamond \varphi \equiv \mu X.\, (\varphi \vee \bigcirc X)$ ("eventually $\varphi$") and $\Box \varphi \equiv \nu X.\, (\varphi \wedge \bigcirc X)$ ("always $\varphi$"), where $\bigcirc$ is the "next" operator.
• Computation Tree Logic (CTL): CTL's branching-time operators, including $\mathsf{EF}\, \varphi$ (there exists a path where eventually $\varphi$) and $\mathsf{AG}\, \varphi$ (on all paths, always $\varphi$), are defined as fixpoints over the transition relation.
• Dynamic logic: The modality $\langle \alpha \rangle \varphi$ ("after executing program $\alpha$, $\varphi$ holds") is expressible, with iteration (Kleene star) captured via the $\mu$-binder: $\langle \alpha^* \rangle \varphi \equiv \mu X.\, (\varphi \vee \langle \alpha \rangle X)$.

Perhaps the most significant application of matching $\mu$-logic is the capture of reachability logic, the logic that underpins program verification in the K framework. Reachability logic allows the specification and verification of program behavior by expressing reachability claims of the form $\varphi \Rightarrow^\bullet \psi$, meaning "any program configuration matching pattern $\varphi$ will eventually reach (in zero or more steps) a configuration matching pattern $\psi$." Reachability logic generalizes Hoare logic: the Hoare triple $\{P\}\; C \;\{Q\}$ can be expressed as the reachability claim $\langle P, C \rangle \Rightarrow^\bullet \langle Q, \cdot \rangle$, where the first component is the state predicate and the second is the remaining computation.

In matching $\mu$-logic, a reachability claim $\varphi \Rightarrow^\bullet \psi$ is expressed using the least fixpoint:

$\varphi \to \mu X.\, (\psi \vee \bigcirc X)$

This says: starting from any configuration matching $\varphi$, either $\psi$ already holds, or after one step ($\bigcirc$), the property $X$ holds --- and by the least fixpoint, this must eventually terminate with $\psi$ holding. The one-step transition $\bigcirc$ is defined using the language's operational semantics (the K rewrite rules). The paper proves that the proof system of matching $\mu$-logic, when instantiated with the axioms corresponding to a K language definition, yields exactly the proof rules of reachability logic. This result is foundational for the K framework, because it means that the K verifier's reasoning is grounded in a sound and complete logic, and that all of K's verification capabilities are instances of matching $\mu$-logic reasoning.

Matching $\mu$-logic serves as the logical foundation of the K framework. In K, a programming language is defined by its syntax, configuration, and rewrite rules. The semantics of a K definition can be formalized as a matching $\mu$-logic theory, where the rewrite rules become axioms expressing one-step transitions. The K verifier proves reachability claims (program specifications) by constructing matching $\mu$-logic proofs, using the rewrite rules as axioms and the fixpoint induction rule as the source of loop invariant reasoning.

The paper establishes that this connection is not merely an analogy but a precise mathematical correspondence. Every K rewrite rule $l \Rightarrow r$ (with side conditions) translates to a matching $\mu$-logic axiom $\forall \bar{x}.\, (l \wedge \text{conditions} \to \bigcirc r)$. Every program property proved by the K verifier corresponds to a theorem of matching $\mu$-logic. This means that every program verification performed in K is, at its core, a matching $\mu$-logic proof, even though the user interacts with K at a much higher level of abstraction. The result provides a strong foundational justification for the K approach to program verification and opens the door to cross-verification: proofs generated by the K verifier can, in principle, be checked by an independent matching $\mu$-logic proof checker. This connection between K and matching $\mu$-logic is central to the Proof of Proof ($\pi^2$) technology developed by Pi2 Labs, which generates cryptographic proofs from matching logic proof certificates.

The paper makes two contributions of lasting significance to the foundations of formal methods. The sound and complete proof system $\mathsf{H}$ for matching logic resolves a fundamental question about the proof theory of this logic and provides a solid deductive foundation for all applications of matching logic. The extension to matching $\mu$-logic, with its ability to capture first-order logic with fixpoints, modal $\mu$-logic, temporal logics, dynamic logic, and reachability logic, establishes matching $\mu$-logic as one of the most expressive and unifying logics in the formal methods landscape.

The practical implications of matching $\mu$-logic are far-reaching. By providing a single logical framework that subsumes the many different logics used in program verification, matching $\mu$-logic simplifies the foundations of verification tools and enables cross-language and cross-logic reasoning. The connection to the K framework means that language-independent program verification can be grounded in a single, well-understood logic. The paper opens numerous directions for future work, including the development of automated proof tactics for matching $\mu$-logic, the investigation of decidability fragments, and the application of matching $\mu$-logic to new domains such as probabilistic programs and quantum computing. Matching $\mu$-logic represents a significant step toward the vision of a universal logic for programming languages and formal verification.