Agreement Target Hierarchy [Cor79]

The Agreement Hierarchy ([Cor79]; [Cor91] ch. 8) has four positions — attributive > predicate > relative pronoun > personal pronoun — along which the likelihood of semantic (rather than syntactic) agreement increases monotonically from left to right.

The AgreementTarget enum below additionally carries a verb target for languages with verbal gender/number agreement. verb is a linglib refinement, not a fifth position of Corbett's hierarchy, and its placement is theory-laden: it is ranked below personal pronoun (the semantic end), following [WZ00]'s classification of verbal agreement as INDEX-reading (see WechslerZlatic2000.indexReaders_lowerSet, which depends on this placement). Corbett instead subsumes verbal agreement under the predicate position, where his Predicate Hierarchy ([Com75]) makes the finite verb the most-syntactic sub-position — the opposite end. That view is formalized separately as PredicateTarget below; the two codings are a genuine cross-framework disagreement, kept visible rather than merged. Theorems about the four-position hierarchy proper should quantify over the four canonical positions only (as Corbett2000.hierarchyPositions does).

This type is shared by gender typology (Studies/Corbett1991.lean) and number agreement (Studies/Corbett2000.lean).

inductive Agreement.AgreementTarget : Type

Morphosyntactic targets where agreement can surface, ranked by the Agreement Hierarchy ([Cor79]). verb is a linglib refinement placed at the semantic end per [WZ00] — NOT a position of Corbett's hierarchy; see the module docstring for the competing Corbett/Comrie placement (PredicateTarget).

Higher rank = closer to the controller, agreement more syntactic. Lower rank = further from the controller, agreement more semantic.

• attributive : AgreementTarget
• predicate : AgreementTarget
• relativePronoun : AgreementTarget
• personalPronoun : AgreementTarget
• verb : AgreementTarget

@[implicit_reducible]

instance Agreement.instDecidableEqAgreementTarget : DecidableEq AgreementTarget

Equations

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

@[implicit_reducible]

instance Agreement.instReprAgreementTarget : Repr AgreementTarget

Equations

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

def Agreement.instReprAgreementTarget.repr : AgreementTarget → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instInhabitedAgreementTarget : Inhabited AgreementTarget

Equations

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

@[implicit_reducible]

instance Agreement.instFintypeAgreementTarget : Fintype AgreementTarget

Equations

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

def Agreement.AgreementTarget.rank : AgreementTarget → ℕ

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

Equations

• Agreement.AgreementTarget.attributive.rank = 4
• Agreement.AgreementTarget.predicate.rank = 3
• Agreement.AgreementTarget.relativePronoun.rank = 2
• Agreement.AgreementTarget.personalPronoun.rank = 1
• Agreement.AgreementTarget.verb.rank = 0

@[implicit_reducible]

instance Agreement.instLinearOrderAgreementTarget : LinearOrder AgreementTarget

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

Equations

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

theorem Agreement.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 Agreement.PredicateTarget : Type

The Predicate Hierarchy ([Com75], systematised by [Cor00]) 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 Agreement.instDecidableEqPredicateTarget : DecidableEq PredicateTarget

Equations

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

def Agreement.instReprPredicateTarget.repr : PredicateTarget → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instReprPredicateTarget : Repr PredicateTarget

Equations

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

@[implicit_reducible]

instance Agreement.instInhabitedPredicateTarget : Inhabited PredicateTarget

Equations

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

def Agreement.PredicateTarget.rank : PredicateTarget → ℕ

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

Equations

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

@[implicit_reducible]

instance Agreement.instLinearOrderPredicateTarget : LinearOrder PredicateTarget

The Predicate Hierarchy is a LinearOrder lifted from the rank.

Equations

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

theorem Agreement.PredicateTarget.rank_injective : Function.Injective rank

The Predicate Hierarchy rank is injective.

def Agreement.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

• Agreement.PredicateTarget.verb.toAgreementTarget = Agreement.AgreementTarget.verb
• Agreement.PredicateTarget.participle.toAgreementTarget = Agreement.AgreementTarget.predicate
• Agreement.PredicateTarget.adjective.toAgreementTarget = Agreement.AgreementTarget.predicate
• Agreement.PredicateTarget.noun.toAgreementTarget = Agreement.AgreementTarget.predicate

inductive Agreement.AgreementType : Type

Whether agreement markers have referential autonomy. [BN07]

• 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 Agreement.instDecidableEqAgreementType : DecidableEq AgreementType

Equations

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

def Agreement.instReprAgreementType.repr : AgreementType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instReprAgreementType : Repr AgreementType

Equations

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

@[implicit_reducible]

instance Agreement.instInhabitedAgreementType : Inhabited AgreementType

Equations

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

inductive Agreement.AgreementDirection : Type

Direction of agreement: which element originates ("drives") the features. [BN07] §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 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 Agreement.instDecidableEqAgreementDirection : DecidableEq AgreementDirection

Equations

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

@[implicit_reducible]

instance Agreement.instReprAgreementDirection : Repr AgreementDirection

Equations

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

def Agreement.instReprAgreementDirection.repr : AgreementDirection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instInhabitedAgreementDirection : Inhabited AgreementDirection

Equations

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