WG Network Integration

Connects Core.Inheritance (Hudson's isA/prop network model) to the dependency grammar module so that word classes and their argument structures live in a single WG network. @cite{hudson-2010}

Argument structures are inherited via default inheritance: a transitive verb inherits from verb, but a passive can override locally (the most specific value wins — what @cite{hudson-2010} calls the "Best Fit Principle").

Subject-auxiliary inversion is modeled as subtype inheritance: the inverted auxiliary (Hudson uses both "inverted" and "interrogative" for the same word-class subtype, viewed from form vs. semantic side — see §11.6.1, p. 308) is a subtype of auxiliary that locally overrides the subject's direction from left to right, following @cite{hudson-2010}'s treatment of inversion as a word-class subtype rather than a movement rule.

inductive WordGrammar.WGNode : Type

Nodes in a WG network: word classes, dependency relations, or directions.

• wordClass (name : String) : WGNode
• depRel (rel : UD.DepRel) : WGNode
• dir (d : DepGrammar.Dir) : WGNode

def WordGrammar.instReprWGNode.repr : WGNode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WordGrammar.instReprWGNode : Repr WGNode

Equations

• WordGrammar.instReprWGNode = { reprPrec := WordGrammar.instReprWGNode.repr }

@[implicit_reducible]

instance WordGrammar.instDecidableEqWGNode : DecidableEq WGNode

Equations

• WordGrammar.instDecidableEqWGNode = WordGrammar.instDecidableEqWGNode.decEq

def WordGrammar.instDecidableEqWGNode.decEq (x✝ x✝¹ : WGNode) : Decidable (x✝ = x✝¹)

Equations

• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.wordClass a) (WordGrammar.WGNode.wordClass b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.wordClass name) (WordGrammar.WGNode.depRel rel) = isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.wordClass name) (WordGrammar.WGNode.dir d) = isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.depRel rel) (WordGrammar.WGNode.wordClass name) = isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.depRel a) (WordGrammar.WGNode.depRel b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.depRel rel) (WordGrammar.WGNode.dir d) = isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.dir d) (WordGrammar.WGNode.wordClass name) = isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.dir d) (WordGrammar.WGNode.depRel rel) = isFalse ⋯
• WordGrammar.instDecidableEqWGNode.decEq (WordGrammar.WGNode.dir a) (WordGrammar.WGNode.dir b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive WordGrammar.WGRel : Type

Relation labels for property links in a WG network. In @cite{hudson-2010}'s terms, these are the named relations that connect word-class nodes to their syntactic properties.

• argSlot (idx : ℕ) : WGRel
• slotDir (idx : ℕ) : WGRel

def WordGrammar.instReprWGRel.repr : WGRel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WordGrammar.instReprWGRel : Repr WGRel

Equations

• WordGrammar.instReprWGRel = { reprPrec := WordGrammar.instReprWGRel.repr }

def WordGrammar.instDecidableEqWGRel.decEq (x✝ x✝¹ : WGRel) : Decidable (x✝ = x✝¹)

Equations

• WordGrammar.instDecidableEqWGRel.decEq (WordGrammar.WGRel.argSlot a) (WordGrammar.WGRel.argSlot b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• WordGrammar.instDecidableEqWGRel.decEq (WordGrammar.WGRel.argSlot idx) (WordGrammar.WGRel.slotDir idx_1) = isFalse ⋯
• WordGrammar.instDecidableEqWGRel.decEq (WordGrammar.WGRel.slotDir idx) (WordGrammar.WGRel.argSlot idx_1) = isFalse ⋯
• WordGrammar.instDecidableEqWGRel.decEq (WordGrammar.WGRel.slotDir a) (WordGrammar.WGRel.slotDir b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WordGrammar.instDecidableEqWGRel : DecidableEq WGRel

Equations

• WordGrammar.instDecidableEqWGRel = WordGrammar.instDecidableEqWGRel.decEq

@[reducible, inline]

abbrev WordGrammar.WGNetwork : Type

Abbreviation for a WG inheritance network.

Equations

• WordGrammar.WGNetwork = Core.Inheritance.Network WordGrammar.WGNode WordGrammar.WGRel

def WordGrammar.isALink (child parent : String) : Core.Inheritance.Link WGNode WGRel

Create an isA link between word classes.

Equations

• WordGrammar.isALink child parent = { kind := Core.Inheritance.LinkKind.isA, source := WordGrammar.WGNode.wordClass child, target := WordGrammar.WGNode.wordClass parent }

def WordGrammar.argSlotLink (wc : String) (idx : ℕ) (rel : UD.DepRel) : Core.Inheritance.Link WGNode WGRel

Create a property link for an argument slot's dependency relation.

Equations

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

def WordGrammar.slotDirLink (wc : String) (idx : ℕ) (d : DepGrammar.Dir) : Core.Inheritance.Link WGNode WGRel

Create a property link for an argument slot's direction.

Equations

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

def WordGrammar.resolveSlot (net : WGNetwork) (wc : String) (idx : ℕ) : Option DepGrammar.ArgSlot

Look up one argument slot from the network for a word class, using default inheritance. Returns none if the slot is not defined.

Equations

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

def WordGrammar.resolveArgStr (net : WGNetwork) (wc : String) (maxSlots : ℕ := 10) : DepGrammar.ArgStr

Resolve the full argument structure for a word class by collecting slots 0, 1, 2, ... until one is not found. Uses default inheritance, so locally specified slots override inherited ones.

Equations

• WordGrammar.resolveArgStr net wc maxSlots = { slots := WordGrammar.resolveArgStr.go net wc 0 maxSlots [] }

def WordGrammar.resolveArgStr.go (net : WGNetwork) (wc : String) (idx fuel : ℕ) (acc : List DepGrammar.ArgSlot) : List DepGrammar.ArgSlot

Equations

• One or more equations did not get rendered due to their size.
• WordGrammar.resolveArgStr.go net wc idx 0 acc = acc.reverse

def WordGrammar.englishAuxNet : WGNetwork

A WG network encoding the English auxiliary word-class hierarchy, following @cite{hudson-2010}:

• verb has slot 0 = nsubj/left (subject precedes verb by default)
• transitive isA verb, adds slot 1 = obj/right
• passive isA transitive, overrides slot 1 to obl/right (by-phrase)
• auxiliary isA verb, adds slot 1 = aux/right (main verb)
• inverted_auxiliary isA auxiliary, overrides slot 0 direction to right — the subject follows the auxiliary in questions

The last point is the key to subject-auxiliary inversion: the inverted auxiliary is a subtype of auxiliary that locally overrides the subject's position. Default inheritance does the rest — the inverted auxiliary inherits nsubj from verb (via auxiliary) but gets direction = right from its own local specification.

Equations

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

theorem WordGrammar.network_transitive_slot0 : resolveSlot englishAuxNet "transitive" 0 = some { depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.left }

A transitive verb inherits nsubj/left from verb and adds obj/right locally — the network-derived argStr matches the manual argStr_VN (modulo optional fields that default).

theorem WordGrammar.network_transitive_slot1 : resolveSlot englishAuxNet "transitive" 1 = some { depType := UD.DepRel.obj, dir := DepGrammar.Dir.right }

theorem WordGrammar.bestFit_passive_overrides : resolveSlot englishAuxNet "passive" 1 = some { depType := UD.DepRel.obl, dir := DepGrammar.Dir.right }

A passive verb's locally specified slot 1 (obl/right) overrides the inherited transitive slot 1 (obj/right) — default inheritance in action.

theorem WordGrammar.network_aux_slot0 : resolveSlot englishAuxNet "auxiliary" 0 = some { depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.left }

The non-inverted auxiliary inherits nsubj/left from verb for slot 0.

theorem WordGrammar.network_argStr_matches_manual : (resolveArgStr englishAuxNet "transitive").slots = [{ depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.left }, { depType := UD.DepRel.obj, dir := DepGrammar.Dir.right }]

The network-derived arg structure for a transitive verb has the same slots as the manually defined argStr_VN.

theorem WordGrammar.inversion_by_subtype : resolveSlot englishAuxNet "auxiliary" 0 = some { depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.left } ∧ resolveSlot englishAuxNet "inverted_auxiliary" 0 = some { depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.right }

The interrogative/inverted auxiliary inherits nsubj from verb (via auxiliary) but its locally specified direction (right) overrides the inherited direction (left). This is Hudson's subtype analysis of inversion (@cite{hudson-2010} §11.6.1, Fig 11.13): the inverted auxiliary is not a separate lexical rule — it's a word-class subtype.

theorem WordGrammar.inverted_aux_inherits_main_verb_slot : resolveSlot englishAuxNet "inverted_auxiliary" 1 = some { depType := UD.DepRel.aux, dir := DepGrammar.Dir.right }

The inverted auxiliary inherits its main-verb slot (aux/right) from auxiliary without overriding it — only the subject direction changes.

theorem WordGrammar.network_aux_argStr : (resolveArgStr englishAuxNet "auxiliary").slots = [{ depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.left }, { depType := UD.DepRel.aux, dir := DepGrammar.Dir.right }]

The full argument structure for the non-inverted auxiliary: nsubj/left (inherited from verb) + aux/right (local).

theorem WordGrammar.network_inverted_aux_argStr : (resolveArgStr englishAuxNet "inverted_auxiliary").slots = [{ depType := UD.DepRel.nsubj, dir := DepGrammar.Dir.right }, { depType := UD.DepRel.aux, dir := DepGrammar.Dir.right }]

The full argument structure for the inverted auxiliary: nsubj/right (local override) + aux/right (inherited from auxiliary).

def WordGrammar.wordClassForClauseType : Features.ClauseForm → String

Map clause type to the word class that licenses the auxiliary in that context. Matrix questions require an interrogative auxiliary (subject follows); all other clause types use the default auxiliary (subject precedes).

Equations

• WordGrammar.wordClassForClauseType Features.ClauseForm.matrixQuestion = "inverted_auxiliary"
• WordGrammar.wordClassForClauseType x✝ = "auxiliary"

def WordGrammar.wgLicenses (net : WGNetwork) (t : DepGrammar.DepTree) (auxIdx : ℕ) (ct : Features.ClauseForm) : Bool

License a dependency tree via the WG network: look up the word class for the clause type, resolve its argument structure from the network, and check the tree satisfies it. This is the end-to-end chain: ClauseForm → wordClass → network → argStr → satisfiesArgStr.

Equations

• WordGrammar.wgLicenses net t auxIdx ct = DepGrammar.satisfiesArgStr t auxIdx (WordGrammar.resolveArgStr net (WordGrammar.wordClassForClauseType ct))