The Agreement Hierarchy

This file defines the four positions of Corbett's Agreement Hierarchy, the attributive modifier, the predicate, the relative pronoun and the personal pronoun, as a chain with the attributive on top; the availability of semantic agreement at a position; the hybrid nouns whose availability varies from position to position; and what it is for a map along a hierarchy to respect it.

A target agrees syntactically when its form follows the feature value the controller is assigned, and semantically when it follows the controller's meaning. A hybrid noun, such as Russian vrač 'doctor' denoting a woman or British English committee, admits both at some positions, and the Agreement Hierarchy predicts that the likelihood of semantic agreement never decreases from the attributive towards the personal pronoun, so a map respects the hierarchy when it is antitone on the positions where it is recorded. A finite verb agrees at the predicate position; Comrie's Predicate Hierarchy, which grades the verb, participle, adjective and noun within the predicate, is Corbett2000.PredicateTarget.

Main definitions

• Agreement.Position: the four positions, a chain lifted along Position.rank.
• Agreement.Kind: syntactic or semantic agreement.
• Agreement.Availability: the five degrees of availability of semantic agreement, from syntactic only to semantic only, linearly ordered.
• Agreement.RespectsHierarchy: a map recorded at some positions of a hierarchy is antitone where it is recorded.
• Agreement.Hybrid: a hybrid noun, the availability of semantic agreement at the positions of a hierarchy for which there are data.

Implementation notes

RespectsHierarchy takes any preorder of positions and any preorder of values, so that it serves the Agreement Hierarchy on Position, the Predicate Hierarchy on the sub-positions of the predicate, and refinements of the attributive position alike, and corpus proportions of semantic agreement as well as availabilities. A position carrying no value is skipped: values are compared only across comparable positions that both carry one.

References

• [Cor79] — the Agreement Hierarchy
• [Cor83a] — hierarchies, targets and controllers
• [Cor91] — the hierarchy applied to gender, chapter 8
• [Cor06] — the standard monograph on agreement

inductive Agreement.Position : Type

A position of the Agreement Hierarchy ([Cor79]).

• attributive : Position

  The attributive modifier (French un bon livre).

• predicate : Position

  The predicate, a finite verb or a predicate adjective (Russian kniga interesna).

• relativePronoun : Position

  The relative pronoun (German der die das).

• personalPronoun : Position

  The personal pronoun (English he she it).

@[instance_reducible]

instance Agreement.instDecidableEqPosition : DecidableEq Position

Equations

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

@[instance_reducible]

instance Agreement.instReprPosition : Repr Position

Equations

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

def Agreement.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Agreement.instInhabitedPosition : Inhabited Position

Equations

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

@[instance_reducible]

instance Agreement.instFintypePosition : Fintype Position

Equations

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

def Agreement.Position.rank : Position → ℕ

The place of a position in the chain, the attributive highest.

Equations

• Agreement.Position.attributive.rank = 3
• Agreement.Position.predicate.rank = 2
• Agreement.Position.relativePronoun.rank = 1
• Agreement.Position.personalPronoun.rank = 0

theorem Agreement.Position.rank_injective : Function.Injective rank

@[instance_reducible]

instance Agreement.Position.instLinearOrder : LinearOrder Position

The Agreement Hierarchy as a chain: personalPronoun < relativePronoun < predicate < attributive.

Equations

• Agreement.Position.instLinearOrder = LinearOrder.lift' Agreement.Position.rank Agreement.Position.rank_injective

inductive Agreement.Kind : Type

Whether an agreement form follows the feature value the controller is assigned or the controller's meaning.

• syntactic : Kind
• semantic : Kind

@[instance_reducible]

instance Agreement.instDecidableEqKind : DecidableEq Kind

Equations

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

def Agreement.instReprKind.repr : Kind → ℕ → Std.Format

Equations

• Agreement.instReprKind.repr Agreement.Kind.syntactic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Kind.syntactic")).group prec✝
• Agreement.instReprKind.repr Agreement.Kind.semantic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Kind.semantic")).group prec✝

@[instance_reducible]

instance Agreement.instReprKind : Repr Kind

Equations

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

@[instance_reducible]

instance Agreement.instFintypeKind : Fintype Kind

Equations

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

inductive Agreement.Availability : Type

The availability of semantic agreement at a position of a hierarchy, the five categories of [Cor91]'s summary of hybrid nouns, ordered by the likelihood of semantic agreement.

• syntacticOnly : Availability
• mostlySyntactic : Availability
• both : Availability
• mostlySemantic : Availability
• semanticOnly : Availability

@[instance_reducible]

instance Agreement.instDecidableEqAvailability : DecidableEq Availability

Equations

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

def Agreement.instReprAvailability.repr : Availability → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Agreement.instReprAvailability : Repr Availability

Equations

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

@[instance_reducible]

instance Agreement.instFintypeAvailability : Fintype Availability

Equations

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

def Agreement.Availability.rank : Availability → ℕ

The rank of an availability in the order of likelihood of semantic agreement.

Equations

• Agreement.Availability.syntacticOnly.rank = 0
• Agreement.Availability.mostlySyntactic.rank = 1
• Agreement.Availability.both.rank = 2
• Agreement.Availability.mostlySemantic.rank = 3
• Agreement.Availability.semanticOnly.rank = 4

theorem Agreement.Availability.rank_injective : Function.Injective rank

@[instance_reducible]

instance Agreement.Availability.instLinearOrder : LinearOrder Availability

Equations

• Agreement.Availability.instLinearOrder = LinearOrder.lift' Agreement.Availability.rank Agreement.Availability.rank_injective

def Agreement.Availability.Allows : Availability → Kind → Prop

Which agreement an availability admits.

Equations

• Agreement.Availability.syntacticOnly.Allows x✝ = (x✝ = Agreement.Kind.syntactic)
• Agreement.Availability.semanticOnly.Allows x✝ = (x✝ = Agreement.Kind.semantic)
• x✝¹.Allows x✝ = True

@[instance_reducible]

instance Agreement.Availability.instDecidableAllows (a : Availability) (k : Kind) : Decidable (a.Allows k)

Equations

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

def Agreement.RespectsHierarchy {ι : Type u_1} {α : Type u_2} [Preorder ι] [Preorder α] (f : ι → Option α) : Prop

A map recording a value at some positions of a hierarchy respects it when the value never decreases down the hierarchy: of two comparable positions that both carry a value, the lower carries the larger.

Equations

• Agreement.RespectsHierarchy f = ∀ ⦃i j : ι⦄, i ≤ j → ∀ a ∈ f i, ∀ b ∈ f j, b ≤ a

@[instance_reducible]

instance Agreement.instDecidableRespectsHierarchyOfFintypeOfDecidableLE {ι : Type u_1} {α : Type u_2} [Preorder ι] [Preorder α] [Fintype ι] [DecidableLE ι] [DecidableLE α] (f : ι → Option α) : Decidable (RespectsHierarchy f)

Equations

• Agreement.instDecidableRespectsHierarchyOfFintypeOfDecidableLE f = id inferInstance

theorem Agreement.respectsHierarchy_some_comp_iff_antitone {ι : Type u_1} {α : Type u_2} [Preorder ι] [Preorder α] {g : ι → α} : RespectsHierarchy (some ∘ g) ↔ Antitone g

A map recorded at every position respects the hierarchy exactly when it is antitone.

@[reducible, inline]

abbrev Agreement.Hybrid (ι : Type u_1) : Type u_1

A hybrid noun, as the availability of semantic agreement at each position of a hierarchy at which agreement in the feature applies and there are data; it respects the hierarchy when RespectsHierarchy holds of it.

Equations

• Agreement.Hybrid ι = (ι → Option Agreement.Availability)