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-1984} @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} later calls the "Best Fit Principle").

Subject-auxiliary inversion is modeled as subtype inheritance: the interrogative auxiliary is a subtype of auxiliary that locally overrides the subject's direction from left to right. This faithfully follows @cite{hudson-1984} pp. 117-118, where the inverted auxiliary is treated as a special subtype of "auxiliary" with its own word-order requirements:

model (interrogative): auxiliary and tensed subject (interrogative): s, interrogative < s

inductive DepGrammar.WG.WGNode : Type

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

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

def DepGrammar.WG.instReprWGNode.repr : WGNode → ℕ → Std.Format

Equations

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

instance DepGrammar.WG.instReprWGNode : Repr WGNode

Equations

• DepGrammar.WG.instReprWGNode = { reprPrec := DepGrammar.WG.instReprWGNode.repr }

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

Equations

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

instance DepGrammar.WG.instDecidableEqWGNode : DecidableEq WGNode

Equations

• DepGrammar.WG.instDecidableEqWGNode = DepGrammar.WG.instDecidableEqWGNode.decEq

def DepGrammar.WG.instBEqWGNode.beq : WGNode → WGNode → Bool

Equations

• DepGrammar.WG.instBEqWGNode.beq (DepGrammar.WG.WGNode.wordClass a) (DepGrammar.WG.WGNode.wordClass b) = (a == b)
• DepGrammar.WG.instBEqWGNode.beq (DepGrammar.WG.WGNode.depRel a) (DepGrammar.WG.WGNode.depRel b) = (a == b)
• DepGrammar.WG.instBEqWGNode.beq (DepGrammar.WG.WGNode.dir a) (DepGrammar.WG.WGNode.dir b) = (a == b)
• DepGrammar.WG.instBEqWGNode.beq x✝¹ x✝ = false

instance DepGrammar.WG.instBEqWGNode : BEq WGNode

Equations

• DepGrammar.WG.instBEqWGNode = { beq := DepGrammar.WG.instBEqWGNode.beq }

inductive DepGrammar.WG.WGRel : Type

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

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

instance DepGrammar.WG.instReprWGRel : Repr WGRel

Equations

• DepGrammar.WG.instReprWGRel = { reprPrec := DepGrammar.WG.instReprWGRel.repr }

def DepGrammar.WG.instReprWGRel.repr : WGRel → ℕ → Std.Format

Equations

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

instance DepGrammar.WG.instDecidableEqWGRel : DecidableEq WGRel

Equations

• DepGrammar.WG.instDecidableEqWGRel = DepGrammar.WG.instDecidableEqWGRel.decEq

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

Equations

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

def DepGrammar.WG.instBEqWGRel.beq : WGRel → WGRel → Bool

Equations

• DepGrammar.WG.instBEqWGRel.beq (DepGrammar.WG.WGRel.argSlot a) (DepGrammar.WG.WGRel.argSlot b) = (a == b)
• DepGrammar.WG.instBEqWGRel.beq (DepGrammar.WG.WGRel.slotDir a) (DepGrammar.WG.WGRel.slotDir b) = (a == b)
• DepGrammar.WG.instBEqWGRel.beq x✝¹ x✝ = false

instance DepGrammar.WG.instBEqWGRel : BEq WGRel

Equations

• DepGrammar.WG.instBEqWGRel = { beq := DepGrammar.WG.instBEqWGRel.beq }

@[reducible, inline]

abbrev DepGrammar.WG.WGNetwork : Type

Abbreviation for a WG inheritance network.

Equations

• DepGrammar.WG.WGNetwork = Core.Inheritance.Network DepGrammar.WG.WGNode DepGrammar.WG.WGRel

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

Create an isA link between word classes.

Equations

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

def DepGrammar.WG.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 DepGrammar.WG.slotDirLink (wc : String) (idx : ℕ) (d : 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 DepGrammar.WG.resolveSlot (net : WGNetwork) (wc : String) (idx : ℕ) : Option 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 DepGrammar.WG.resolveArgStr (net : WGNetwork) (wc : String) (maxSlots : ℕ := 10) : 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

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

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

Equations

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

def DepGrammar.WG.englishAuxNet : WGNetwork

A WG network encoding the English auxiliary word-class hierarchy, following @cite{hudson-1984} Ch. 3:

• 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)
• interrogative_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 interrogative auxiliary is a subtype of auxiliary that locally overrides the subject's position. Default inheritance does the rest — the interrogative auxiliary inherits nsubj from verb (via auxiliary) but gets direction = right from its own local specification. (@cite{hudson-1984} pp. 117-118)

Equations

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

theorem DepGrammar.WG.network_transitive_slot0 : resolveSlot englishAuxNet "transitive" 0 = some { depType := UD.DepRel.nsubj, dir := 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 DepGrammar.WG.network_transitive_slot1 : resolveSlot englishAuxNet "transitive" 1 = some { depType := UD.DepRel.obj, dir := Dir.right }

theorem DepGrammar.WG.bestFit_passive_overrides : resolveSlot englishAuxNet "passive" 1 = some { depType := UD.DepRel.obl, dir := 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 DepGrammar.WG.network_aux_slot0 : resolveSlot englishAuxNet "auxiliary" 0 = some { depType := UD.DepRel.nsubj, dir := Dir.left }

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

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

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

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

The interrogative 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: the interrogative auxiliary is not a separate lexical rule — it's a word-class subtype.

theorem DepGrammar.WG.interrogative_aux_inherits_main_verb_slot : resolveSlot englishAuxNet "interrogative_auxiliary" 1 = some { depType := UD.DepRel.aux, dir := Dir.right }

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

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

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

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

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

def DepGrammar.WG.wordClassForClauseType : ClauseType → 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

• DepGrammar.WG.wordClassForClauseType ClauseType.matrixQuestion = "interrogative_auxiliary"
• DepGrammar.WG.wordClassForClauseType x✝ = "auxiliary"

def DepGrammar.WG.wgLicenses (net : WGNetwork) (t : DepTree) (auxIdx : ℕ) (ct : ClauseType) : 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: ClauseType → wordClass → network → argStr → satisfiesArgStr.

Equations

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