RSRL interpretations

This file defines the interpretations of an RSRL signature. An interpretation over a universe U of entities assigns a sort to every entity, a partial function on entities to every attribute, and a set of tuples of entities to every relation symbol. A term then denotes a partial function on entities, and the components of an entity are the entities that some path reaches from it.

Main definitions

• HPSG.RSRL.Interpretation: an interpretation of a signature over a universe U.
• HPSG.RSRL.Interpretation.termDenot: the term interpretation function under a variable assignment.
• HPSG.RSRL.Interpretation.IsComponentOf: the component relation between entities.
• HPSG.RSRL.Interpretation.IsSortResolved: every entity has a species as its sort.
• HPSG.RSRL.Interpretation.IsWellTyped: every defined attribute is appropriate and has a value of the appropriate sort.
• HPSG.RSRL.Interpretation.IsTotallyWellTyped: in addition, every appropriate attribute is defined.

Main results

• HPSG.RSRL.Interpretation.isComponentOf_iff_exists_path: the components of an entity are the denotations of the paths that are defined on it.
• HPSG.RSRL.Interpretation.termDenot_congr: a term denotation depends only on the values that the assignment gives to the variables of the term.
• HPSG.RSRL.Interpretation.IsWellTyped.admits: in a well-typed interpretation the signature admits every defined path.

Implementation notes

The universe is a parameter of Interpretation rather than a field, as the carrier of a first-order structure is in mathlib, so that Fintype and DecidableEq instances on the universe are found without any per-model declaration.

Richter builds sort resolution and total well-typedness into the definition of an interpretation. Here they are separate predicates, named as in Carpenter's typed feature logic, because a worked example usually interprets only the part of a feature structure that the principle under test mentions. Such an example is well-typed without being totally well-typed. Richter also restricts the tuples of a relation to entities that are components of one common entity. That restriction is not imposed.

References

• [Ric00]
• [Ric24]
• [Car92]

structure HPSG.RSRL.Interpretation {Srt : Type u} [PartialOrder Srt] (Sig : Signature Srt) (U : Type v) : Type (max u v)

An interpretation of the signature Sig over the universe U ([Ric24], Definition 7).

• S : U → Srt

  The sort of each entity.

• A : Sig.Attr → U → Option U

  The partial function on entities that interprets each attribute.

• R (ρ : Sig.Rel) : Set (Fin (Sig.arity ρ) → U)

  The set of argument tuples that interprets each relation symbol.

Term denotation

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

The entity that a term denotes at the described entity u under the assignment g, when every attribute along the term is defined ([Ric24], Definition 10).

Equations

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

@[simp]

theorem HPSG.RSRL.Interpretation.termDenot_colon {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} : I.termDenot g Term.colon u = some u

@[simp]

theorem HPSG.RSRL.Interpretation.termDenot_var {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} (n : ℕ) : I.termDenot g (Term.var n) u = some (g n)

@[simp]

theorem HPSG.RSRL.Interpretation.termDenot_feat {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} (t : Term Sig) (α : Sig.Attr) : I.termDenot g (t.feat α) u = (I.termDenot g t u).bind (I.A α)

theorem HPSG.RSRL.Interpretation.termDenot_congr {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g g' : ℕ → U} {u : U} {t : Term Sig} (h : ∀ x ∈ t.freeVars, g x = g' x) : I.termDenot g t u = I.termDenot g' t u

A term denotation depends only on the values of the variables that occur in the term.

theorem HPSG.RSRL.Interpretation.termDenot_path {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {u : U} (g g' : ℕ → U) (p : Path Sig) : I.termDenot g (Term.path p) u = I.termDenot g' (Term.path p) u

The denotation of a path does not depend on the assignment.

Components

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

The entity v is the value of some attribute at u.

Equations

• I.attrSucc u v = ∃ (α : Sig.Attr), I.A α u = some v

@[instance_reducible]

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

Equations

• HPSG.RSRL.Interpretation.instDecidableRelAttrSuccOfFintypeAttrOfDecidableEq x✝¹ x✝ = id inferInstance

@[reducible, inline]

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

The entity v is a component of u when a sequence of attributes leads from u to v. Quantification in RSRL ranges over the components of the described entity.

Equations

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

@[instance_reducible]

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

Equations

• HPSG.RSRL.Interpretation.instDecidableIsComponentOfOfDecidableEqOfFintypeAttr u v = Relation.ReflTransGen.decidable_of_fintype u v

theorem HPSG.RSRL.Interpretation.isComponentOf_iff_exists_path {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {u v : U} (g : ℕ → U) : I.IsComponentOf u v ↔ ∃ (p : Path Sig), I.termDenot g (Term.path p) u = some v

The components of u are the entities that some path denotes at u ([Ric24], Definition 11).

Typing

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

An interpretation is sort-resolved when the sort of every entity is a species.

Equations

• I.IsSortResolved = ∀ (u : U), HPSG.RSRL.IsSpecies (I.S u)

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

An interpretation is well-typed when every attribute that is defined on an entity is appropriate to the entity's sort, with a value of the appropriate sort.

Equations

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

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

An interpretation is totally well-typed when it is well-typed and every attribute that is appropriate to the sort of an entity is defined on it.

• isWellTyped : I.IsWellTyped

  The interpretation is well-typed.

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

  Every appropriate attribute is defined.

@[instance_reducible]

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

Equations

• HPSG.RSRL.Interpretation.instDecidableIsSpeciesOfFintypeOfDecidableLE σ = { decide := decide (∀ a ∈ Finset.univ, (fun (b : Srt) => b ≤ σ → σ ≤ b) a), reflects_decide := ⋯ }

@[instance_reducible]

instance HPSG.RSRL.Interpretation.instDecidableIsSortResolvedOfDecidableLEOfFintype {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} [Fintype Srt] [DecidableLE Srt] [Fintype U] : Decidable I.IsSortResolved

Equations

• HPSG.RSRL.Interpretation.instDecidableIsSortResolvedOfDecidableLEOfFintype = { decide := decide (∀ a ∈ Finset.univ, (fun (u : U) => HPSG.RSRL.IsSpecies (I.S u)) a), reflects_decide := ⋯ }

@[instance_reducible]

instance HPSG.RSRL.Interpretation.instDecidableIsWellTypedOfDecidableLEOfFintypeAttr {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} [DecidableLE Srt] [Fintype U] [Fintype Sig.Attr] : Decidable I.IsWellTyped

Equations

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

@[instance_reducible]

instance HPSG.RSRL.Interpretation.instDecidableIsTotallyWellTypedOfDecidableLEOfFintypeAttr {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} [DecidableLE Srt] [Fintype U] [Fintype Sig.Attr] : Decidable I.IsTotallyWellTyped

Equations

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

theorem HPSG.RSRL.Interpretation.termDenot_path_cons {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} (α : Sig.Attr) (p : Path Sig) : I.termDenot g (Term.path (α :: p)) u = (I.A α u).bind (I.termDenot g (Term.path p))

The denotation of a path that starts with α is the denotation of the rest at the value of α.

theorem HPSG.RSRL.Interpretation.termDenot_path_append {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u : U} (p q : Path Sig) : I.termDenot g (Term.path (p ++ q)) u = (I.termDenot g (Term.path p) u).bind (I.termDenot g (Term.path q))

The denotation of a path p ++ q is the denotation of q at the end of p.

theorem HPSG.RSRL.Interpretation.IsWellTyped.admits {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {g : ℕ → U} {u v : U} (hI : I.IsWellTyped) {p : Path Sig} (h : I.termDenot g (Term.path p) u = some v) : Sig.Admits (I.S u) p (I.S v)

In a well-typed interpretation the signature admits every path that is defined, from the sort of the entity it starts at to the sort of the entity it reaches.

@[instance_reducible]

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

The relations of an interpretation are decidable when the signature has no relation symbols.

Equations

• HPSG.RSRL.Interpretation.instDecidablePredForallFinArityROfIsEmptyRel ρ = isEmptyElim ρ