RSRL descriptions

This file defines the description language of RSRL and its satisfaction relation. A formula assigns a sort to a term, equates two terms, applies a relation symbol to variables, or combines formulae with the classical connectives and with quantifiers. The quantifiers range over the components of the described entity rather than over the whole universe. A grammar is a list of formulae, its principles, and an interpretation is a model of a grammar when every principle holds of every entity.

Richter reserves the word description for a formula without free variables, and observes that the denotation of a description does not depend on the variable assignment. The file proves that observation. It also proves that a sort assignment is monotone in the sort, which is what makes a constraint on a sort hold of the entities of every subsort.

Main definitions

• HPSG.RSRL.Desc: a formula of the description language.
• HPSG.RSRL.Desc.freeVars: the variables that occur free in a formula.
• HPSG.RSRL.Interpretation.Satisfies: an entity satisfies a formula under a variable assignment.
• HPSG.RSRL.Grammar: a list of principles.
• HPSG.RSRL.Interpretation.Models: every entity satisfies every principle of the grammar.
• HPSG.RSRL.Constraint: a principle that requires the entities of one sort to satisfy a formula.
• HPSG.RSRL.Constraint.inherited: the constraints of a list that a sort inherits.

Main results

• HPSG.RSRL.Interpretation.satisfies_congr: satisfaction depends only on the values that the assignment gives to the free variables.
• HPSG.RSRL.Interpretation.models_iff_forall_assignment: a model of a grammar of closed formulae satisfies them under every assignment.
• HPSG.RSRL.Interpretation.forall_satisfies_map_toDesc_iff: an entity satisfies a list of constraints exactly when it satisfies the constraints that its sort inherits.

Implementation notes

A relational formula applies a relation symbol to exactly as many variables as its arity, as in Richter's syntax. A term is passed to a relation by binding it to a quantified variable first. Models evaluates each principle at the entity u under the constant assignment fun _ ↦ u, so that it is decidable on a finite universe. For closed principles the choice of assignment is immaterial by models_iff_forall_assignment.

References

• [Ric00]
• [Ric24]

inductive HPSG.RSRL.Desc {Srt : Type u} [PartialOrder Srt] (Sig : Signature Srt) : Type u

A formula of the description language ([Ric24], Definition 4).

• sortAssign {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (t : Term Sig) (σ : Srt) : Desc Sig

  The sort assignment t ∼ σ says that t denotes an entity whose sort is at least as specific as σ.

• pathEq {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (t₁ t₂ : Term Sig) : Desc Sig

  The path equation t₁ ≈ t₂ says that t₁ and t₂ denote the same entity.

• rel {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (ρ : Sig.Rel) (xs : Fin (Sig.arity ρ) → ℕ) : Desc Sig

  The relational formula ρ(x₁, …, xₙ) says that the values of the variables stand in the relation ρ.

• neg {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (d : Desc Sig) : Desc Sig

  Negation.

• and {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (d e : Desc Sig) : Desc Sig

  Conjunction.

• or {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (d e : Desc Sig) : Desc Sig

  Disjunction.

• imp {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (d e : Desc Sig) : Desc Sig

  Classical implication.

• ex {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (x : ℕ) (d : Desc Sig) : Desc Sig

  The formula ex x d says that d holds when x is some component of the described entity.

• all {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (x : ℕ) (d : Desc Sig) : Desc Sig

  The formula all x d says that d holds when x is any component of the described entity.

def HPSG.RSRL.Desc.iff {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (d e : Desc Sig) : Desc Sig

The biconditional of two formulae.

Equations

• d.iff e = (d.imp e).and (e.imp d)

def HPSG.RSRL.Desc.freeVars {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : Desc Sig → Finset ℕ

The variables that occur free in a formula ([Ric24], Definition 5).

Equations

• (HPSG.RSRL.Desc.sortAssign t σ).freeVars = t.freeVars
• (HPSG.RSRL.Desc.pathEq t₁ t₂).freeVars = t₁.freeVars ∪ t₂.freeVars
• (HPSG.RSRL.Desc.rel ρ xs).freeVars = Finset.image xs Finset.univ
• d.neg.freeVars = d.freeVars
• (d.and e).freeVars = d.freeVars ∪ e.freeVars
• (d.or e).freeVars = d.freeVars ∪ e.freeVars
• (d.imp e).freeVars = d.freeVars ∪ e.freeVars
• (HPSG.RSRL.Desc.ex x_1 d).freeVars = d.freeVars.erase x_1
• (HPSG.RSRL.Desc.all x_1 d).freeVars = d.freeVars.erase x_1

@[simp]

theorem HPSG.RSRL.Desc.freeVars_iff {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (d e : Desc Sig) : (d.iff e).freeVars = d.freeVars ∪ e.freeVars

Satisfaction

def HPSG.RSRL.Interpretation.Satisfies {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) (g : ℕ → U) (u : U) : Desc Sig → Prop

The entity u satisfies a formula under the assignment g ([Ric24], Definition 14). An atomic formula with an undefined term is false.

Equations

• I.Satisfies g u (HPSG.RSRL.Desc.sortAssign t σ) = ∃ v ∈ I.termDenot g t u, I.S v ≤ σ
• I.Satisfies g u (HPSG.RSRL.Desc.pathEq t₁ t₂) = ∃ v ∈ I.termDenot g t₁ u, v ∈ I.termDenot g t₂ u
• I.Satisfies g u (HPSG.RSRL.Desc.rel ρ xs) = I.R ρ fun (i : Fin (Sig.arity ρ)) => g (xs i)
• I.Satisfies g u d.neg = ¬I.Satisfies g u d
• I.Satisfies g u (d.and e) = (I.Satisfies g u d ∧ I.Satisfies g u e)
• I.Satisfies g u (d.or e) = (I.Satisfies g u d ∨ I.Satisfies g u e)
• I.Satisfies g u (d.imp e) = (I.Satisfies g u d → I.Satisfies g u e)
• I.Satisfies g u (HPSG.RSRL.Desc.ex x_1 d) = ∃ (w : U), I.IsComponentOf u w ∧ I.Satisfies (Function.update g x_1 w) u d
• I.Satisfies g u (HPSG.RSRL.Desc.all x_1 d) = ∀ (w : U), I.IsComponentOf u w → I.Satisfies (Function.update g x_1 w) u d

@[instance_reducible]

instance HPSG.RSRL.Interpretation.decidableSatisfies {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) [Fintype U] [DecidableEq U] [DecidableLE Srt] [Fintype Sig.Attr] [(ρ : Sig.Rel) → DecidablePred (I.R ρ)] (g : ℕ → U) (u : U) (d : Desc Sig) : Decidable (I.Satisfies g u d)

Equations

• I.decidableSatisfies g u (HPSG.RSRL.Desc.sortAssign t σ) = (I.termDenot g t u).decidableExistsMem
• I.decidableSatisfies g u (HPSG.RSRL.Desc.pathEq t₁ t₂) = (I.termDenot g t₁ u).decidableExistsMem
• I.decidableSatisfies g u (HPSG.RSRL.Desc.rel ρ xs) = ⋯.mpr inferInstance
• I.decidableSatisfies g u d.neg = ⋯.mpr inferInstance
• I.decidableSatisfies g u (d.and e) = ⋯.mpr inferInstance
• I.decidableSatisfies g u (d.or e) = ⋯.mpr inferInstance
• I.decidableSatisfies g u (d.imp e) = ⋯.mpr inferInstance
• I.decidableSatisfies g u (HPSG.RSRL.Desc.ex x_1 d) = ⋯.mpr inferInstance
• I.decidableSatisfies g u (HPSG.RSRL.Desc.all x_1 d) = ⋯.mpr inferInstance

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_sortAssign {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {t : Term Sig} {σ : Srt} : I.Satisfies g u (Desc.sortAssign t σ) ↔ ∃ v ∈ I.termDenot g t u, I.S v ≤ σ

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_pathEq {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {t₁ t₂ : Term Sig} : I.Satisfies g u (Desc.pathEq t₁ t₂) ↔ ∃ v ∈ I.termDenot g t₁ u, v ∈ I.termDenot g t₂ u

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_rel {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {ρ : Sig.Rel} {xs : Fin (Sig.arity ρ) → ℕ} : I.Satisfies g u (Desc.rel ρ xs) ↔ I.R ρ fun (i : Fin (Sig.arity ρ)) => g (xs i)

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_neg {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d : Desc Sig} : I.Satisfies g u d.neg ↔ ¬I.Satisfies g u d

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_and {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d e : Desc Sig} : I.Satisfies g u (d.and e) ↔ I.Satisfies g u d ∧ I.Satisfies g u e

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_or {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d e : Desc Sig} : I.Satisfies g u (d.or e) ↔ I.Satisfies g u d ∨ I.Satisfies g u e

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_imp {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d e : Desc Sig} : I.Satisfies g u (d.imp e) ↔ I.Satisfies g u d → I.Satisfies g u e

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_iff {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d e : Desc Sig} : I.Satisfies g u (d.iff e) ↔ (I.Satisfies g u d ↔ I.Satisfies g u e)

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_ex {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d : Desc Sig} {x : ℕ} : I.Satisfies g u (Desc.ex x d) ↔ ∃ (w : U), I.IsComponentOf u w ∧ I.Satisfies (Function.update g x w) u d

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_all {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {d : Desc Sig} {x : ℕ} : I.Satisfies g u (Desc.all x d) ↔ ∀ (w : U), I.IsComponentOf u w → I.Satisfies (Function.update g x w) u d

theorem HPSG.RSRL.Interpretation.Satisfies.sortAssign_mono {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {t : Term Sig} {σ τ : Srt} (hστ : σ ≤ τ) (h : I.Satisfies g u (Desc.sortAssign t σ)) : I.Satisfies g u (Desc.sortAssign t τ)

A sort assignment is monotone in the sort.

Free variables

theorem HPSG.RSRL.Interpretation.satisfies_congr {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {u : U} {d : Desc Sig} {g g' : ℕ → U} : (∀ x ∈ d.freeVars, g x = g' x) → (I.Satisfies g u d ↔ I.Satisfies g' u d)

Satisfaction depends only on the values of the free variables.

theorem HPSG.RSRL.Interpretation.satisfies_iff_of_freeVars_eq_empty {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {u : U} {d : Desc Sig} (hd : d.freeVars = ∅) (g g' : ℕ → U) : I.Satisfies g u d ↔ I.Satisfies g' u d

The satisfaction of a closed formula does not depend on the assignment.

Grammars and models

@[reducible, inline]

abbrev HPSG.RSRL.Grammar {Srt : Type u} [PartialOrder Srt] (Sig : Signature Srt) : Type u

A grammar over a signature is a list of formulae, its principles ([Ric24], Definition 16).

Equations

• HPSG.RSRL.Grammar Sig = List (HPSG.RSRL.Desc Sig)

def HPSG.RSRL.Interpretation.Models {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) (G : Grammar Sig) : Prop

An interpretation is a model of a grammar when every entity satisfies every principle ([Ric24], Definition 18).

Equations

• I.Models G = ∀ (u : U), ∀ d ∈ G, I.Satisfies (fun (x : ℕ) => u) u d

@[instance_reducible]

instance HPSG.RSRL.Interpretation.instDecidableModelsOfDecidableEqOfDecidableLEOfFintypeAttrOfDecidablePredForallFinArityR {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) [Fintype U] [DecidableEq U] [DecidableLE Srt] [Fintype Sig.Attr] [(ρ : Sig.Rel) → DecidablePred (I.R ρ)] (G : Grammar Sig) : Decidable (I.Models G)

Equations

• I.instDecidableModelsOfDecidableEqOfDecidableLEOfFintypeAttrOfDecidablePredForallFinArityR G = id inferInstance

theorem HPSG.RSRL.Interpretation.models_iff_forall_assignment {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {G : Grammar Sig} (hG : ∀ d ∈ G, d.freeVars = ∅) : I.Models G ↔ ∀ (g : ℕ → U) (u : U), ∀ d ∈ G, I.Satisfies g u d

A model of a grammar of closed formulae satisfies them under every assignment.

@[simp]

theorem HPSG.RSRL.Interpretation.models_nil {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} : I.Models []

@[simp]

theorem HPSG.RSRL.Interpretation.models_append {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {G H : Grammar Sig} : I.Models (G ++ H) ↔ I.Models G ∧ I.Models H

theorem HPSG.RSRL.Interpretation.Models.mono {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {G H : Grammar Sig} (hI : I.Models H) (hGH : G ⊆ H) : I.Models G

A model of a grammar is a model of any part of it.

Constraints on sorts

structure HPSG.RSRL.Constraint {Srt : Type u} [PartialOrder Srt] (Sig : Signature Srt) : Type u

A constraint σ ⇒ d requires every entity whose sort is at least as specific as σ to satisfy the formula d.

• sort : Srt

  The sort that the constraint applies to.

• body : Desc Sig

  The formula that the entities of that sort satisfy.

def HPSG.RSRL.Constraint.toDesc {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (c : Constraint Sig) : Desc Sig

The formula that states a constraint.

Equations

• c.toDesc = (HPSG.RSRL.Desc.sortAssign HPSG.RSRL.Term.colon c.sort).imp c.body

@[instance_reducible]

instance HPSG.RSRL.Constraint.instCoeDesc {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : Coe (Constraint Sig) (Desc Sig)

Equations

• HPSG.RSRL.Constraint.instCoeDesc = { coe := HPSG.RSRL.Constraint.toDesc }

@[simp]

theorem HPSG.RSRL.Constraint.freeVars_toDesc {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (c : Constraint Sig) : c.toDesc.freeVars = c.body.freeVars

def HPSG.RSRL.Constraint.inherited {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} [DecidableLE Srt] (C : List (Constraint Sig)) (σ : Srt) : List (Constraint Sig)

The constraints among C that the sort σ inherits, those on σ and on its supersorts.

Equations

• HPSG.RSRL.Constraint.inherited C σ = List.filter (fun (c : HPSG.RSRL.Constraint Sig) => decide (σ ≤ c.sort)) C

@[simp]

theorem HPSG.RSRL.Interpretation.satisfies_toDesc {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} {c : Constraint Sig} : I.Satisfies g u c.toDesc ↔ I.S u ≤ c.sort → I.Satisfies g u c.body

theorem HPSG.RSRL.Interpretation.forall_satisfies_map_toDesc_iff {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {C : List (Constraint Sig)} {g : ℕ → U} {u : U} [DecidableLE Srt] : (∀ d ∈ List.map Constraint.toDesc C, I.Satisfies g u d) ↔ ∀ c ∈ Constraint.inherited C (I.S u), I.Satisfies g u c.body

An entity satisfies the formulae that state a list of constraints exactly when it satisfies the bodies of the constraints that its sort inherits. An entity below several constrained sorts therefore satisfies the constraints on all of them.

theorem HPSG.RSRL.Interpretation.models_map_toDesc_iff {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {C : List (Constraint Sig)} [DecidableLE Srt] : I.Models (List.map Constraint.toDesc C) ↔ ∀ (u : U), ∀ c ∈ Constraint.inherited C (I.S u), I.Satisfies (fun (x : ℕ) => u) u c.body

An interpretation is a model of a list of constraints exactly when every entity satisfies the constraints that its sort inherits.

theorem HPSG.RSRL.Interpretation.Models.satisfies_body {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {u : U} {G : Grammar Sig} (hI : I.Models G) {c : Constraint Sig} (hc : c.toDesc ∈ G) (hu : I.S u ≤ c.sort) : I.Satisfies (fun (x : ℕ) => u) u c.body

In a model, a constraint among the principles holds of every entity whose sort is at least as specific as the constrained sort.