Inheritance Networks

Hudson's Word Grammar organizes all linguistic knowledge as networks of nodes connected by labeled directed links. @cite{hudson-2010}

Properties in WG are not key-value pairs attached to nodes — they ARE links between nodes. "Bird has wing" is a link labeled front-limb from bird to wing. IsA links form a taxonomy; properties flow down the taxonomy by default inheritance. The Best Fit Principle (§3.5) resolves conflicts: the most specific value (nearest ancestor in the isA chain) wins.

Hudson's five primitive relations (§3.2.5)

• isA — taxonomic classification (bird isA animal)
• or — mutual exclusivity / choice sets (male or female)
• prop — named property/relation links (bird --front-limb--> wing)

(Hudson also lists argument and value as primitives for defining relational concepts; these are modeled here as prop links with appropriate labels.)

Key definitions

• LinkKind — isA, or, prop (the three distinguished link types)
• Link — a labeled directed edge in the network
• Network — a set of labeled directed links between nodes
• parents, ancestors, isA — taxonomy traversal
• choiceSet — OR alternatives (mutually exclusive values)
• localProps, inherited — property lookup with Best Fit default inheritance
• Prototype — graded category membership (typicality rankings)

inductive Core.Inheritance.LinkKind : Type

Distinguished link types in a WG network. @cite{hudson-2010} §3.2. IsA and or are separated from general property links because the inheritance algorithm must traverse isA links and choice-set resolution uses or links.

• isA : LinkKind
• or : LinkKind
• prop : LinkKind

def Core.Inheritance.instReprLinkKind.repr : LinkKind → Nat → Std.Format

Equations

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

instance Core.Inheritance.instReprLinkKind : Repr LinkKind

Equations

• Core.Inheritance.instReprLinkKind = { reprPrec := Core.Inheritance.instReprLinkKind.repr }

instance Core.Inheritance.instDecidableEqLinkKind : DecidableEq LinkKind

Equations

• Core.Inheritance.instDecidableEqLinkKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Inheritance.instBEqLinkKind.beq : LinkKind → LinkKind → Bool

Equations

• Core.Inheritance.instBEqLinkKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Inheritance.instBEqLinkKind : BEq LinkKind

Equations

• Core.Inheritance.instBEqLinkKind = { beq := Core.Inheritance.instBEqLinkKind.beq }

structure Core.Inheritance.Link (α R : Type) : Type

A labeled directed edge: source --[kind, label]--> target. In WG, all knowledge is encoded as links between nodes: "cat isA mammal", "bird --front-limb--> wing", "male or female".

• kind : LinkKind
• source : α
• target : α
• label : Option R

instance Core.Inheritance.instReprLink {α✝ R✝ : Type} [Repr α✝] [Repr R✝] : Repr (Link α✝ R✝)

Equations

• Core.Inheritance.instReprLink = { reprPrec := Core.Inheritance.instReprLink.repr }

def Core.Inheritance.instReprLink.repr {α✝ R✝ : Type} [Repr α✝] [Repr R✝] : Link α✝ R✝ → Nat → Std.Format

Equations

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

def Core.Inheritance.instDecidableEqLink.decEq {α✝ R✝ : Type} [DecidableEq α✝] [DecidableEq R✝] (x✝ x✝¹ : Link α✝ R✝) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.Inheritance.instDecidableEqLink {α✝ R✝ : Type} [DecidableEq α✝] [DecidableEq R✝] : DecidableEq (Link α✝ R✝)

Equations

• Core.Inheritance.instDecidableEqLink = Core.Inheritance.instDecidableEqLink.decEq

def Core.Inheritance.instBEqLink.beq {α✝ R✝ : Type} [BEq α✝] [BEq R✝] : Link α✝ R✝ → Link α✝ R✝ → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.Inheritance.instBEqLink.beq x✝¹ x✝ = false

instance Core.Inheritance.instBEqLink {α✝ R✝ : Type} [BEq α✝] [BEq R✝] : BEq (Link α✝ R✝)

Equations

• Core.Inheritance.instBEqLink = { beq := Core.Inheritance.instBEqLink.beq }

structure Core.Inheritance.Network (α R : Type) [DecidableEq α] [DecidableEq R] : Type

A WG inheritance network: nodes connected by labeled directed links. Parameterized over node type α and relation-label type R.

• links : List (Link α R)

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

Direct isA parents of a node.

Equations

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

def Core.Inheritance.ancestors {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (fuel : Nat := 100) : List α

Ancestors: transitive closure of parents, with fuel for termination.

Equations

• One or more equations did not get rendered due to their size.
• Core.Inheritance.ancestors net node 0 = []

def Core.Inheritance.isA {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (a b : α) (fuel : Nat := 100) : Bool

Reflexive-transitive isA: does a inherit from b?

Equations

• Core.Inheritance.isA net a b fuel = (a == b || List.elem b (Core.Inheritance.ancestors net a fuel))

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

OR-alternatives of a node (§3.3): mutually exclusive choices. E.g., choiceSet net gender returns [male, female] if the network contains male --or--> gender and female --or--> gender.

Equations

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

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.inherited {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) (r : R) (fuel : Nat := 100) : List α

Inherited property values for relation r, resolved by the Best Fit Principle (§3.5): the most specific (nearest ancestor in the isA chain) wins. Breadth-first walk up the taxonomy; returns the first non-empty result found.

Equations

• One or more equations did not get rendered due to their size.
• Core.Inheritance.inherited net node r 0 = match Core.Inheritance.localProps net node r with | [] => [] | vs => vs

theorem Core.Inheritance.isA_refl {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (a : α) : isA net a a = true

Every node isA itself.

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 (the Best Fit Principle: local overrides inherited).

structure Core.Inheritance.Prototype (α : Type) : Type

A prototype: a category with graded typicality over instances. Higher values = more prototypical. @cite{hudson-2010} Ch 2: categories have graded membership; the prototype is the best exemplar.

• category : α
• typicality : α → Nat

def Core.Inheritance.Prototype.atLeastAsTypical {α : Type} (proto : Prototype α) (a b : α) : Bool

Whether a is at least as typical as b in a prototype.

Equations

• proto.atLeastAsTypical a b = decide (proto.typicality a ≥ proto.typicality b)

def Core.Inheritance.Prototype.moreTypical {α : Type} (proto : Prototype α) (a b : α) : Bool

Whether a is strictly more typical than b in a prototype.

Equations

• proto.moreTypical a b = decide (proto.typicality a > proto.typicality b)

theorem Core.Inheritance.Prototype.atLeastAsTypical_refl {α : Type} (proto : Prototype α) (a : α) : proto.atLeastAsTypical a a = true

atLeastAsTypical is reflexive.

theorem Core.Inheritance.Prototype.atLeastAsTypical_trans {α : Type} (proto : Prototype α) (a b c : α) (hab : proto.atLeastAsTypical a b = true) (hbc : proto.atLeastAsTypical b c = true) : proto.atLeastAsTypical a c = true

atLeastAsTypical is transitive.