RSRL descriptions

[Ric00], [Ric24]

The description language of RSRL — the formulae stating an HPSG grammar's principles (Def. 54; satisfaction Def. 58). Includes relational formulae and component quantification (∃/∀ over the components of the described entity), the features making RSRL richer than FOL. Chains (list-valued relation arguments, Def. 49–50) are deferred.

ex/all are bounded by IsComponentOf (reachability by attributes), decidable on finite models, so ∃-worked examples reduce by decide. Models evaluates the (variable-free) principles under the assignment fun _ => u.

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

RSRL descriptions over Terms ([Ric00], Def. 54): atomic sort-assignments and path-equations, relational formulae, the classical connectives, and component quantification.

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

  Sort assignment τ ~ σ: the entity at t has a sort at least as specific as σ.

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

  Path equation τ₁ ≈ τ₂: the entities at t₁ and t₂ are token-identical.

• rel {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (ρ : Sig.Rel) (ts : List (Term Sig)) : Desc Sig

  Relational formula ρ(t₁,…,tₙ): the tuple of denoted terms stands in 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

  Implication (classical; vacuously satisfied where the antecedent fails).

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

  Existential component quantification: some component of the described entity.

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

  Universal component quantification: every component of the described entity.

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

Satisfaction under a variable assignment ([Ric00], Def. 58). ex/all quantify over the components of u (IsComponentOf), RSRL's bounded quantification. An undefined term makes an atomic description false.

Equations

• I.satisfies ass u (HPSG.RSRL.Desc.sortAssign t σ) = match I.termDenot ass t u with | some v => I.S v ≤ σ | none => False
• I.satisfies ass u (HPSG.RSRL.Desc.pathEq t₁ t₂) = match I.termDenot ass t₁ u, I.termDenot ass t₂ u with | some a, some b => a = b | x, x_1 => False
• I.satisfies ass u (HPSG.RSRL.Desc.rel ρ ts) = match List.mapM (fun (t : HPSG.RSRL.Term Sig) => I.termDenot ass t u) ts with | some args => I.R ρ args | none => False
• I.satisfies ass u d.neg = ¬I.satisfies ass u d
• I.satisfies ass u (d.and e) = (I.satisfies ass u d ∧ I.satisfies ass u e)
• I.satisfies ass u (d.or e) = (I.satisfies ass u d ∨ I.satisfies ass u e)
• I.satisfies ass u (d.imp e) = (I.satisfies ass u d → I.satisfies ass u e)
• I.satisfies ass u (HPSG.RSRL.Desc.ex v d) = ∃ (w : I.U), I.IsComponentOf u w ∧ I.satisfies (Function.update ass v w) u d
• I.satisfies ass u (HPSG.RSRL.Desc.all v d) = ∀ (w : I.U), I.IsComponentOf u w → I.satisfies (Function.update ass v w) u d

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.
• I.decSatisfies ass u d.neg = ⋯.mpr inferInstance
• I.decSatisfies ass u (d.and e) = ⋯.mpr inferInstance
• I.decSatisfies ass u (d.or e) = ⋯.mpr inferInstance
• I.decSatisfies ass u (d.imp e) = ⋯.mpr inferInstance
• I.decSatisfies ass u (HPSG.RSRL.Desc.ex v d) = ⋯.mpr inferInstance
• I.decSatisfies ass u (HPSG.RSRL.Desc.all v d) = ⋯.mpr inferInstance

@[reducible, inline]

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

A grammar is a signature together with a set (here List) of descriptions, its principles ([Ric00]).

Equations

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

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

An interpretation is a model of a grammar iff every principle holds of every entity in all its components ([Ric00]). Principles are variable-free, so they are evaluated under any assignment (here fun _ => u).

Equations

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

@[implicit_reducible]

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

Equations

• I.instDecidableModelsOfDecidableEqOfDecidableLEOfFintypeAttrOfDecidablePredListUR G = id inferInstance

@[implicit_reducible]

instance HPSG.RSRL.instDecidableIsSpecies {Srt : Type u} [PartialOrder Srt] [Fintype Srt] [DecidableLE Srt] (σ : Srt) : Decidable (IsSpecies σ)

IsSpecies (i.e. IsMin) is decidable on a finite sort hierarchy.

Equations

• HPSG.RSRL.instDecidableIsSpecies σ = HPSG.RSRL.instDecidableIsSpecies._aux_1 σ

@[implicit_reducible]

instance HPSG.RSRL.instDecidableWellTyped {Srt : Type u} [PartialOrder Srt] [Fintype Srt] [DecidableLE Srt] {Sig : Signature Srt} (I : Interpretation Sig) [Fintype I.U] [DecidableEq I.U] [Fintype Sig.Attr] : Decidable I.WellTyped

WellTyped is decidable on a finite interpretation.

Equations

• One or more equations did not get rendered due to their size.