structure DepGrammar.HeadCriteria.HeadCriterion : Type

The six criteria for head-dependent relations.

• name : String
• satisfied : Dependency → List Word → Bool

  Does this criterion identify H as head in the given dependency?

def DepGrammar.HeadCriteria.categoryDetermination : HeadCriterion

Category determination: H determines the syntactic category of the phrase. Operationalized: the phrase's category equals the head's category.

Equations

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

def DepGrammar.HeadCriteria.obligatoriness : HeadCriterion

Obligatoriness: H is obligatory in C; D may be optional. Operationalized: removing D yields a grammatical result; removing H does not.

Equations

• DepGrammar.HeadCriteria.obligatoriness = { name := "Obligatoriness", satisfied := fun (_dep : DepGrammar.Dependency) (_words : List Word) => true }

def DepGrammar.HeadCriteria.selection (argStr : ArgStr) : HeadCriterion

Selection: H selects D (subcategorizes for it). Operationalized: H's argument structure includes a slot matching D.

Equations

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

def DepGrammar.HeadCriteria.morphologicalDetermination : HeadCriterion

Morphological determination: form of D depends on H. Operationalized: D agrees with H in some features (agreement) or H governs D's morphological form (case government).

Equations

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

def DepGrammar.HeadCriteria.positionalDetermination (argStr : ArgStr) : HeadCriterion

Positional determination: D's linear position is specified relative to H. Operationalized: there is a direction constraint on D relative to H.

Equations

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

def DepGrammar.HeadCriteria.criterionCount (criteria : List HeadCriterion) (dep : Dependency) (words : List Word) : ℕ

Count how many criteria a dependency satisfies.

Equations

• DepGrammar.HeadCriteria.criterionCount criteria dep words = (List.filter (fun (x : DepGrammar.HeadCriteria.HeadCriterion) => x.satisfied dep words) criteria).length

def DepGrammar.HeadCriteria.isPrototypicalHead (criteria : List HeadCriterion) (dep : Dependency) (words : List Word) (threshold : ℕ := 4) : Bool

A dependency is a prototypical head-dependent relation if it satisfies most criteria (@cite{hudson-1990}'s prototype structure).

Equations

• DepGrammar.HeadCriteria.isPrototypicalHead criteria dep words threshold = decide (DepGrammar.HeadCriteria.criterionCount criteria dep words ≥ threshold)

inductive DepGrammar.HeadCriteria.RelationClass : Type

How many criteria does each class of UD relation typically satisfy?

Core arguments (nsubj, obj) satisfy all six: head determines category, selects dependent, governs agreement, and specifies position.

Function word relations (det, aux, case) are controversial: the function word often determines morphological form but the content word determines category. This is why UD treats content words as heads — they satisfy more criteria overall.

• coreArgument : RelationClass
• modifier : RelationClass
• functionWord : RelationClass

instance DepGrammar.HeadCriteria.instReprRelationClass : Repr RelationClass

Equations

• DepGrammar.HeadCriteria.instReprRelationClass = { reprPrec := DepGrammar.HeadCriteria.instReprRelationClass.repr }

def DepGrammar.HeadCriteria.instReprRelationClass.repr : RelationClass → ℕ → Std.Format

Equations

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

instance DepGrammar.HeadCriteria.instDecidableEqRelationClass : DecidableEq RelationClass

Equations

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

def DepGrammar.HeadCriteria.classifyRelation : UD.DepRel → RelationClass

Classify a UD relation by how prototypically "head-dependent" it is.

Equations

• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.nsubj = DepGrammar.HeadCriteria.RelationClass.coreArgument
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.obj = DepGrammar.HeadCriteria.RelationClass.coreArgument
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.iobj = DepGrammar.HeadCriteria.RelationClass.coreArgument
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.csubj = DepGrammar.HeadCriteria.RelationClass.coreArgument
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.ccomp = DepGrammar.HeadCriteria.RelationClass.coreArgument
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.xcomp = DepGrammar.HeadCriteria.RelationClass.coreArgument
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.amod = DepGrammar.HeadCriteria.RelationClass.modifier
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.advmod = DepGrammar.HeadCriteria.RelationClass.modifier
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.nmod = DepGrammar.HeadCriteria.RelationClass.modifier
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.obl = DepGrammar.HeadCriteria.RelationClass.modifier
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.advcl = DepGrammar.HeadCriteria.RelationClass.modifier
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.acl = DepGrammar.HeadCriteria.RelationClass.modifier
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.det = DepGrammar.HeadCriteria.RelationClass.functionWord
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.aux = DepGrammar.HeadCriteria.RelationClass.functionWord
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.case_ = DepGrammar.HeadCriteria.RelationClass.functionWord
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.mark = DepGrammar.HeadCriteria.RelationClass.functionWord
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.cop = DepGrammar.HeadCriteria.RelationClass.functionWord
• DepGrammar.HeadCriteria.classifyRelation UD.DepRel.cc = DepGrammar.HeadCriteria.RelationClass.functionWord
• DepGrammar.HeadCriteria.classifyRelation x✝ = DepGrammar.HeadCriteria.RelationClass.modifier

def DepGrammar.HeadCriteria.expectedCriteriaCount : RelationClass → ℕ

Core arguments satisfy the most criteria.

Equations

• DepGrammar.HeadCriteria.expectedCriteriaCount DepGrammar.HeadCriteria.RelationClass.coreArgument = 6
• DepGrammar.HeadCriteria.expectedCriteriaCount DepGrammar.HeadCriteria.RelationClass.modifier = 3
• DepGrammar.HeadCriteria.expectedCriteriaCount DepGrammar.HeadCriteria.RelationClass.functionWord = 4

inductive DepGrammar.HeadCriteria.HeadednessAnalysis : Type

Two competing analyses of function words.

Function-head: auxiliaries, determiners, prepositions are heads.

• Most traditional DG frameworks (@cite{hudson-1990}, MTT, FGD)
• Function words satisfy criteria 3 (obligatory) and 5 (govern form)

Content-head: content words are heads, function words are dependents.

• Universal Dependencies
• Content words satisfy criteria 1 (determine category) and 2 (determine semantics)
• Better for crosslinguistic parallelism

• functionHead : HeadednessAnalysis
• contentHead : HeadednessAnalysis

instance DepGrammar.HeadCriteria.instReprHeadednessAnalysis : Repr HeadednessAnalysis

Equations

• DepGrammar.HeadCriteria.instReprHeadednessAnalysis = { reprPrec := DepGrammar.HeadCriteria.instReprHeadednessAnalysis.repr }

def DepGrammar.HeadCriteria.instReprHeadednessAnalysis.repr : HeadednessAnalysis → ℕ → Std.Format

Equations

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

instance DepGrammar.HeadCriteria.instDecidableEqHeadednessAnalysis : DecidableEq HeadednessAnalysis

Equations

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

structure DepGrammar.HeadCriteria.HeadednessEvidence : Type

Which criteria favor each analysis for a verb group like "will chase"?

Function-head (aux "will" is head):

• Criterion 3: "will" is obligatory for tense marking
• Criterion 5: "will" determines subject-verb agreement
• Criterion 6: "will" determines word order

Content-head (verb "chase" is head):

• Criterion 1: "chase" determines the VP category
• Criterion 2: "chase" determines the semantic predicate
• Criterion 4: "chase" selects its arguments

• relation : UD.DepRel
• functionHeadCriteria : List String
• contentHeadCriteria : List String

def DepGrammar.HeadCriteria.instReprHeadednessEvidence.repr : HeadednessEvidence → ℕ → Std.Format

Equations

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

instance DepGrammar.HeadCriteria.instReprHeadednessEvidence : Repr HeadednessEvidence

Equations

• DepGrammar.HeadCriteria.instReprHeadednessEvidence = { reprPrec := DepGrammar.HeadCriteria.instReprHeadednessEvidence.repr }

def DepGrammar.HeadCriteria.auxHeadednessEvidence : HeadednessEvidence

Evidence for the auxiliary relation

Equations

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

def DepGrammar.HeadCriteria.detHeadednessEvidence : HeadednessEvidence

Evidence for the determiner relation

Equations

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

theorem DepGrammar.HeadCriteria.content_head_more_criteria_for_det : detHeadednessEvidence.contentHeadCriteria.length > detHeadednessEvidence.functionHeadCriteria.length

UD's choice: content words as heads maximizes crosslinguistic parallelism because function words vary across languages while content structure is stable.

def DepGrammar.HeadCriteria.subjectVerbCriteria (argStr : ArgStr) : List HeadCriterion

A subject-verb dependency satisfies all six criteria.

Equations

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

theorem DepGrammar.HeadCriteria.nsubj_is_core_argument : classifyRelation UD.DepRel.nsubj = RelationClass.coreArgument

Subject-verb is a prototypical head-dependent relation: the verb (head) determines category, selects the subject, governs agreement, and specifies position.

theorem DepGrammar.HeadCriteria.obj_is_core_argument : classifyRelation UD.DepRel.obj = RelationClass.coreArgument

theorem DepGrammar.HeadCriteria.det_is_function_word : classifyRelation UD.DepRel.det = RelationClass.functionWord

theorem DepGrammar.HeadCriteria.aux_is_function_word : classifyRelation UD.DepRel.aux = RelationClass.functionWord

theorem DepGrammar.HeadCriteria.core_args_most_criteria : expectedCriteriaCount RelationClass.coreArgument > expectedCriteriaCount RelationClass.modifier ∧ expectedCriteriaCount RelationClass.coreArgument > expectedCriteriaCount RelationClass.functionWord

Core arguments are expected to satisfy the most criteria.