RSRL signatures

[Ric00], [Ric24], [PS94]

An RSRL signature (Def. 47): a sort hierarchy [PartialOrder Srt] (a ≤ b = "a at least as specific as b") with appropriateness declarations and relation symbols. The model-theoretic foundation of HPSG (Pollard & Sag 1994 onward); Interpretation.lean gives the models, Description.lean the description language.

Structural subsumption order from a covers relation

The sort hierarchy's ≤ is the reflexive-transitive closure of a direct-subsumption (covers) relation, so transitivity is structural (ReflTransGen.trans) and never a proof obligation — and, since the order is not decided by a Bool predicate, there is no |α|³ transitivity decide to exceed the elaborator recursion depth on a large hierarchy. Antisymmetry follows from a rank function every edge strictly decreases; the author declares the ~|α|-edge DAG and a depth function, not the closure.

@[reducible]

def HPSG.RSRL.partialOrderOfCovers {α : Type u} (covers : α → α → Prop) (rank : α → ℕ) (hrank : ∀ (a b : α), covers a b → rank b < rank a) : PartialOrder α

Build a PartialOrder from a direct-subsumption ("covers") relation and a rank that every edge strictly decreases. ≤ is ReflTransGen covers; transitivity is structural and antisymmetry follows from rank — no decide over the order, so it scales to large hierarchies.

Equations

• HPSG.RSRL.partialOrderOfCovers covers rank hrank = { le := fun (a b : α) => Relation.ReflTransGen covers a b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible]

def HPSG.RSRL.decidableLEOfCovers {α : Type u} [DecidableEq α] {covers : α → α → Prop} [DecidableRel covers] (allSorts : List α) (complete : ∀ (a b : α), covers a b → b ∈ allSorts) (a b : α) : Decidable (Relation.ReflTransGen covers a b)

Decidable (a ≤ b) for partialOrderOfCovers, via finite reachability over an explicit list of all sorts (Core.Relation.ReflTransGen.decidable_of_finite — mathlib has no Decidable (ReflTransGen …); the List-based variant kernel-reduces under decide where the Finset/Quotient one does not). allSorts need only contain every covers-target; pass the sort enumeration.

Equations

• HPSG.RSRL.decidableLEOfCovers allSorts complete a b = Relation.ReflTransGen.decidable_of_finite allSorts complete a b

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

An RSRL signature ([Ric00], Def. 47) over a sort hierarchy Srt.

• Attr : Type u

  Attributes (feature names).

• Rel : Type u

  Relation symbols (unused until a principle needs relations).

• arity : self.Rel → ℕ

  Relation arities.

• approp : Srt → self.Attr → Option Srt

  Appropriateness: approp σ α = some τ means α is appropriate to σ with value sort τ.

• approp_inherits {σ₁ σ₂ : Srt} {α : self.Attr} {τ₁ : Srt} : σ₂ ≤ σ₁ → self.approp σ₁ α = some τ₁ → ∃ (τ₂ : Srt), self.approp σ₂ α = some τ₂ ∧ τ₂ ≤ τ₁

  Feature inheritance: a more specific sort inherits appropriateness with an at-least-as- specific value.

@[reducible, inline]

abbrev HPSG.RSRL.IsSpecies {Srt : Type u} [PartialOrder Srt] (σ : Srt) : Prop

A species is a maximally specific sort — minimal in the specificity order.

Equations

• HPSG.RSRL.IsSpecies σ = IsMin σ

def HPSG.RSRL.Signature.IsAtomicSort {Srt : Type u} [PartialOrder Srt] (Sig : Signature Srt) (σ : Srt) : Prop

An atomic sort: a species with no appropriate attributes. (Distinct from IsAtom.)

Equations

• Sig.IsAtomicSort σ = (IsMin σ ∧ ∀ (α : Sig.Attr), Sig.approp σ α = none)

@[reducible, inline]

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

A :-rooted attribute path (Def. 52, variable-free fragment): [] is the described entity, α :: p follows α then the rest.

Equations

• HPSG.RSRL.Path Sig = List Sig.Attr

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

An RSRL term (Def. 52): rooted at the described entity (colon) or a variable (var n), extended by attributes (feat t α). Variables support relations and quantification.

• colon {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : Term Sig

  The described entity (RSRL :).

• var {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : ℕ → Term Sig

  A variable.

• feat {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : Term Sig → Sig.Attr → Term Sig

  Follow attribute α from t (RSRL tα).

def HPSG.RSRL.Term.path {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (p : Path Sig) : Term Sig

The :-rooted term following a path: Term.path [α, β] = (colon.feat α).feat β.

Equations

• HPSG.RSRL.Term.path p = List.foldl HPSG.RSRL.Term.feat HPSG.RSRL.Term.colon p

theorem HPSG.RSRL.approp_inh_of_propagates {Srt : Type u} [PartialOrder Srt] {Attr : Type u} {approp : Srt → Attr → Option Srt} (h : ∀ (σ₁ σ₂ : Srt) (α : Attr), σ₂ ≤ σ₁ → (approp σ₁ α).isSome = true → approp σ₂ α = approp σ₁ α) {σ₁ σ₂ : Srt} {α : Attr} {τ₁ : Srt} (hle : σ₂ ≤ σ₁) (happ : approp σ₁ α = some τ₁) : ∃ (τ₂ : Srt), approp σ₂ α = some τ₂ ∧ τ₂ ≤ τ₁

Derive the Signature.approp_inherits obligation from an isSome-gated propagation lemma. When appropriateness values do not refine down the order (a sort and its subsorts carry the same value for an attribute — the common case), the inherited value is τ₁ itself, so the propagation σ₂ ≤ σ₁ → (approp σ₁ α).isSome → approp σ₂ α = approp σ₁ α suffices. A large signature proves that propagation by decide (no ∃-search, no τ₁ quantifier — far cheaper) and feeds it here.