Inheritance Networks — Basic Types and Taxonomy

@cite{hudson-2010}

Hudson's Word Grammar organizes all linguistic knowledge as networks of nodes connected by labeled directed links. Properties 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.

Hudson's six primitive relations (Ch 3 summary box, p. 68)

isA, argument, value, or (choice), quantity, identity — listed verbatim in @cite{hudson-2010}'s Ch 3 summary box on p. 68 under "Links between concepts are therefore of two types: primitive relations / conceptual relations".

This module distinguishes three link kinds at the type level:

• isA — taxonomic classification (bird isA animal)
• or — mutual exclusivity / choice sets (male or female)
• prop — named property/relation links (bird --front-limb--> wing), covering argument, value, identity, quantity via the relation label

Key definitions

• LinkKind, Link, Network
• Network.nodeUniverse — finite carrier derived from the link list
• parents, ancestorsBound, ancestors — computational taxonomy traversal
• IsA — the canonical reflexive-transitive isA, defined as Relation.ReflTransGen of the parent edge

IsA is the API; parents/ancestors are computational evidence producers. IsA is decidable for any concrete network via the Relation.ReflTransGen.decidable_of_finite_step substrate, so positive and negative IsA claims both reduce by decide. Termination of ancestors is bounded by nodeUniverse.length, not a magic constant.

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 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Inheritance.instReprLinkKind : Repr LinkKind

Equations

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

@[implicit_reducible]

instance Core.Inheritance.instDecidableEqLinkKind : DecidableEq LinkKind

Equations

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

structure Core.Inheritance.Link (α : Type u) (R : Type v) : Type (max u v)

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

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.Network.nodeUniverse {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) : List α

The finite set of nodes mentioned by the network's links. Used as the natural termination bound for traversals — the longest acyclic path in a finite network cannot exceed nodeUniverse.length steps.

Equations

• net.nodeUniverse = (List.map Core.Inheritance.Link.source net.links ++ List.map Core.Inheritance.Link.target net.links).dedup

def Core.Inheritance.parents {α : Type u} {R : Type v} [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.ancestorsBound {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) : ℕ → List α

Bounded transitive closure of parents. The bound parameter is intended to be ≥ (nodeUniverse net).length; under that assumption every reachable ancestor appears. Structurally recursive on Nat to keep decide happy.

Equations

• Core.Inheritance.ancestorsBound net node 0 = []
• Core.Inheritance.ancestorsBound net node n.succ = Core.Inheritance.parents net node ++ List.flatMap (fun (p : α) => Core.Inheritance.ancestorsBound net p n) (Core.Inheritance.parents net node)

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

Transitive ancestors of node in the isA taxonomy. The recursion bound is derived from the network itself (number of distinct nodes), so finite networks always traverse to fixpoint without a magic constant.

Equations

• Core.Inheritance.ancestors net node = Core.Inheritance.ancestorsBound net node net.nodeUniverse.length

def Core.Inheritance.isAEdge {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (a b : α) : Prop

The single-step parent relation.

Equations

• Core.Inheritance.isAEdge net a b = (b ∈ Core.Inheritance.parents net a)

@[implicit_reducible]

instance Core.Inheritance.instDecidableIsAEdge {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (a b : α) : Decidable (isAEdge net a b)

Equations

• Core.Inheritance.instDecidableIsAEdge net a b = Core.Inheritance.instDecidableIsAEdge._aux_1 net a b

def Core.Inheritance.IsA {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (a b : α) : Prop

Reflexive-transitive isA: a inherits from b along the chain of isA links. Defined as Relation.ReflTransGen of the parent edge — the same construction mathlib uses for transitive closures elsewhere, so every lemma about ReflTransGen (and the Preorder structure in Core.Inheritance.Order) applies for free.

Equations

• Core.Inheritance.IsA net a b = Relation.ReflTransGen (Core.Inheritance.isAEdge net) a b

theorem Core.Inheritance.IsA.refl {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (a : α) : IsA net a a

Every node IsA itself.

theorem Core.Inheritance.IsA.trans {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) {a b c : α} (hab : IsA net a b) (hbc : IsA net b c) : IsA net a c

IsA is transitive (mathlib gives this for free via ReflTransGen.trans).

theorem Core.Inheritance.mem_nodeUniverse_of_mem_parents {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (a b : α) (h : b ∈ parents net a) : b ∈ net.nodeUniverse

Direct parents of any node are mentioned by some isA link, hence in nodeUniverse. The "successor in universe" witness fed to the substrate.

@[implicit_reducible]

instance Core.Inheritance.IsA.decidable {α : Type u} {R : Type v} [DecidableEq α] [DecidableEq R] (net : Network α R) (a b : α) : Decidable (IsA net a b)

IsA is decidable on finite networks: the network's own nodeUniverse provides the bound, and Relation.ReflTransGen.decidable_of_finite_step supplies the path-compression argument.

Equations

• Core.Inheritance.IsA.decidable net a b = Relation.ReflTransGen.decidable_of_finite_step (Core.Inheritance.parents net) net.nodeUniverse ⋯ ⋯ a b