RSRL interpretations

[Ric00], [Ric24]

An RSRL interpretation of a Signature (Def. 48): a universe U, a species assignment S, partial attribute functions A, and a relation interpretation R. WellTyped is the totally-well-typed, sort-resolved condition a model must meet. ex/all quantification ranges over the components of an entity (IsComponentOf).

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

An RSRL interpretation of a signature ([Ric00], Def. 48).

• U : Type u

  The universe of entities.

• S : self.U → Srt

  Species assignment — every entity has a (maximally specific) sort.

• A : Sig.Attr → self.U → Option self.U

  Attribute interpretation: each attribute a partial function on entities.

• R : Sig.Rel → Set (List self.U)

  Relation interpretation.

def HPSG.RSRL.Interpretation.termDenot {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (I : Interpretation Sig) (ass : ℕ → I.U) : Term Sig → I.U → Option I.U

Term denotation under an assignment (Def. 53): colon ↦ u, var n ↦ ass n (the anchor u is intentionally ignored for variables), feat t α ↦ follow α from t.

Equations

• I.termDenot ass HPSG.RSRL.Term.colon x✝ = some x✝
• I.termDenot ass (HPSG.RSRL.Term.var n) x✝ = some (ass n)
• I.termDenot ass (t.feat a) x✝ = (I.termDenot ass t x✝).bind (I.A a)

def HPSG.RSRL.Interpretation.attrSucc {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (I : Interpretation Sig) (x y : I.U) : Prop

y is an attribute value of x; its reflexive-transitive closure is IsComponentOf.

Equations

• I.attrSucc x y = ∃ (α : Sig.Attr), I.A α x = some y

@[implicit_reducible]

instance HPSG.RSRL.Interpretation.instDecidableRelUAttrSuccOfFintypeAttrOfDecidableEq {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (I : Interpretation Sig) [Fintype Sig.Attr] [DecidableEq I.U] : DecidableRel I.attrSucc

Equations

• I.instDecidableRelUAttrSuccOfFintypeAttrOfDecidableEq x✝¹ x✝ = id inferInstance

@[reducible, inline]

abbrev HPSG.RSRL.Interpretation.IsComponentOf {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (I : Interpretation Sig) (u v : I.U) : Prop

v is a component of u — reachable from u by following attributes. RSRL bounds quantification to these ([Ric24], Ch. 3).

Equations

• I.IsComponentOf u v = Relation.ReflTransGen I.attrSucc u v

@[implicit_reducible]

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

Equations

• I.instDecidableIsComponentOfOfDecidableEqUOfFintypeAttr u v = Relation.ReflTransGen.decidable_of_fintype u v

structure HPSG.RSRL.Interpretation.WellTyped {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (I : Interpretation Sig) : Prop

Totally-well-typed, sort-resolved (Def. 48): S species-valued, and A defined exactly where appropriate, with appropriate value sorts.

• species (u : I.U) : IsSpecies (I.S u)

  Every entity's sort is a species.

• appropDefined (α : Sig.Attr) (u : I.U) : (I.A α u).isSome = (Sig.approp (I.S u) α).isSome

  An attribute is defined exactly when appropriate to the entity's species.

• appropSort (α : Sig.Attr) (u v : I.U) : I.A α u = some v → ∀ τ ∈ Sig.approp (I.S u) α, I.S v ≤ τ

  A defined value's sort is at least as specific as the appropriate value sort.

@[implicit_reducible]

instance HPSG.RSRL.instDecidablePredR_of_isEmpty {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} [IsEmpty Sig.Rel] (I : Interpretation Sig) (ρ : Sig.Rel) : DecidablePred (I.R ρ)

For a relation-free signature, every relation symbol's membership is vacuously decidable — the hypothesis the satisfies/Models decision procedure needs. Replaces the per-signature fun ρ => nomatch ρ instance for every Rel = Empty fragment.

Equations

• HPSG.RSRL.instDecidablePredR_of_isEmpty I ρ = isEmptyElim ρ