Default inheritance

This file defines default inheritance in a taxonomy: a node takes the value of an attribute from the most specific nodes above it that specify one, so a value specified lower down overrides one specified higher up. The taxonomy is a partial order in which a ≤ m reads "a isA m", and an attribute is a partial map att : α → Option β, the values nodes specify themselves. Default inheritance organizes the lexicon of Word Grammar [Hud10] and of the defaults-based morphology of DATR [EG96] and Network Morphology [BH12], and the hierarchical lexicon of Construction Morphology.

The specifiers of a node are the nodes above it with a value of their own, and the node inherits the values of its minimal specifiers. This is the Specificity Principle: a value specified at a more specific node overrides one specified at a less specific node. The definition depends on the order alone. Two incomparable specifiers with different values, as in the Nixon diamond, leave a node with both values. Each is a credulous conclusion, and a skeptical reasoner draws neither. A value is a skeptical conclusion when it is the only value inherited, which is preferential consequence over the taxonomy (entails_iff_inherited_subset). A node inherits at most one value when the specifiers above it form a chain, as in a single-parent hierarchy, or when no node lies below two specifiers, as with the members of a choice set. The procedural account climbs the taxonomy from the node and takes the first value found. It agrees with the definition for every order of the climb that never visits a node before a node below it, such as the order of ascending degree by which inheritance networks build their extensions.

Main definitions

• DefaultInheritance.specifiers: the nodes above a node that specify the attribute.
• DefaultInheritance.inherited: the values of a node's minimal specifiers.

Main results

• DefaultInheritance.inherited_eq_singleton_of_eq_some: a node's own value is the only one it inherits.
• DefaultInheritance.inherited_eq_singleton_of_isLeast: the value of a least specifier is the only one inherited.
• DefaultInheritance.subsingleton_inherited_of_isChain, DefaultInheritance.subsingleton_inherited_of_pairwiseDisjoint: specifiers in a chain, or with pairwise disjoint lower sets, leave no conflict.
• DefaultInheritance.mem_inherited_of_find?_eq_some, DefaultInheritance.find?_bind_eq_of_inherited_eq_singleton: a bottom-up search returns an inherited value, the only one when there is no conflict.
• DefaultInheritance.entails_iff_inherited_subset: skeptical inheritance as preferential consequence.

Implementation notes

The isA links are strict and only the link from a node to its value is defeasible, so the specificity is the strong kind, and every path has a single defeasible link. The problems of longer defeasible paths, floating conclusions and zombie arguments, do not arise. Two values compete when they are values of one attribute. [Hud10] also lets links compete when one link isA the other, and relations compete when they belong to one choice set. Neither kind of competition is modelled here. The taxonomy is a partial order rather than a preorder because isA is acyclic. The node types of the consumers are finite, and partialOrderOfCovers builds their orders from immediate isA edges.

References

• [SA24]
• [Hud10]
• [EG96]
• [BH12]

def DefaultInheritance.specifiers {α : Type u_1} {β : Type u_2} [PartialOrder α] (att : α → Option β) (a : α) : Set α

The specifiers of a: the nodes above a with a value of their own.

Equations

• DefaultInheritance.specifiers att a = {m : α | a ≤ m ∧ (att m).isSome = true}

def DefaultInheritance.inherited {α : Type u_1} {β : Type u_2} [PartialOrder α] (att : α → Option β) (a : α) : Set β

The values a inherits: those of its most specific specifiers, the credulous conclusions.

Equations

• DefaultInheritance.inherited att a = {v : β | ∃ (m : α), Minimal (fun (x : α) => x ∈ DefaultInheritance.specifiers att a) m ∧ att m = some v}

theorem DefaultInheritance.mem_specifiers {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a m : α} : m ∈ specifiers att a ↔ a ≤ m ∧ (att m).isSome = true

theorem DefaultInheritance.mem_inherited {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} {v : β} : v ∈ inherited att a ↔ ∃ (m : α), Minimal (fun (x : α) => x ∈ specifiers att a) m ∧ att m = some v

@[instance_reducible]

instance DefaultInheritance.instDecidablePredMemSetSpecifiersOfDecidableLE {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} [DecidableLE α] : DecidablePred fun (x : α) => x ∈ specifiers att a

Equations

• DefaultInheritance.instDecidablePredMemSetSpecifiersOfDecidableLE x✝ = { decide := decide (a ≤ x✝) && decide ((att x✝).isSome = true), reflects_decide := ⋯ }

@[instance_reducible]

instance DefaultInheritance.instDecidablePredMemSetInheritedOfFintypeOfDecidableLEOfDecidableEq {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} [Fintype α] [DecidableLE α] [DecidableEq β] : DecidablePred fun (x : β) => x ∈ inherited att a

Equations

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

theorem DefaultInheritance.exists_le_of_mem_inherited {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} {v : β} (h : v ∈ inherited att a) : ∃ (m : α), a ≤ m ∧ att m = some v

An inherited value is the value of some node above.

theorem DefaultInheritance.inherited_eq_singleton_of_isLeast {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a m : α} {v : β} (h : IsLeast (specifiers att a) m) (hm : att m = some v) : inherited att a = {v}

The value of a least specifier is the only value inherited.

theorem DefaultInheritance.inherited_eq_singleton_of_eq_some {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} {v : β} (h : att a = some v) : inherited att a = {v}

A node's own value overrides every value above it.

theorem DefaultInheritance.subsingleton_inherited_of_isChain {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} (h : IsChain (fun (x1 x2 : α) => x1 ≤ x2) (specifiers att a)) : (inherited att a).Subsingleton

A node inherits at most one value when its specifiers form a chain, as in a single-parent hierarchy.

theorem DefaultInheritance.subsingleton_inherited_of_pairwiseDisjoint {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} (h : {m : α | (att m).isSome = true}.PairwiseDisjoint Set.Iic) : (inherited att a).Subsingleton

No node inherits two values when no node lies below two specifiers, as when the specifiers are members of one choice set.

theorem DefaultInheritance.mem_inherited_of_find?_eq_some {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a m : α} {v : β} [DecidableLE α] {l : List α} (hl : List.Pairwise (fun (x y : α) => ¬y < x) l) (hs : ∀ m ∈ specifiers att a, m ∈ l) (hm : List.find? (fun (x : α) => decide (x ∈ specifiers att a)) l = some m) (hv : att m = some v) : v ∈ inherited att a

A search that climbs from a through l and takes the value of the first specifier it meets returns an inherited value. The climb may be in any order that never visits a node before a node below it, and l must hold every specifier.

theorem DefaultInheritance.find?_bind_eq_of_inherited_eq_singleton {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} {v : β} [DecidableLE α] {l : List α} (hl : List.Pairwise (fun (x y : α) => ¬y < x) l) (hs : ∀ m ∈ specifiers att a, m ∈ l) (h : inherited att a = {v}) : (List.find? (fun (x : α) => decide (x ∈ specifiers att a)) l).bind att = some v

When a node inherits exactly one value, every bottom-up search returns it.

theorem DefaultInheritance.entails_iff_inherited_subset {α : Type u_1} {β : Type u_2} [PartialOrder α] {att : α → Option β} {a : α} {v : β} : Nonmonotonic.Entails inferInstance (specifiers att a) {m : α | att m = some v} ↔ inherited att a ⊆ {v}

A node inherits no value but v, the skeptical conclusion, exactly when its specifiers preferentially entail specifying v: its most specific specifiers all specify v.