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.

Symbol	Unicode	Name	Meaning
⟦φ⟧	—	Extension	Matched elements
∧	U+2227	And	Intersection
¬	U+00AC	Not	Complement
x, y	—	Element variable	Denotes a singleton
X, Y	—	Set variable	Denotes any subset
∃	U+2203	Exists	Binds element variables
μ	U+03BC	Least fixed point	Binds set variables, positive occurrence
⌈·⌉	—	Definedness	Non-empty
·	—	Application	Symbol application
=	—	Equality	Same extension

Metatheory. Complete proof system exists. Subsumes FOL (encode predicates). Subsumes modal logic. Subsumes separation logic. Rewriting reducible to matching logic. Foundation for K Framework language semantics.

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

Limitations. Recent — tool support developing. Abstract: learning curve. Subsumption encodings non-trivial. Community smaller than established logics. Theory still being developed.