Matching Logic

Origin. Roșu introduced Matching Logic (2017). Unifying framework: FOL, modal logics, separation logic, rewriting. Patterns match (sets of) elements. Foundation for K Framework. Aims to be "the" logic for programming language semantics.

Models. Patterns over algebras. Standard FOL: formulas denote truth values. Matching logic: patterns denote sets of elements they match. Unifies terms (match one element) and formulas (match all satisfying elements). Subsumes many logics.

Formalism.

Syntax: Patterns: φ ::= x | X | σ(φ₁,...,φₙ) | ¬φ | φ₁ ∧ φ₂ | ∃x.φ | μX.φ | φ₁ · φ₂ (application)

Variables are patterns, symbols applied to patterns give patterns.

Two sorts of variable: Element variables x, y: ρ(x) ∈ M. Set variables X, Y: ρ(X) ⊆ M. The distinction is essential and cannot be collapsed — element variables are what ∃ binds, set variables are what μ binds.

Semantics: Every pattern evaluates to a subset of the carrier M. ⟦x⟧ρ = {ρ(x)} — a singleton, since x names one element ⟦X⟧ρ = ρ(X) — an arbitrary subset ⟦σ(φ₁,...,φₙ)⟧ρ = {σ(a₁,...,aₙ) : aᵢ ∈ ⟦φᵢ⟧ρ} ⟦¬φ⟧ρ = M \ ⟦φ⟧ρ ⟦φ ∧ ψ⟧ρ = ⟦φ⟧ρ ∩ ⟦ψ⟧ρ ⟦∃x.φ⟧ρ = ⋃{⟦φ⟧ρ[x↦a] : a ∈ M} — a ranges over elements; letting it range over subsets would make ∃ second-order and erase the element sort ⟦μX.φ⟧ρ = least fixed point of A ↦ ⟦φ⟧ρ[X↦A], defined when X occurs only positively in φ. Fixed points over set variables are what give matching logic recursion and induction.

Definedness: ⌈φ⌉ = "φ is defined", i.e. φ matches something. ⟦⌈φ⌉⟧ρ = M if ⟦φ⟧ρ ≠ ∅, and ∅ otherwise. Definedness is a designated symbol with its own axiom (⌈x⌉ = ⊤ for element variables x), not an abbreviation built from ¬ and ∧ — no propositional combination can test emptiness, since ¬ and ∧ act pointwise on extensions. Totality ⌊φ⌋ = ¬⌈¬φ⌉, membership x ∈ φ = ⌈x ∧ φ⌉, and equality all derive from it.

Equality: φ = ψ means they match same elements.

Subsumes:

• FOL: predicates as patterns matching elements
• Modal: □φ via frame encoding
• Separation: * via heap composition symbol
• Rewriting: φ ⇒ ψ encoded

Symbols.

Metatheory. A pattern denotes the set of elements it matches, so validity means denoting the whole carrier in every model. Roșu (LMCS 2017) gave a Hilbert-style proof system for matching logic and proved it sound and complete; the argument is Henkin-style and turns on the definedness symbol ⌈·⌉, from which membership, equality and totality are all derived, and which no propositional combination of ¬ and ∧ can define, since those act pointwise on extensions. First-order logic embeds via the predicate patterns — those whose extension is always ∅ or M — and the embedding is faithful, so first-order validity is a lower bound on matching logic validity. Chen and Roșu (LICS 2019) added least and greatest fixed points; matching μ-logic captures the modal μ-calculus, LTL, CTL, separation logic and reachability logic as theories over a signature, and, being strong enough to axiomatize arithmetic, admits no complete recursively enumerable proof system.

Applies to. Programming language semantics (K Framework). Language-independent verification. Rewriting-based systems. Unifying logical frameworks. Formal methods tools.

Limitations. The subsumption results are embeddings into matching logic theories, not identifications: separation logic or LTL becomes a signature plus axioms, and nothing about the source logic travels with it — its decision procedures, complexity bounds and proof automation have to be rebuilt over the pattern language. Validity is undecidable already in the fixpoint-free fragment, since first-order logic embeds faithfully, and matching μ-logic axiomatizes arithmetic, so the fixpoints that make induction and recursion expressible are exactly what forfeits completeness. μX.φ requires X positive in φ, so recursion through negation is not expressible at all. In the K Framework, what a verified program is verified against is the K definition of the language, and the fidelity of that definition to a real compiler is outside what the logic addresses.

© 2026 Lingenic LLC