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.φ | φ₁ · φ₂ (application)

Variables are patterns, symbols applied to patterns give patterns.

Semantics: Interpretation ρ: Var → P(M). ⟦x⟧ρ = ρ(x) ⟦σ(φ₁,...,φₙ)⟧ρ = {σ(a₁,...,aₙ) : aᵢ ∈ ⟦φᵢ⟧ρ} ⟦¬φ⟧ρ = M \ ⟦φ⟧ρ ⟦φ ∧ ψ⟧ρ = ⟦φ⟧ρ ∩ ⟦ψ⟧ρ ⟦∃x.φ⟧ρ = ⋃{⟦φ⟧ρ[x↦A] : A ⊆ M}

Definedness: ⌈φ⌉ = "φ is defined" (matches something) ⌈φ⌉ = ¬(φ ∧ ¬φ) ... actually: pattern that is ⊤ iff ⟦φ⟧ ≠ ∅

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
∃	U+2203	Exists	Union over assignments
⌈·⌉	—	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.