Inheritance hierarchies

The rival horn of the motivation question ([JA20] ch. 3): a lexical entry is motivated by inheriting default properties from a more general entry, overriding where it legislates locally. A Hierarchy is a single-parent chain with acyclicity witnessed by a well-founded parent relation (the taxonomy of [JA20]'s Figure 3.5); multiple inheritance — a node with two schematic parents, as in their cross-classifying cases — is deferred to a future engine and out of scope here.

Default/override lookup (Hierarchy.value) reads a node's local specification if present, else the nearest ancestor's. It is computed by fuel-bounded structural recursion saturating at Fintype.card, so it kernel-reduces (a WellFounded.fix definition would not, blocking decide). Acyclicity is not needed for the lookup laws — card fuel saturates any finite parent map — so value_eq_of_att and value_eq_parent hold structurally; the well-founded field records the taxonomy commitment and feeds later results.

Formal defaults-with-override traditions this abstracts: DATR ([EG96]) and Network Morphology ([BH12]). [JA20] argue inheritance and the impoverished-entry model do not by themselves explicate motivation — their claim, contested in the DATR literature. The one-level default-override primitive already lives in Syntax/ConstructionGrammar/Inheritance.lean (inheritField, child-wins); the transitive chain walk here is new, and the shared Option-level override primitive is a candidate for a future Core/Order/ lift.

Main declarations

• Hierarchy — a single-parent chain with a well-founded parent relation
• valueFuel, Hierarchy.value — fuel-bounded default/override lookup
• Hierarchy.value_eq_of_att, Hierarchy.value_eq_parent — override wins; path extension to the parent
• Hierarchy.parent_asymm — no 2-cycle: nodes cannot be each other's parent

structure Morphology.Construction.Hierarchy (ι : Type u_3) : Type u_3

A single-parent inheritance chain: parent links each node to its immediate supertype (none at a root), with wf witnessing 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 Morphology.Construction.valueFuel {ι : Type u_1} {β : Type u_2} (parent : ι → Option ι) (att : ι → Option β) : ℕ → ι → Option β

Default/override lookup with a step budget: at fuel 0 only the local specification is read; each further unit walks one step to the parent.

Equations

• Morphology.Construction.valueFuel parent att 0 x✝ = att x✝
• Morphology.Construction.valueFuel parent att k.succ x✝ = match att x✝ with | some v => some v | none => (parent x✝).bind (Morphology.Construction.valueFuel parent att k)

Fuel monotonicity and saturation

theorem Morphology.Construction.valueFuel_of_att {ι : Type u_1} {β : Type u_2} {parent : ι → Option ι} {att : ι → Option β} {n : ι} {v : β} (h : att n = some v) (k : ℕ) : valueFuel parent att k n = some v

A local specification is read at any fuel.

theorem Morphology.Construction.valueFuel_some_succ {ι : Type u_1} {β : Type u_2} {parent : ι → Option ι} {att : ι → Option β} (k : ℕ) (n : ι) (v : β) (h : valueFuel parent att k n = some v) : valueFuel parent att (k + 1) n = some v

A value found within k steps is still found within k + 1.

theorem Morphology.Construction.valueFuel_succ_congr {ι : Type u_1} {β : Type u_2} {parent : ι → Option ι} {att : ι → Option β} {j k : ℕ} (h : valueFuel parent att j = valueFuel parent att k) : valueFuel parent att (j + 1) = valueFuel parent att (k + 1)

Two fuel levels giving the same lookup give the same lookup after one more step: the recursion consumes only the previous level.

theorem Morphology.Construction.valueFuel_const_of_fixed {ι : Type u_1} {β : Type u_2} {parent : ι → Option ι} {att : ι → Option β} {k : ℕ} (hfix : valueFuel parent att k = valueFuel parent att (k + 1)) (m : ℕ) : k ≤ m → valueFuel parent att m = valueFuel parent att k

Once a fuel level is a fixed point, every larger level agrees with it.

theorem Morphology.Construction.valueFuel_card_fixed {ι : Type u_1} {β : Type u_2} {parent : ι → Option ι} {att : ι → Option β} [Fintype ι] : valueFuel parent att (Fintype.card ι) = valueFuel parent att (Fintype.card ι + 1)

Card fuel saturates: with Fintype.card fuel the lookup is a fixed point of the one-step recursion. A monotone chain of defined-sets bounded by the universe can strictly grow at most card times.

def Morphology.Construction.Hierarchy.value {ι : Type u_1} {β : Type u_2} [Fintype ι] (h : Hierarchy ι) (att : ι → Option β) (n : ι) : Option β

Default/override lookup: a node's local specification if present, else the nearest ancestor's, computed by saturating the fuel recursion at Fintype.card.

Equations

• h.value att n = Morphology.Construction.valueFuel h.parent att (Fintype.card ι) n

theorem Morphology.Construction.Hierarchy.value_eq_of_att {ι : Type u_1} {β : Type u_2} [Fintype ι] (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 Morphology.Construction.Hierarchy.value_eq_parent {ι : Type u_1} {β : Type u_2} [Fintype ι] (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 Morphology.Construction.Hierarchy.parent_asymm {ι : Type u_1} (h : Hierarchy ι) {a b : ι} (hab : h.parent a = some b) (hba : h.parent b = some a) : False

No 2-cycle: in a well-founded hierarchy no two nodes are each other's parent. This is the obstruction a single directed inheritance relation hits on [JA20]'s Objection 10 — a pair whose form and meaning planes demand opposite parent orientations cannot both be edges of one acyclic hierarchy.

Figure 3.5: default and override

The taxonomy Animal → Bird/Fish, Bird → Canary/Ostrich: birds fly by default, the ostrich overrides to not-fly, the canary inherits flight. A concept hierarchy, not linguistic data — an abstract witness that override and default inheritance compute as intended.

@[implicit_reducible]

instance Morphology.Construction.instDecidableEqAnimal : DecidableEq Morphology.Construction.Animal✝

Equations

• Morphology.Construction.instDecidableEqAnimal x✝ y✝ = if h : Morphology.Construction.Animal.ctorIdx✝ x✝ = Morphology.Construction.Animal.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.Construction.instFintypeAnimal : Fintype Morphology.Construction.Animal✝

Equations

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