Documentation

Linglib.Syntax.HPSG.Subinterpretation

Generated sub-interpretations #

This file defines the sub-interpretation that an entity generates and proves that satisfaction is local to it. The sub-interpretation generated by r has the components of r as its universe and inherits the sorts, attribute values and relations of the whole interpretation. Because quantification in RSRL ranges over components, an entity of the sub-interpretation satisfies a formula there exactly when it satisfies it in the whole interpretation.

An interpretation is rooted at r when every entity is a component of r. A generated sub-interpretation is rooted at its generator, so every entity of a model of a grammar is the root of a rooted model of the same grammar.

Main definitions #

Main results #

References #

source
def HPSG.RSRL.Interpretation.generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) (r : U) :
Interpretation Sig { v : U // I.IsComponentOf r v }

The sub-interpretation generated by r, whose universe is the set of components of r.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HPSG.RSRL.Interpretation.IsRootedAt {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) (r : U) :
    Prop

    An interpretation is rooted at r when every entity is a component of r.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance HPSG.RSRL.Interpretation.instDecidableIsRootedAtOfDecidableEqOfFintypeAttr {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} (I : Interpretation Sig U) (r : U) [Fintype U] [DecidableEq U] [Fintype Sig.Attr] :
      Decidable (I.IsRootedAt r)
      Equations
      source
      @[simp]
      theorem HPSG.RSRL.Interpretation.generated_S {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} {v : { v : U // I.IsComponentOf r v }} :
      (I.generated r).S v = I.S ↑v
      source
      @[simp]
      theorem HPSG.RSRL.Interpretation.map_val_generated_A {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} {v : { v : U // I.IsComponentOf r v }} (α : Sig.Attr) :
      Option.map Subtype.val ((I.generated r).A α v) = I.A α ↑v
      source
      theorem HPSG.RSRL.Interpretation.generated_A_eq_some {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} {v w : { v : U // I.IsComponentOf r v }} {α : Sig.Attr} :
      (I.generated r).A α v = some w ↔ I.A α ↑v = some ↑w
      source
      @[simp]
      theorem HPSG.RSRL.Interpretation.map_val_termDenot_generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} {v : { v : U // I.IsComponentOf r v }} (g : ℕ → { v : U // I.IsComponentOf r v }) (t : Term Sig) :
      Option.map Subtype.val ((I.generated r).termDenot g t v) = I.termDenot (fun (n : ℕ) => ↑(g n)) t ↑v
      source
      theorem HPSG.RSRL.Interpretation.isComponentOf_generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} {v w : { v : U // I.IsComponentOf r v }} :
      (I.generated r).IsComponentOf v w ↔ I.IsComponentOf ↑v ↑w
      source
      theorem HPSG.RSRL.Interpretation.isRootedAt_generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} :
      (I.generated r).IsRootedAt ⟨r, ⋯⟩

      A generated sub-interpretation is rooted at its generator.

      source
      theorem HPSG.RSRL.Interpretation.satisfies_generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {r : U} {v : { v : U // I.IsComponentOf r v }} {d : Desc Sig} {g : ℕ → { v : U // I.IsComponentOf r v }} :
      (I.generated r).Satisfies g v d ↔ I.Satisfies (fun (n : ℕ) => ↑(g n)) (↑v) d

      Satisfaction is local. An entity of a generated sub-interpretation satisfies a formula there exactly when it satisfies it in the whole interpretation.

      source
      theorem HPSG.RSRL.Interpretation.Models.generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} {G : Grammar Sig} (hI : I.Models G) (r : U) :
      (I.generated r).Models G

      A generated sub-interpretation of a model of a grammar is a model of it.

      source
      theorem HPSG.RSRL.Interpretation.IsWellTyped.generated {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} {U : Type v} {I : Interpretation Sig U} (hI : I.IsWellTyped) (r : U) :
      (I.generated r).IsWellTyped

      A generated sub-interpretation of a well-typed interpretation is well-typed.