MatchingLogic.Semantics

def MatchingLogic.FV {S : Signature} {Var : Type} : Pattern S Var → Set Var

The free variables of a pattern. ∃x binds x.

Equations

• MatchingLogic.FV (MatchingLogic.Pattern.var x_1) = {x_1}
• MatchingLogic.FV MatchingLogic.Pattern.bot = ∅
• MatchingLogic.FV (MatchingLogic.Pattern.app σ f) = ⋃ (i : Fin (S.arity σ)), MatchingLogic.FV (f i)
• MatchingLogic.FV (φ.imp ψ) = MatchingLogic.FV φ ∪ MatchingLogic.FV ψ
• MatchingLogic.FV (MatchingLogic.Pattern.ex x_1 φ) = MatchingLogic.FV φ \ {x_1}

def MatchingLogic.Closed {S : Signature} {Var : Type} (φ : Pattern S Var) : Prop

A pattern is closed when it has no free variables. The paper assumes throughout Sections 3-5 that Γ and φ are closed, without loss of generality.

Equations

• MatchingLogic.Closed φ = (MatchingLogic.FV φ = ∅)

@[simp]

theorem MatchingLogic.FV_var {S : Signature} {Var : Type} (x : Var) : FV (Pattern.var x) = {x}

@[simp]

theorem MatchingLogic.FV_bot {S : Signature} {Var : Type} : FV Pattern.bot = ∅

@[simp]

theorem MatchingLogic.FV_imp {S : Signature} {Var : Type} (φ ψ : Pattern S Var) : FV (φ.imp ψ) = FV φ ∪ FV ψ

@[simp]

theorem MatchingLogic.FV_app {S : Signature} {Var : Type} (σ : S.Sym) (f : Fin (S.arity σ) → Pattern S Var) : FV (Pattern.app σ f) = ⋃ (i : Fin (S.arity σ)), FV (f i)

@[simp]

theorem MatchingLogic.FV_ex {S : Signature} {Var : Type} (x : Var) (φ : Pattern S Var) : FV (Pattern.ex x φ) = FV φ \ {x}

theorem MatchingLogic.denote_congr {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (φ : Pattern S Var) (ρ ρ' : Var → M.carrier) : (∀ x ∈ FV φ, ρ x = ρ' x) → M.denote ρ φ = M.denote ρ' φ

The denotation depends on a valuation only through the free variables.

theorem MatchingLogic.denote_closed {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) {φ : Pattern S Var} (hφ : Closed φ) (ρ ρ' : Var → M.carrier) : M.denote ρ φ = M.denote ρ' φ

For a closed pattern the denotation does not depend on the valuation at all; this is what licenses the paper's ⟦ψ⟧ notation.

Definition 1: totality and the three consequence relations

def MatchingLogic.Model.Total {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (φ : Pattern S Var) : Prop

φ is total in M under ρ when ρ(φ) = M.

Equations

• M.Total ρ φ = (M.denote ρ φ = Set.univ)

def MatchingLogic.Model.Sat {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (φ : Pattern S Var) : Prop

M ⊨ φ: φ is total in M under every valuation.

Equations

• M.Sat φ = ∀ (ρ : Var → M.carrier), M.Total ρ φ

def MatchingLogic.Model.SatSet {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (Γ : Set (Pattern S Var)) : Prop

M ⊨ Γ.

Equations

• M.SatSet Γ = ∀ γ ∈ Γ, M.Sat γ

def MatchingLogic.Model.denoteSet {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (Δ : Set (Pattern S Var)) : Set M.carrier

ρ(Δ) = ⋂_{δ ∈ Δ} ρ(δ), with value M when Δ = ∅.

Equations

• M.denoteSet ρ Δ = ⋂ δ ∈ Δ, M.denote ρ δ

def MatchingLogic.LocalCons {S : Signature} {Var : Type} [DecidableEq Var] (Δ : Set (Pattern S Var)) (φ : Pattern S Var) : Prop

Δ ⊨loc φ: local consequence, comparing denotations pointwise.

Equations

• MatchingLogic.LocalCons Δ φ = ∀ (M : MatchingLogic.Model S) (ρ : Var → M.carrier), M.denoteSet ρ Δ ⊆ M.denote ρ φ

def MatchingLogic.GlobalCons {S : Signature} {Var : Type} [DecidableEq Var] (Γ : Set (Pattern S Var)) (φ : Pattern S Var) : Prop

Γ ⊨ φ: global consequence, asking for totality.

Equations

• MatchingLogic.GlobalCons Γ φ = ∀ (M : MatchingLogic.Model S), M.SatSet Γ → M.Sat φ

theorem MatchingLogic.Model.sat_iff_denote_eq_univ {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) {φ : Pattern S Var} (hφ : Closed φ) (ρ : Var → M.carrier) : M.Sat φ ↔ M.denote ρ φ = Set.univ

For closed φ, M ⊨ φ says exactly ⟦φ⟧ = M, with no valuation quantifier left (paper, Section 2, "Closed patterns").