RSRL signatures

This file defines the signatures of Relational Speciate Re-entrant Logic (RSRL), the logic in which Richter states HPSG grammars, together with the terms of its description language. A signature declares a sort hierarchy, a set of attributes with their appropriateness conditions, and a set of relation symbols with their arities. A term is a sequence of attributes that starts either at the described entity or at a variable.

The sort hierarchy is a partial order in which σ ≤ τ says that σ is at least as specific as τ. The maximally specific sorts, the species, are therefore the minimal elements.

Main definitions

• HPSG.RSRL.Signature: a signature over a sort hierarchy Srt.
• HPSG.RSRL.IsSpecies: a sort is a species when it is minimal in the hierarchy.
• HPSG.RSRL.Signature.ofDecl: the signature in which each attribute is declared once at the sorts that introduce it and inherited by their subsorts.
• HPSG.RSRL.Term: a term of the description language.
• HPSG.RSRL.Term.path: the term that follows a list of attributes from the described entity.
• HPSG.RSRL.Term.freeVars: the variables that occur in a term.
• HPSG.RSRL.Signature.Admits: the paths that the appropriateness conditions allow between two sorts.

Implementation notes

The sort hierarchy is a PartialOrder instance on the type of sorts rather than a field of the signature, so that the order lemmas of mathlib apply to sorts directly. Richter requires every relation symbol to have a positive arity and the set of relation symbols to be finite. Neither condition is imposed here. Chains, the list-like arguments that RSRL relations may take, are not formalized.

A large hierarchy is declared by its immediate-subsumption edges and a rank that every edge strictly decreases (partialOrderOfCovers). The order is then the reflexive transitive closure of the edges, so transitivity never has to be checked by enumeration.

References

• [Ric00]
• [Ric24]
• [PS94]

Signatures

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

An RSRL signature over the sort hierarchy Srt ([Ric24], Definition 1).

• Attr : Type u

  The attributes.

• Rel : Type u

  The relation symbols.

• arity : self.Rel → ℕ

  The number of arguments of each relation symbol.

• approp : Srt → self.Attr → Option Srt

  The appropriateness function. approp σ α = some τ says that α is appropriate to σ and that its values at σ have sort τ.

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

  An attribute appropriate to a sort is appropriate to each of its subsorts, with a value sort that is at least as specific.

@[reducible, inline]

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

A species is a maximally specific sort, a minimal element of the sort hierarchy.

Equations

• HPSG.RSRL.IsSpecies σ = IsMin σ

Signatures from feature declarations

def HPSG.RSRL.appropOfDecl {Srt : Type u} [PartialOrder Srt] [DecidableLE Srt] {Attr : Type u} (decl : Attr → List (Srt × Srt)) (σ : Srt) (α : Attr) : Option Srt

The appropriateness function generated by feature declarations. The list decl α pairs each sort that introduces the attribute α with the value sort of α there, and every subsort of an introducing sort inherits the declaration.

Equations

• HPSG.RSRL.appropOfDecl decl σ α = Option.map Prod.snd (List.find? (fun (d : Srt × Srt) => decide (σ ≤ d.1)) (decl α))

theorem HPSG.RSRL.exists_mem_decl_of_appropOfDecl_eq_some {Srt : Type u} [PartialOrder Srt] [DecidableLE Srt] {Attr : Type u} (decl : Attr → List (Srt × Srt)) {σ τ : Srt} {α : Attr} (h : appropOfDecl decl σ α = some τ) : ∃ d ∈ decl α, σ ≤ d.1 ∧ d.2 = τ

An attribute that declarations make appropriate to a sort is declared at a supersort of it, with the value sort that the declaration names.

theorem HPSG.RSRL.appropOfDecl_inherits {Srt : Type u} [PartialOrder Srt] [DecidableLE Srt] {Attr : Type u} (decl : Attr → List (Srt × Srt)) (hdecl : ∀ (α : Attr), List.Pairwise (fun (d d' : Srt × Srt) => ∀ σ ≤ d.1, ¬σ ≤ d'.1) (decl α)) {σ₁ σ₂ : Srt} {α : Attr} {τ₁ : Srt} (hle : σ₂ ≤ σ₁) (h : appropOfDecl decl σ₁ α = some τ₁) : ∃ (τ₂ : Srt), appropOfDecl decl σ₂ α = some τ₂ ∧ τ₂ ≤ τ₁

Declarations generate an appropriateness function with feature inheritance when no sort lies below two sorts that introduce the same attribute.

@[reducible]

def HPSG.RSRL.Signature.ofDecl {Srt : Type u} [PartialOrder Srt] [DecidableLE Srt] (Attr Rel : Type u) (arity : Rel → ℕ) (decl : Attr → List (Srt × Srt)) (hdecl : ∀ (α : Attr), List.Pairwise (fun (d d' : Srt × Srt) => ∀ σ ≤ d.1, ¬σ ≤ d'.1) (decl α)) : Signature Srt

The signature generated by feature declarations.

Equations

• HPSG.RSRL.Signature.ofDecl Attr Rel arity decl hdecl = { Attr := Attr, Rel := Rel, arity := arity, approp := HPSG.RSRL.appropOfDecl decl, approp_inherits := ⋯ }

Terms

@[reducible, inline]

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

A path is a list of attributes, read from the first attribute followed to the last.

Equations

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

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

A term of the description language ([Ric24], Definition 3).

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

  The colon denotes the described entity.

• 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

  The term t.feat α follows the attribute α from the entity that t denotes.

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

The term that follows the path p from the described entity.

Equations

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

@[simp]

theorem HPSG.RSRL.Term.path_nil {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : path [] = colon

@[simp]

theorem HPSG.RSRL.Term.path_concat {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (p : Path Sig) (α : Sig.Attr) : path (p ++ [α]) = (path p).feat α

def HPSG.RSRL.Term.freeVars {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} : Term Sig → Finset ℕ

The variables that occur in a term ([Ric24], Definition 5).

Equations

• HPSG.RSRL.Term.colon.freeVars = ∅
• (HPSG.RSRL.Term.var n).freeVars = {n}
• (t.feat a).freeVars = t.freeVars

@[simp]

theorem HPSG.RSRL.Term.freeVars_path {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} (p : Path Sig) : (path p).freeVars = ∅

Admissible paths

def HPSG.RSRL.Signature.Admits {Srt : Type u} [PartialOrder Srt] (Sig : Signature Srt) : Srt → Path Sig → Srt → Prop

The signature admits the path p from the sort σ to the sort ρ when each attribute of p is appropriate to the sort reached so far, which may be any subsort of the declared value sort.

Equations

• Sig.Admits x✝¹ [] x✝ = (x✝¹ = x✝)
• Sig.Admits x✝¹ (α :: p) x✝ = ∃ τ ∈ Sig.approp x✝¹ α, ∃ σ' ≤ τ, Sig.Admits σ' p x✝

@[instance_reducible]

instance HPSG.RSRL.Signature.decidableAdmits {Srt : Type u} [PartialOrder Srt] {Sig : Signature Srt} [Fintype Srt] [DecidableEq Srt] [DecidableLE Srt] (σ : Srt) (p : Path Sig) (ρ : Srt) : Decidable (Sig.Admits σ p ρ)

Equations

• HPSG.RSRL.Signature.decidableAdmits x✝¹ [] x✝ = HPSG.RSRL.Signature.decidableAdmits._aux_1 x✝¹ x✝
• HPSG.RSRL.Signature.decidableAdmits x✝¹ (α :: p) x✝ = ⋯.mpr inferInstance