Agreement Target Hierarchy @cite{corbett-1991}

The Agreement Hierarchy (@cite{corbett-1991}) ranks morphosyntactic targets by likelihood of showing agreement: attributive adjectives are most likely, verbs least likely. If a language shows gender/number agreement on a lower target, it shows agreement on all higher targets.

This type is shared by gender typology (Phenomena/Gender/Typology.lean) and number agreement (Phenomena/Agreement/Studies/Corbett2000.lean).

inductive Core.AgreementTarget : Type

Morphosyntactic targets where agreement can surface, ordered by the Agreement Hierarchy (@cite{corbett-1991}).

Higher rank = more likely to show agreement (closer to controller). Lower rank = less likely (further from controller, more semantic).

• attributive : AgreementTarget
• predicate : AgreementTarget
• relativePronoun : AgreementTarget
• personalPronoun : AgreementTarget
• verbTarget : AgreementTarget

@[implicit_reducible]

instance Core.instDecidableEqAgreementTarget : DecidableEq AgreementTarget

Equations

• Core.instDecidableEqAgreementTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprAgreementTarget : Repr AgreementTarget

Equations

• Core.instReprAgreementTarget = { reprPrec := Core.instReprAgreementTarget.repr }

def Core.instReprAgreementTarget.repr : AgreementTarget → Nat → Std.Format

Equations

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

def Core.AgreementTarget.rank : AgreementTarget → Nat

Numeric rank in the Agreement Hierarchy: higher = more likely to show agreement (more syntactic); lower = less likely (more semantic).

Equations

• Core.AgreementTarget.attributive.rank = 4
• Core.AgreementTarget.predicate.rank = 3
• Core.AgreementTarget.relativePronoun.rank = 2
• Core.AgreementTarget.personalPronoun.rank = 1
• Core.AgreementTarget.verbTarget.rank = 0

theorem Core.agreement_rank_injective (a b : AgreementTarget) (h : a.rank = b.rank) : a = b

The hierarchy rank is injective — no two positions share a rank. This guarantees the Agreement Hierarchy is a total (not just partial) order: for any two targets, one strictly outranks the other.

inductive Core.PredicateTarget : Type

The Predicate Hierarchy (@cite{corbett-2000}) decomposes the predicate position on the Agreement Hierarchy into a sub-hierarchy: verb < participle < adjective < noun.

Semantic agreement increases monotonically along this sub-hierarchy: if semantic agreement is possible on a verb, it is possible on a participle; if on a participle, then on an adjective; etc.

This is orthogonal to AgreementTarget, which treats .predicate and .verbTarget as two positions on the main hierarchy. The Predicate Hierarchy provides finer resolution within the predicate position.

• verb : PredicateTarget
• participle : PredicateTarget
• adjective : PredicateTarget
• noun : PredicateTarget

@[implicit_reducible]

instance Core.instDecidableEqPredicateTarget : DecidableEq PredicateTarget

Equations

• Core.instDecidableEqPredicateTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprPredicateTarget : Repr PredicateTarget

Equations

• Core.instReprPredicateTarget = { reprPrec := Core.instReprPredicateTarget.repr }

def Core.instReprPredicateTarget.repr : PredicateTarget → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.instReprPredicateTarget.repr Core.PredicateTarget.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.PredicateTarget.verb")).group prec✝
• Core.instReprPredicateTarget.repr Core.PredicateTarget.noun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.PredicateTarget.noun")).group prec✝

def Core.PredicateTarget.rank : PredicateTarget → Nat

Rank in the Predicate Hierarchy: higher = more likely to show semantic agreement. verb (0) < participle (1) < adjective (2) < noun (3).

Equations

• Core.PredicateTarget.verb.rank = 0
• Core.PredicateTarget.participle.rank = 1
• Core.PredicateTarget.adjective.rank = 2
• Core.PredicateTarget.noun.rank = 3

theorem Core.predicate_rank_injective (a b : PredicateTarget) (h : a.rank = b.rank) : a = b

The Predicate Hierarchy rank is injective — a total order on predicate positions. Semantic agreement increases monotonically along the hierarchy.

def Core.PredicateTarget.toAgreementTarget : PredicateTarget → AgreementTarget

Map a PredicateTarget to the corresponding AgreementTarget. The predicate sub-positions map to either .predicate or .verbTarget.

Equations

• Core.PredicateTarget.verb.toAgreementTarget = Core.AgreementTarget.verbTarget
• Core.PredicateTarget.participle.toAgreementTarget = Core.AgreementTarget.predicate
• Core.PredicateTarget.adjective.toAgreementTarget = Core.AgreementTarget.predicate
• Core.PredicateTarget.noun.toAgreementTarget = Core.AgreementTarget.predicate

inductive Core.AgreementType : Type

Whether agreement markers have referential autonomy. @cite{bickel-nichols-2001}

• grammatical: pure agreement — the marker cannot stand alone as an argument; an independent NP is required (English she walk-s, the -s cannot replace she)
• pronominal: cross-referencing — the marker can function as the sole expression of the argument; an independent NP is optional (Swahili a-li-ki-soma (kitabu) — the prefixes suffice without the noun)

This distinction is orthogonal to the Agreement Hierarchy: a language can have pronominal agreement on verbs but grammatical agreement on adjectives, or vice versa.

• grammatical : AgreementType
• pronominal : AgreementType

@[implicit_reducible]

instance Core.instDecidableEqAgreementType : DecidableEq AgreementType

Equations

• Core.instDecidableEqAgreementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instReprAgreementType.repr : AgreementType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprAgreementType : Repr AgreementType

Equations

• Core.instReprAgreementType = { reprPrec := Core.instReprAgreementType.repr }

inductive Core.AgreementDirection : Type

Direction of agreement: which element originates ("drives") the features. @cite{bickel-nichols-2001} §9

• headDriven: the phrasal head provides features that percolate to its dependents — dependents carry the agreement morphology. (German/Watam NP concord: noun's gender/number → adjective, det; = dependent marking in the sense of §3.)
• dependentDriven: a dependent provides features that the head matches — the head carries the agreement morphology. (Belhare/Swahili verb agreement: subject's person/number → verb; = head marking in the sense of §3.)

Related to but distinct from Core.Morphology.LocusOfMarking: locus is a language-level WALS typological parameter classifying where all grammatical relations are marked (head, dependent, double, zero). AgreementDirection is phenomenon-specific — a language can be overall head-marking (LocusOfMarking.headMarking) yet have specific head-driven agreement (e.g., NP concord in an otherwise head-marking language).

• headDriven : AgreementDirection
• dependentDriven : AgreementDirection

@[implicit_reducible]

instance Core.instDecidableEqAgreementDirection : DecidableEq AgreementDirection

Equations

• Core.instDecidableEqAgreementDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instReprAgreementDirection.repr : AgreementDirection → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprAgreementDirection : Repr AgreementDirection

Equations

• Core.instReprAgreementDirection = { reprPrec := Core.instReprAgreementDirection.repr }