Agreement targets

This file defines the morphosyntactic positions where agreement surfaces, ordered by Corbett's Agreement Hierarchy: attributive > predicate > relative pronoun > personal pronoun, with semantic (rather than syntactic) agreement increasingly likely from left to right.

Main declarations

• Agreement.Target: the four hierarchy positions, plus verb for languages with verbal gender/number agreement.
• Agreement.Target.hierarchyRank: position on the hierarchy (higher = more syntactic); none for verb.
• The PartialOrder instance: the four positions form a chain; verb is comparable only to itself.

Implementation notes

verb is not a position of Corbett's hierarchy, and no ranking of it is encoded. [WZ00] classify verbs with the pronouns as INDEX-readers without ranking the INDEX-readers among themselves (WechslerZlatic2000.indexReaders_lowerSet), and [Com75]'s Predicate Hierarchy grades semantic-agreement likelihood among predicate sub-positions (Corbett2000.PredicateTarget); the two classifications are orthogonal. Hence the order is partial rather than linear.

References

• [Cor79] — the Agreement Hierarchy
• [Cor91], ch. 8 — the hierarchy applied to gender
• [Cor06] — the standard monograph on agreement

inductive Agreement.Target : Type

A morphosyntactic target where agreement can surface: the four positions of the Agreement Hierarchy ([Cor79]), plus verb for verbal gender/number agreement (off the hierarchy — see the module docstring).

• attributive : Target

  Attributive adjective (e.g. French un bon livre).

• predicate : Target

  Predicate adjective/verb (e.g. Russian kniga interesna).

• relativePronoun : Target

  Relative pronoun (e.g. German der/die/das).

• personalPronoun : Target

  Personal pronoun (e.g. English he/she/it).

• verb : Target

  Verb (e.g. Hindi laRkaa aayaa vs laRkii aayii). A label only, not a fifth hierarchy position: hierarchyRank is none.

@[implicit_reducible]

instance Agreement.instDecidableEqTarget : DecidableEq Target

Equations

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

def Agreement.instReprTarget.repr : Target → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instReprTarget : Repr Target

Equations

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

@[implicit_reducible]

instance Agreement.instInhabitedTarget : Inhabited Target

Equations

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

@[implicit_reducible]

instance Agreement.instFintypeTarget : Fintype Target

Equations

• Agreement.instFintypeTarget = { elems := { val := ↑Agreement.Target.enumList, nodup := Agreement.Target.enumList_nodup }, complete := Agreement.instFintypeTarget._proof_1 }

def Agreement.Target.hierarchyRank : Target → Option ℕ

Position on the four-point Agreement Hierarchy, higher = more syntactic (more likely to show syntactic agreement); none for verb, which is off the hierarchy.

Equations

• Agreement.Target.attributive.hierarchyRank = some 3
• Agreement.Target.predicate.hierarchyRank = some 2
• Agreement.Target.relativePronoun.hierarchyRank = some 1
• Agreement.Target.personalPronoun.hierarchyRank = some 0
• Agreement.Target.verb.hierarchyRank = none

@[implicit_reducible]

instance Agreement.Target.instDecidableRelSumLe {α : Type u_1} {β : Type u_2} [LE α] [LE β] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : DecidableRel fun (x1 x2 : α ⊕ β) => x1 ≤ x2

Equations

• Agreement.Target.instDecidableRelSumLe (Sum.inl a) (Sum.inl b) = decidable_of_iff (a ≤ b) ⋯
• Agreement.Target.instDecidableRelSumLe (Sum.inl val) (Sum.inr val_1) = isFalse ⋯
• Agreement.Target.instDecidableRelSumLe (Sum.inr val) (Sum.inl val_1) = isFalse ⋯
• Agreement.Target.instDecidableRelSumLe (Sum.inr a) (Sum.inr b) = decidable_of_iff (a ≤ b) ⋯

@[implicit_reducible]

instance Agreement.Target.instPartialOrder : PartialOrder Target

The Agreement Hierarchy as a partial order, lifted along hierarchyCoord: the four canonical positions form a chain (so personalPronoun ≤ attributive); verb, off the hierarchy, is comparable only to itself.

Equations

• Agreement.Target.instPartialOrder = PartialOrder.lift Agreement.Target.hierarchyCoord✝ Agreement.Target.instPartialOrder._proof_1

@[implicit_reducible]

instance Agreement.Target.instDecidableRelLe : DecidableRel fun (x1 x2 : Target) => x1 ≤ x2

Equations

• t.instDecidableRelLe u = Agreement.Target.instDecidableRelSumLe (Agreement.Target.hierarchyCoord✝ t) (Agreement.Target.hierarchyCoord✝ u)