Government in Dependency Grammar

Formalizes government ([Osb19], Ch. 4 §4.8 and Ch. 5): the mechanism by which a head determines the morphosyntactic form of its dependent — case on a complement of a preposition, verb form on the complement of a control verb, finiteness of a clausal complement.

Government is orthogonal to valency: "want to go" and "enjoy swimming" share an xcomp slot but require different forms (infinitive vs. gerund) on the complement.

Main declarations

• GovernedFeature, GovernedValue — the morphosyntactic dimensions a head can govern, with a typed value space (no String tags).
• GovRequirement — one head-cat / dep-rel / feature / required-value 4-tuple, with five English instances from [Osb19].
• checkGovernment — Bool checker that verifies every dependency in a DepTree honours every requirement that applies to it.
• withHim_govOk / withHe_govFail etc. — small fixtures exercising the checker on accusative-vs-nominative preposition complements and infinitive-vs-gerund verb complements.

Implementation notes

• Bool checker, not Prop predicate: matches the substrate-wide convention in this directory; Prop+Decidable migration is out of scope for the cleanup pass.
• No bridge theorems to HeadCriteria. The audit flagged the previous government_implies_head and argslot_agnostic_to_government as rfl-on-stipulation tautologies; cross-framework rivalry against HPSG COMPS|VFORM or Minimalist selectional features belongs in a paper-anchored Studies file, not the substrate.

Government dimensions and values

inductive DepGrammar.Government.GovernedFeature : Type

A morphosyntactic feature a head can govern on its dependent. [Osb19].

• 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.

@[implicit_reducible]

instance DepGrammar.Government.instReprGovernedFeature : Repr GovernedFeature

Equations

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

@[implicit_reducible]

instance DepGrammar.Government.instDecidableEqGovernedFeature : DecidableEq GovernedFeature

Equations

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

inductive DepGrammar.Government.GovernedValue : Type

The typed value space for governed features (replaces stringly-typed requirement tags). [Osb19].

• acc : GovernedValue
• nom : GovernedValue
• gen : GovernedValue
• infinitive : GovernedValue
• base : GovernedValue
• gerund : GovernedValue
• participle : GovernedValue
• finite : GovernedValue
• nonfinite : GovernedValue

@[implicit_reducible]

instance DepGrammar.Government.instReprGovernedValue : Repr GovernedValue

Equations

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

def DepGrammar.Government.instReprGovernedValue.repr : GovernedValue → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DepGrammar.Government.instDecidableEqGovernedValue : DecidableEq GovernedValue

Equations

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

structure DepGrammar.Government.GovRequirement : Type

A government requirement: a head of category headCat requires its dependent on relation depRel to have value requiredValue of feature feature. [Osb19].

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

@[implicit_reducible]

instance DepGrammar.Government.instReprGovRequirement : Repr GovRequirement

Equations

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

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

Equations

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

@[implicit_reducible]

instance DepGrammar.Government.instDecidableEqGovRequirement : DecidableEq GovRequirement

Equations

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

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

Equations

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

English government data

def DepGrammar.Government.govVerbInfinitive : GovRequirement

"want to go" — want governs the infinitival form of its xcomp.

Equations

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

def DepGrammar.Government.govVerbBareInf : GovRequirement

"make him go" — make governs the bare form of its xcomp.

Equations

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

def DepGrammar.Government.govVerbGerund : GovRequirement

"enjoy swimming" — enjoy governs the gerund form of its xcomp.

Equations

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

def DepGrammar.Government.govVerbFinite : GovRequirement

"think that ..." — think governs a finite ccomp.

Equations

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

def DepGrammar.Government.govPrepAcc : GovRequirement

"with him / *with he" — preposition governs accusative on its obj.

Equations

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

def DepGrammar.Government.englishGovRequirements : List GovRequirement

The English government patterns from [Osb19].

Equations

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

Government checking

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

Does the word w carry the value reqVal of feature feat? Returns true when the relevant feature slot is unspecified (vacuous satisfaction); a marked slot whose value differs from the requirement fails.

Equations

• One or more equations did not get rendered due to their size.
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.Case reqVal✝ = true
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.Case DepGrammar.Government.GovernedValue.acc = decide (c = Case.acc)
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.Case DepGrammar.Government.GovernedValue.nom = decide (c = Case.nom)
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.Case DepGrammar.Government.GovernedValue.gen = decide (c = Case.gen)
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.Case reqVal✝ = true
• DepGrammar.Government.matchGovFeature w DepGrammar.Government.GovernedFeature.Mood reqVal = true

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

A dependency tree satisfies its government requirements when every matching head-cat / dep-rel pair carries the required value.

Equations

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

Example trees

def DepGrammar.Government.exSheWantsToGo : DepTree

"She wants to go": wants(1) heads she(0) (nsubj) and go(3) (xcomp); go(3) heads to(2) (mark).

Equations

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

def DepGrammar.Government.exSheEnjoysSwimming : DepTree

"She enjoys swimming": enjoys(1) heads she(0) (nsubj) and swimming(2) (xcomp).

Equations

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

def DepGrammar.Government.exWithHim : DepTree

"with him": preposition governs accusative — well-formed.

Equations

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

def DepGrammar.Government.exWithHe : DepTree

"with he": preposition government violation (nominative for accusative).

Equations

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

def DepGrammar.Government.exPrepDatObj : DepTree

Regression guard for matchGovFeature: a preposition's obj bearing a marked case other than the required accusative (here dative) violates government. The earlier checker fell through to true for any case outside {nom, acc, gen}, so a dative object spuriously satisfied govPrepAcc.

Equations

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

Checker behaviour on the fixtures

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

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

theorem DepGrammar.Government.prepDatObj_govFail : checkGovernment exPrepDatObj [govPrepAcc] = false

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

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