Government in Dependency Grammar

@cite{osborne-2019}

Formalizes government (@cite{osborne-2019}, Ch 4 §4.8, Ch 5): the mechanism by which a head determines the morphosyntactic form of its dependent.

Government is distinct from:

• Selection: what semantic type the head requires (animate, proposition, etc.)
• Subcategorization: which argument slots the head has
• Government: what morphosyntactic form the head requires (case, verb form)

Key Insight

The same valency frame (transitive verb taking two NP arguments) can have different government patterns: "want to go" vs "enjoy swimming" — same slot count, different morphological requirements on the complement.

Bridges

• → CRDC.lean: government complements ValencyFrame — valency says WHAT slots exist, government says HOW they're filled
• → HeadCriteria.lean: government is criterion 5 (morphological determination) — the governor is the head
• → Core/Basic.lean: ArgSlot has cat and depType; government adds morphological form constraints

inductive DepGrammar.Government.GovernedFeature : Type

A morphosyntactic feature that a head can govern on its dependent. @cite{osborne-2019}.

• case_ : GovernedFeature
• vform : GovernedFeature
• mood : GovernedFeature
• finiteness : GovernedFeature

def DepGrammar.Government.instReprGovernedFeature.repr : GovernedFeature → ℕ → Std.Format

Equations

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

instance DepGrammar.Government.instReprGovernedFeature : Repr GovernedFeature

Equations

• DepGrammar.Government.instReprGovernedFeature = { reprPrec := DepGrammar.Government.instReprGovernedFeature.repr }

instance DepGrammar.Government.instDecidableEqGovernedFeature : DecidableEq GovernedFeature

Equations

• DepGrammar.Government.instDecidableEqGovernedFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure DepGrammar.Government.GovRequirement : Type

A government requirement: head requires dependent to have specific feature value. @cite{osborne-2019}.

• headCat : UD.UPOS
• depRel : UD.DepRel
• feature : GovernedFeature
• requiredValue : String

def DepGrammar.Government.instReprGovRequirement.repr : GovRequirement → ℕ → Std.Format

Equations

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

instance DepGrammar.Government.instReprGovRequirement : Repr GovRequirement

Equations

• DepGrammar.Government.instReprGovRequirement = { reprPrec := DepGrammar.Government.instReprGovRequirement.repr }

def DepGrammar.Government.instDecidableEqGovRequirement.decEq (x✝ x✝¹ : GovRequirement) : Decidable (x✝ = x✝¹)

Equations

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

instance DepGrammar.Government.instDecidableEqGovRequirement : DecidableEq GovRequirement

Equations

• DepGrammar.Government.instDecidableEqGovRequirement = DepGrammar.Government.instDecidableEqGovRequirement.decEq

def DepGrammar.Government.govVerbInfinitive : GovRequirement

Verb + to-infinitive: "want to go" — want governs infinitival form. @cite{osborne-2019}.

Equations

• DepGrammar.Government.govVerbInfinitive = { headCat := UD.UPOS.VERB, depRel := UD.DepRel.xcomp, feature := DepGrammar.Government.GovernedFeature.vform, requiredValue := "infinitive" }

def DepGrammar.Government.govVerbBareInf : GovRequirement

Verb + bare infinitive: "make him go" — make governs base form. @cite{osborne-2019}.

Equations

• DepGrammar.Government.govVerbBareInf = { headCat := UD.UPOS.VERB, depRel := UD.DepRel.xcomp, feature := DepGrammar.Government.GovernedFeature.vform, requiredValue := "base" }

def DepGrammar.Government.govVerbGerund : GovRequirement

Verb + gerund: "enjoy swimming" — enjoy governs gerund form. @cite{osborne-2019}.

Equations

• DepGrammar.Government.govVerbGerund = { headCat := UD.UPOS.VERB, depRel := UD.DepRel.xcomp, feature := DepGrammar.Government.GovernedFeature.vform, requiredValue := "gerund" }

def DepGrammar.Government.govVerbFinite : GovRequirement

Verb + finite that-clause: "think that..." — think governs finite complement. @cite{osborne-2019}.

Equations

• DepGrammar.Government.govVerbFinite = { headCat := UD.UPOS.VERB, depRel := UD.DepRel.ccomp, feature := DepGrammar.Government.GovernedFeature.finiteness, requiredValue := "finite" }

def DepGrammar.Government.govPrepAcc : GovRequirement

Preposition + accusative: "with him/*he" — preposition governs accusative case. @cite{osborne-2019}.

Equations

• DepGrammar.Government.govPrepAcc = { headCat := UD.UPOS.ADP, depRel := UD.DepRel.obj, feature := DepGrammar.Government.GovernedFeature.case_, requiredValue := "acc" }

def DepGrammar.Government.englishGovRequirements : List GovRequirement

All English government requirements from @cite{osborne-2019}.

Equations

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

def DepGrammar.Government.matchGovFeature (w : Word) (feat : GovernedFeature) (reqVal : String) : Bool

Match a governed feature against a word's feature bundle. Returns true if the word has the required value.

Equations

• One or more equations did not get rendered due to their size.
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.finiteness reqVal = match w.features.finite with | true => reqVal == "finite" | false => reqVal == "nonfinite"
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.mood reqVal = true

def DepGrammar.Government.checkGovernment (t : DepTree) (govReqs : List GovRequirement) : Bool

Check if a dependency edge satisfies its government requirements.

Equations

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

structure DepGrammar.Government.GovernmentPattern : Type

A government pattern: a verb with its government requirements. Distinct from CRDC.ValencyFrame which captures WHAT dependents appear.

• verb : String
• requirements : List GovRequirement

def DepGrammar.Government.instReprGovernmentPattern.repr : GovernmentPattern → ℕ → Std.Format

Equations

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

instance DepGrammar.Government.instReprGovernmentPattern : Repr GovernmentPattern

Equations

• DepGrammar.Government.instReprGovernmentPattern = { reprPrec := DepGrammar.Government.instReprGovernmentPattern.repr }

def DepGrammar.Government.wantGov : GovernmentPattern

"want" governs infinitival complement: "want to go"

Equations

• DepGrammar.Government.wantGov = { verb := "want", requirements := [DepGrammar.Government.govVerbInfinitive] }

def DepGrammar.Government.enjoyGov : GovernmentPattern

"enjoy" governs gerund complement: "enjoy swimming"

Equations

• DepGrammar.Government.enjoyGov = { verb := "enjoy", requirements := [DepGrammar.Government.govVerbGerund] }

def DepGrammar.Government.thinkGov : GovernmentPattern

"think" governs finite complement: "think that..."

Equations

• DepGrammar.Government.thinkGov = { verb := "think", requirements := [DepGrammar.Government.govVerbFinite] }

def DepGrammar.Government.makeGov : GovernmentPattern

"make" governs bare infinitive: "make him go"

Equations

• DepGrammar.Government.makeGov = { verb := "make", requirements := [DepGrammar.Government.govVerbBareInf] }

theorem DepGrammar.Government.government_orthogonal_to_valency : (wantGov.requirements.length == enjoyGov.requirements.length && Option.map (fun (x : GovRequirement) => x.depRel) wantGov.requirements.head? == Option.map (fun (x : GovRequirement) => x.depRel) enjoyGov.requirements.head? && Option.map (fun (x : GovRequirement) => x.requiredValue) wantGov.requirements.head? != Option.map (fun (x : GovRequirement) => x.requiredValue) enjoyGov.requirements.head?) = true

Government and valency are orthogonal: valency says WHAT dependents, government says WHAT FORM. @cite{osborne-2019}. A verb can have the same valency (transitive, taking xcomp) but different government (infinitive vs gerund complement).

"want to go" and "enjoy swimming" — both take a VP complement (same valency: verb + xcomp), but want requires infinitive while enjoy requires gerund.

def DepGrammar.Government.ex_sheWantsToGo : DepTree

"She wants to go" — verb governs infinitival complement. Words: she(0) wants(1) to(2) go(3) Deps: wants → she (nsubj), wants → go (xcomp), go → to (mark)

Equations

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

def DepGrammar.Government.ex_sheEnjoysSw : DepTree

"She enjoys swimming" — verb governs gerund complement. Words: she(0) enjoys(1) swimming(2) Deps: enjoys → she (nsubj), enjoys → swimming (xcomp)

Equations

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

def DepGrammar.Government.ex_withHim : DepTree

"with him" — preposition governs accusative case. Words: with(0) him(1) Deps: with → him (obj)

Equations

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

def DepGrammar.Government.ex_withHe : DepTree

"with he" — preposition government violation (nominative instead of accusative).

Equations

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

theorem DepGrammar.Government.withHim_govOk : checkGovernment ex_withHim [govPrepAcc] = true

"with him" satisfies case government (accusative).

theorem DepGrammar.Government.withHe_govFail : checkGovernment ex_withHe [govPrepAcc] = false

"with he" violates case government (nominative instead of accusative).

theorem DepGrammar.Government.wantsToGo_govOk : checkGovernment ex_sheWantsToGo [govVerbInfinitive] = true

"She wants to go" satisfies infinitive government.

theorem DepGrammar.Government.enjoysSwimming_govOk : checkGovernment ex_sheEnjoysSw [govVerbGerund] = true

"She enjoys swimming" satisfies gerund government.

theorem DepGrammar.Government.same_valency_different_government : have wantFrame := CRDC.transitiveFrame "want"; have enjoyFrame := CRDC.transitiveFrame "enjoy"; (wantFrame.valents.length == enjoyFrame.valents.length && Option.map (fun (x : GovRequirement) => x.requiredValue) wantGov.requirements.head? != Option.map (fun (x : GovRequirement) => x.requiredValue) enjoyGov.requirements.head?) = true

Bridge → CRDC.lean: Same valency frame can have different government. Both "want" and "enjoy" are transitive (take xcomp), but differ in government. Valency frame (what slots exist) is independent of government (how slots are realized morphologically).

theorem DepGrammar.Government.government_implies_head : HeadCriteria.classifyRelation UD.DepRel.xcomp = HeadCriteria.RelationClass.coreArgument ∧ HeadCriteria.expectedCriteriaCount HeadCriteria.RelationClass.coreArgument = 6

Bridge → HeadCriteria.lean: Government is one of the six head criteria (criterion 5: morphological determination). The governor is the head. Core arguments satisfy all 6 criteria including government.

theorem DepGrammar.Government.argslot_agnostic_to_government : have slot := { depType := UD.DepRel.xcomp, dir := Dir.right, cat := some UD.UPOS.VERB }; (slot.depType == UD.DepRel.xcomp) = true

Bridge → Core/Basic.lean: ArgSlot captures what relation and direction a dependent has. Government adds a morphological dimension: the slot for xcomp is the same regardless of whether the governed form is infinitive or gerund.

theorem DepGrammar.Government.english_gov_requirements_count : englishGovRequirements.length = 5

Government requirements are distinct across all five English patterns.