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 (Linglib/Typology/Gender.lean and Phenomena/Gender/Studies/Corbett1991.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
• verb : 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 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instInhabitedAgreementTarget : Inhabited AgreementTarget

Equations

• Core.instInhabitedAgreementTarget = { default := Core.instInhabitedAgreementTarget.default }

def Core.instInhabitedAgreementTarget.default : AgreementTarget

Equations

• Core.instInhabitedAgreementTarget.default = Core.AgreementTarget.attributive

def Core.AgreementTarget.rank : AgreementTarget → ℕ

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.verb.rank = 0

@[implicit_reducible]

instance Core.instLinearOrderAgreementTarget : LinearOrder AgreementTarget

The Agreement Hierarchy is a LinearOrder lifted from the rank. Provides ≤, <, min, max, Finset.sort, etc. for free.

Equations

• Core.instLinearOrderAgreementTarget = LinearOrder.lift' Core.AgreementTarget.rank Core.instLinearOrderAgreementTarget._proof_1

theorem Core.AgreementTarget.rank_injective : Function.Injective rank

The hierarchy rank is injective — derivable from the LinearOrder instance, restated here as a named lemma for direct invocation.

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 .verb 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 ⋯

def Core.instReprPredicateTarget.repr : PredicateTarget → ℕ → 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✝

@[implicit_reducible]

instance Core.instReprPredicateTarget : Repr PredicateTarget

Equations

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

def Core.instInhabitedPredicateTarget.default : PredicateTarget

Equations

• Core.instInhabitedPredicateTarget.default = Core.PredicateTarget.verb

@[implicit_reducible]

instance Core.instInhabitedPredicateTarget : Inhabited PredicateTarget

Equations

• Core.instInhabitedPredicateTarget = { default := Core.instInhabitedPredicateTarget.default }

def Core.PredicateTarget.rank : PredicateTarget → ℕ

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

@[implicit_reducible]

instance Core.instLinearOrderPredicateTarget : LinearOrder PredicateTarget

The Predicate Hierarchy is a LinearOrder lifted from the rank.

Equations

• Core.instLinearOrderPredicateTarget = LinearOrder.lift' Core.PredicateTarget.rank Core.instLinearOrderPredicateTarget._proof_1

theorem Core.PredicateTarget.rank_injective : Function.Injective rank

The Predicate Hierarchy rank is injective.

def Core.PredicateTarget.toAgreementTarget : PredicateTarget → AgreementTarget

Map a PredicateTarget to the corresponding AgreementTarget. Verb maps to .verb; participle/adjective/noun all map to .predicate. Many-to-one, monotone (preserves the ≤ order once you account for rank collapsing inside .predicate).

Equations

• Core.PredicateTarget.verb.toAgreementTarget = Core.AgreementTarget.verb
• 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 → ℕ → 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 }

@[implicit_reducible]

instance Core.instInhabitedAgreementType : Inhabited AgreementType

Equations

• Core.instInhabitedAgreementType = { default := Core.instInhabitedAgreementType.default }

def Core.instInhabitedAgreementType.default : AgreementType

Equations

• Core.instInhabitedAgreementType.default = Core.AgreementType.grammatical

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 → ℕ → 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 }

@[implicit_reducible]

instance Core.instInhabitedAgreementDirection : Inhabited AgreementDirection

Equations

• Core.instInhabitedAgreementDirection = { default := Core.instInhabitedAgreementDirection.default }

def Core.instInhabitedAgreementDirection.default : AgreementDirection

Equations

• Core.instInhabitedAgreementDirection.default = Core.AgreementDirection.headDriven