Inheritance hierarchies

This file defines default inheritance with override: a lexical entry inherits a property from a more general entry unless it specifies the property itself. It is the organizing principle of the hierarchical lexicon of Construction Morphology and the rival to relational motivation in Relational Morphology. A Hierarchy is a single-parent forest whose parent relation is well-founded, and Hierarchy.value looks up a node's own specification if it has one and its nearest ancestor's otherwise, by recursion along the parent relation; the recursion step is the priority union of partial values, Option.or.

A finite family of schemas with distinct descriptions carries its own hierarchy (Hierarchy.ofFamily): a schema's parent is the nearest more general schema of the family, the one whose description is greatest among those strictly below its own. What is inherited monotonically, everything a more general description pins, needs no lookup, since an instance of a schema instantiates every more general schema; the lookup is for defeasible properties that a subschema may override.

Multiple inheritance, a node with two parents, is not modelled here; the multi-parent form of the override step is Syntax/ConstructionGrammar/Inheritance.lean. The formal traditions of defaults with override are DATR and Network Morphology.

Main declarations

• Hierarchy, Hierarchy.ofDepth: a single-parent forest with a well-founded parent relation.
• Hierarchy.value, Hierarchy.value_eq: default-and-override lookup and its recursion.
• Hierarchy.parent_asymm: no two nodes are each other's parent.
• Hierarchy.NearestGeneral, Hierarchy.ofFamily, Hierarchy.ofFamily_parent_eq_some_iff: the hierarchy derived from a finite family of schemas.

References

• [jackendoff-audring-2020]
• [booij-2010-compass]
• [evans-gazdar-1996]
• [brown-hippisley-2012]

structure ConstructionMorphology.Hierarchy (ι : Type u_3) : Type u_3

A single-parent inheritance hierarchy: parent links each node to its immediate supertype, none at a root, and wf witnesses acyclicity.

• parent : ι → Option ι

  The immediate-supertype map.

• wf : WellFounded fun (a b : ι) => self.parent b = some a

  Acyclicity: the parent relation is well-founded.

def ConstructionMorphology.Hierarchy.ofDepth {ι : Type u_1} (parent : ι → Option ι) (depth : ι → ℕ) (h : ∀ (a b : ι), parent b = some a → depth a < depth b) : Hierarchy ι

A hierarchy from a parent map and a depth function decreasing toward the root; on a finite node type the obligation closes by decide.

Equations

• ConstructionMorphology.Hierarchy.ofDepth parent depth h = { parent := parent, wf := ⋯ }

def ConstructionMorphology.Hierarchy.value {ι : Type u_1} {β : Type u_2} (h : Hierarchy ι) (att : ι → Option β) : ι → Option β

Default-and-override lookup: a node's own specification if present, else the nearest ancestor's, by recursion along the parent relation.

Equations

• h.value att = ⋯.fix fun (n : ι) (ih : (y : ι) → h.parent n = some y → Option β) => (att n).or ((h.parent n).pbind fun (m : ι) (hm : h.parent n = some m) => ih m ⋯)

theorem ConstructionMorphology.Hierarchy.value_eq {ι : Type u_1} {β : Type u_2} (h : Hierarchy ι) {att : ι → Option β} (n : ι) : h.value att n = (att n).or ((h.parent n).bind (h.value att))

The recursion step is the priority union: the local specification wins, else defer to the parent.

theorem ConstructionMorphology.Hierarchy.value_eq_of_att {ι : Type u_1} {β : Type u_2} (h : Hierarchy ι) {att : ι → Option β} {n : ι} {v : β} (hn : att n = some v) : h.value att n = some v

Override wins: a local specification is the value.

theorem ConstructionMorphology.Hierarchy.value_eq_parent {ι : Type u_1} {β : Type u_2} (h : Hierarchy ι) {att : ι → Option β} {n : ι} (hn : att n = none) : h.value att n = (h.parent n).bind (h.value att)

Path extension: at a node with no local specification, the value is the parent's.

theorem ConstructionMorphology.Hierarchy.parent_asymm {ι : Type u_1} (h : Hierarchy ι) {a b : ι} (hab : h.parent a = some b) (hba : h.parent b = some a) : False

No two nodes are each other's parent.

The hierarchy of a family of schemas

def ConstructionMorphology.Hierarchy.NearestGeneral {ι : Type u_1} {V : Type u_3} {α : Type u_4} [PartialOrder α] (family : ι → Schema V α) (i j : ι) : Prop

j is the nearest more general schema than i in the family when its description is strictly below i's and above every other description of the family strictly below i's.

Equations

• ConstructionMorphology.Hierarchy.NearestGeneral family i j = ((family j).body < (family i).body ∧ ∀ (k : ι), (family k).body < (family i).body → (family k).body ≤ (family j).body)

theorem ConstructionMorphology.Hierarchy.NearestGeneral.unique {ι : Type u_1} {V : Type u_3} {α : Type u_4} [PartialOrder α] {family : ι → Schema V α} {i j : ι} (hinj : Function.Injective fun (i : ι) => (family i).body) {j' : ι} (hj : NearestGeneral family i j) (hj' : NearestGeneral family i j') : j = j'

With distinct descriptions, the nearest more general schema is unique.

@[instance_reducible]

instance ConstructionMorphology.Hierarchy.instDecidableNearestGeneral {ι : Type u_1} {V : Type u_3} {α : Type u_4} [PartialOrder α] [Fintype ι] [DecidableLE (V → α)] [DecidableLT (V → α)] (family : ι → Schema V α) (i j : ι) : Decidable (NearestGeneral family i j)

Equations

• ConstructionMorphology.Hierarchy.instDecidableNearestGeneral family i j = id inferInstance

def ConstructionMorphology.Hierarchy.ofFamily {ι : Type u_1} {V : Type u_3} {α : Type u_4} [PartialOrder α] [Fintype ι] [DecidableLE (V → α)] [DecidableLT (V → α)] (family : ι → Schema V α) (hinj : Function.Injective fun (i : ι) => (family i).body) : Hierarchy ι

The subsumption hierarchy of a finite family of schemas with distinct descriptions: a schema's parent is the nearest more general schema of the family, when there is one.

Equations

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

theorem ConstructionMorphology.Hierarchy.ofFamily_parent_eq_some_iff {ι : Type u_1} {V : Type u_3} {α : Type u_4} [PartialOrder α] {family : ι → Schema V α} {i j : ι} [Fintype ι] [DecidableLE (V → α)] [DecidableLT (V → α)] (hinj : Function.Injective fun (i : ι) => (family i).body) : (ofFamily family hinj).parent i = some j ↔ NearestGeneral family i j

theorem ConstructionMorphology.Hierarchy.ofFamily_parent_eq_none_iff {ι : Type u_1} {V : Type u_3} {α : Type u_4} [PartialOrder α] {family : ι → Schema V α} {i : ι} [Fintype ι] [DecidableLE (V → α)] [DecidableLT (V → α)] (hinj : Function.Injective fun (i : ι) => (family i).body) : (ofFamily family hinj).parent i = none ↔ ¬∃ (j : ι), NearestGeneral family i j