WG Network Integration

Connects WordGrammar.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. [Hud10]

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 [Hud10] 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 [Hud10]'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 : DependencyGrammar.Dir) : WGNode

@[instance_reducible]

instance WordGrammar.instReprWGNode : Repr WGNode

Equations

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

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

Equations

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

@[instance_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 [Hud10]'s terms, these are the named relations that connect word-class nodes to their syntactic properties.

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

@[instance_reducible]

instance WordGrammar.instReprWGRel : Repr WGRel

Equations

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

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

Equations

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

@[instance_reducible]

instance WordGrammar.instDecidableEqWGRel : DecidableEq WGRel

Equations

• WordGrammar.instDecidableEqWGRel = WordGrammar.instDecidableEqWGRel.decEq

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 ⋯

@[reducible, inline]

abbrev WordGrammar.WGNetwork : Type

Abbreviation for a WG inheritance network.

Equations

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

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

Create an isA link between word classes.

Equations

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

def WordGrammar.argSlotLink (wc : String) (idx : ℕ) (rel : UD.DepRel) : 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 : DependencyGrammar.Dir) : 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 DependencyGrammar.Valency.Slot

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.resolveValency (net : WGNetwork) (wc : String) (maxSlots : ℕ := 10) : DependencyGrammar.Valency

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.resolveValency net wc maxSlots = WordGrammar.resolveValency.go net wc 0 maxSlots []

def WordGrammar.resolveValency.go (net : WGNetwork) (wc : String) (idx fuel : ℕ) (acc : List DependencyGrammar.Valency.Slot) : List DependencyGrammar.Valency.Slot

Equations

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

def WordGrammar.englishAuxNet : WGNetwork

A WG network encoding the English auxiliary word-class hierarchy, following [Hud10]:

• 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 := DependencyGrammar.Dir.left }

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

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

theorem WordGrammar.bestFit_passive_overrides : resolveSlot englishAuxNet "passive" 1 = some { depType := UD.DepRel.obl, dir := DependencyGrammar.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 := DependencyGrammar.Dir.left }

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

theorem WordGrammar.network_valency_matches_manual : resolveValency englishAuxNet "transitive" = [{ depType := UD.DepRel.nsubj, dir := DependencyGrammar.Dir.left }, { depType := UD.DepRel.obj, dir := DependencyGrammar.Dir.right }]

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

theorem WordGrammar.inversion_by_subtype : resolveSlot englishAuxNet "auxiliary" 0 = some { depType := UD.DepRel.nsubj, dir := DependencyGrammar.Dir.left } ∧ resolveSlot englishAuxNet "inverted_auxiliary" 0 = some { depType := UD.DepRel.nsubj, dir := DependencyGrammar.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 ([Hud10] §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 := DependencyGrammar.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_valency : resolveValency englishAuxNet "auxiliary" = [{ depType := UD.DepRel.nsubj, dir := DependencyGrammar.Dir.left }, { depType := UD.DepRel.aux, dir := DependencyGrammar.Dir.right }]

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

theorem WordGrammar.network_inverted_aux_valency : resolveValency englishAuxNet "inverted_auxiliary" = [{ depType := UD.DepRel.nsubj, dir := DependencyGrammar.Dir.right }, { depType := UD.DepRel.aux, dir := DependencyGrammar.Dir.right }]

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

def WordGrammar.wordClassFor (f : Mood.Illocutionary) (e : Clause.EmbeddingContext) : String

Map force and embedding context to the word class that licenses the auxiliary. Matrix interrogatives require an inverted auxiliary (subject follows); everything else uses the default auxiliary (subject precedes).

Equations

• WordGrammar.wordClassFor f e = if f = Mood.Illocutionary.interrogative ∧ e = Clause.EmbeddingContext.matrix then "inverted_auxiliary" else "auxiliary"

def WordGrammar.WGLicenses {n : ℕ} (net : WGNetwork) (t : DependencyGrammar.Graph n) (auxIdx : Fin n) (f : Mood.Illocutionary) (e : Clause.EmbeddingContext) : Prop

The WG network licenses a dependency tree: the word class for the clause context resolves to an argument structure from the network, which the tree satisfies. The end-to-end chain: force × context → wordClass → network → valency → SatisfiesValency.

Equations

• WordGrammar.WGLicenses net t auxIdx f e = DependencyGrammar.SatisfiesValency t auxIdx (WordGrammar.resolveValency net (WordGrammar.wordClassFor f e))

@[instance_reducible]

instance WordGrammar.instDecidableWGLicenses {n : ℕ} (net : WGNetwork) (t : DependencyGrammar.Graph n) (auxIdx : Fin n) (f : Mood.Illocutionary) (e : Clause.EmbeddingContext) : Decidable (WGLicenses net t auxIdx f e)

Equations

• WordGrammar.instDecidableWGLicenses net t auxIdx f e = WordGrammar.instDecidableWGLicenses._aux_1 net t auxIdx f e