Default Inheritance — Local Properties + BFS Lookup + Best Fit Principle

@cite{hudson-2010} §2.5, §3.5, §4.6.4

A node's value for a relation r is determined by:

1. Its local value if one is specified (localProps net node r).
2. Otherwise, the value of its nearest ancestor in the isA chain that has a local value for r — the Best Fit Principle: "When a default conflicts with a more specific fact, the specific fact wins" @cite{hudson-2010} §4.6.4. Hudson attributes the principle to Winograd's earlier work on frame-based defaults but generalises it from frames to a property of the cognitive network as a whole.

Like ancestors, the BFS recursion is bounded by nodeUniverse.length rather than a magic constant — finite networks always reach a fixpoint.

The override case (where a child specifies a local value that differs from its parent's) is the empirical heart of WG: passive inherits transitive's arg-structure but overrides slot 1; the inverted auxiliary inherits the verb's subject slot but overrides its direction.

def Core.Inheritance.localProps {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (r : R) : List α

Local property values: targets of .prop links from node with label r. A node may have multiple values for the same relation (e.g., a bird has two wings).

Equations

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

def Core.Inheritance.inheritedBound {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (r : R) : ℕ → List α

Bounded BFS for inherited property values. The bound parameter is intended to be ≥ (nodeUniverse net).length. Structurally recursive on Nat.

Equations

• One or more equations did not get rendered due to their size.
• Core.Inheritance.inheritedBound net node r 0 = Core.Inheritance.localProps net node r

def Core.Inheritance.inherited {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (r : R) : List α

Inherited property values for relation r, resolved by the Best Fit Principle: the most specific (nearest ancestor in the isA chain) wins. Recursion bound derived from network size.

Equations

• Core.Inheritance.inherited net node r = Core.Inheritance.inheritedBound net node r net.nodeUniverse.length

theorem Core.Inheritance.bestFit_local {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (r : R) (h : localProps net node r ≠ []) : inherited net node r = localProps net node r

If a node has local properties for r, inherited returns them directly (local overrides inherited).

theorem Core.Inheritance.localProps_via_prop_link {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (r : R) (a : α) (h : a ∈ localProps net node r) : ∃ l ∈ net.links, l.kind = LinkKind.prop ∧ l.source = node ∧ l.label = some r ∧ l.target = a

Every value returned by localProps is the target of a prop link from node labelled r. The "kind discipline" — localProps only ever returns the targets of property links, never of isA or or links.

theorem Core.Inheritance.localProps_monotone_in_links {α R : Type} [DecidableEq α] [DecidableEq R] (net₁ net₂ : Network α R) (node : α) (r : R) (hsub : net₁.links ⊆ net₂.links) (a : α) (hmem : a ∈ localProps net₁ node r) : a ∈ localProps net₂ node r

The inherited BFS is monotone in the link list: adding new property links for r to node can only add to (never remove from) localProps. This is a sanity check on the network update semantics.