Corbett's morphology of agreement

Agreement is the systematic covariance of one element's form with properties of another, and it is asymmetric: the controller determines the target. Gender, number and person are the indisputable agreement features because their values originate on the controller, gender inherent to the noun, person to the pronoun, and number relating primarily to the noun; case covaries within the noun phrase too, but is imposed on noun and modifier alike by a governor outside it, and definiteness is imposed on the phrase as a whole, so neither is agreement. The exponents of agreement are affixes before, after and inside the stem, and a target may carry several for one controller; the features constrain one another, Russian distinguishing gender only in the singular in conformity with Greenberg's universal, and their joint expression may be fusional and syncretic, at its most spectacular in polarity, where the Somali article of one gender in one number is that of the other gender in the other number. The target then shapes agreement twice over. The forms available depend on its word class and even its lexical class, Upper Sorbian finite verbs and participles agreeing in different features and Latin adjective classes distinguishing three genders, two or none; and the form selected may depend on another target or on syncretism, conjoined Chichewa plurals taking the target form they share rather than the resolved one. The chapter's examples are the rows of Data/Examples/Corbett1998.json.

Implementation notes

• The asymmetry criterion is read off where a covarying feature's value originates, the chapter's classification of the five dimensions carried as data; the substrate profile records covariance in the wide sense, and what a target agrees in is the covarying dimensions whose origin is the controller.
• Polarity is defined for any exponent of two features and shown to need two-valued features, each of which it keeps fully distinct within the other; Somali's article is polar and its verbal prefix is not, the plural prefix coinciding with the masculine singular's instead.
• Number-conditioned gender distinctions are the convergent maps of Corbett's typology of gender, whose agreement classes, resolution rules and Latin carrier this file reuses; Chichewa's coordination rules are its rules over fragment nouns, one per target form before the semantic rule.
• The agreement slots of a target, their controllers and their bound of four are described in the rows and not modelled.

TODO

• Nichols's hierarchy of the three features by their propensity to be marked only by agreement, the default-or-ungrammaticality outcomes of missing morphology, and the dependence of one target's form on another in Tigre, in Somali focus constructions and in German noun phrases are prose only.
• The Chichewa nouns carry no number, so the restriction of the shared-form rule to plural conjuncts, and the triggering of gender resolution by number resolution, are not stated.
• The syncretism claims are not stated over the cell-to-exponent tables of Syntax/Agreement/Paradigm.lean, whose cells are UD-typed where the carriers here are the languages' own.

References

• G. G. Corbett, Morphology and agreement (1998)
• G. G. Corbett, Gender (1991)
• [J. H. Greenberg, Some universals of grammar (1963)][greenberg-1963]
• [G. G. Corbett, A. D. Mtenje, Gender agreement in Chichewa (1987)][corbett-mtenje-1987]

Agreement features (§§1–2)

inductive Corbett1998.Origin : Type

Where the value of a covarying feature originates: on the controller, inherent to it or relating primarily to it; on a governor outside the phrase; or on the phrase as a whole.

• controller : Origin
• governor : Origin
• phrase : Origin

@[instance_reducible]

instance Corbett1998.instDecidableEqOrigin : DecidableEq Origin

Equations

• Corbett1998.instDecidableEqOrigin x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett1998.instReprOrigin.repr : Origin → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1998.instReprOrigin : Repr Origin

Equations

• Corbett1998.instReprOrigin = { reprPrec := Corbett1998.instReprOrigin.repr }

@[instance_reducible]

instance Corbett1998.instFintypeOrigin : Fintype Origin

Equations

• Corbett1998.instFintypeOrigin = { elems := { val := ↑Corbett1998.Origin.enumList, nodup := Corbett1998.Origin.enumList_nodup }, complete := Corbett1998.instFintypeOrigin._proof_1 }

def Corbett1998.origin : Agreement.Dimension → Origin

The chapter's classification: gender is inherent to the noun and person to the pronoun, number relates primarily to the noun, case is imposed by government and definiteness on the phrase as a whole.

Equations

• Corbett1998.origin Agreement.Dimension.gender = Corbett1998.Origin.controller
• Corbett1998.origin Agreement.Dimension.number = Corbett1998.Origin.controller
• Corbett1998.origin Agreement.Dimension.person = Corbett1998.Origin.controller
• Corbett1998.origin Agreement.Dimension.case = Corbett1998.Origin.governor
• Corbett1998.origin Agreement.Dimension.definiteness = Corbett1998.Origin.phrase

@[reducible, inline]

abbrev Corbett1998.IsAgreementFeature (d : Agreement.Dimension) : Prop

Covariance is agreement when it is asymmetric: the value originates on the controller.

Equations

• Corbett1998.IsAgreementFeature d = (Corbett1998.origin d = Corbett1998.Origin.controller)

theorem Corbett1998.isAgreementFeature_iff (d : Agreement.Dimension) : IsAgreementFeature d ↔ d = Agreement.Dimension.gender ∨ d = Agreement.Dimension.number ∨ d = Agreement.Dimension.person

The three indisputable agreement features, read off the classification.

def Corbett1998.agreementFeatures (p : Agreement.Profile) (t : Agreement.Target) : Finset Agreement.Dimension

What a target agrees in: the dimensions it covaries in that are agreement features.

Equations

• Corbett1998.agreementFeatures p t = Finset.filter Corbett1998.IsAgreementFeature (p t)

theorem Corbett1998.Russian.case_mem_profile_attributive : Agreement.Dimension.case ∈ Russian.Agreement.profile Agreement.Target.attributive

Case covaries on the attributive adjective, (5).

theorem Corbett1998.Russian.not_isAgreementFeature_case : ¬IsAgreementFeature Agreement.Dimension.case

But it is imposed by government: covariance without asymmetry.

theorem Corbett1998.Russian.agreementFeatures_attributive : agreementFeatures Russian.Agreement.profile Agreement.Target.attributive = {Agreement.Dimension.number, Agreement.Dimension.gender}

The attributive adjective agrees in number and gender, (1)–(4).

The exponents of agreement (§3.1)

theorem Corbett1998.CoastalMarind.faithful_light : Function.Injective CoastalMarind.light

The infixed vowel of ak-k 'light' distinguishes all four genders, (6)–(9).

theorem Corbett1998.CoastalMarind.not_faithful_demonstrative : ¬Function.Injective CoastalMarind.demonstrative

The demonstrative does not: genders I and III share e-pe.

Constraints on the co-occurrence of features (§3.2)

theorem Corbett1998.Russian.convergent : Corbett1991.Convergent (fun (x : Russian.Gender.Value) => x.adjEnding false) fun (x : Russian.Gender.Value) => x.adjEnding true

Adjectives distinguish gender only in the singular, (1)–(4): a convergent system.

theorem Corbett1998.Russian.card_adjEnding_pl_le : Nat.card ↑(Set.range fun (x : Russian.Gender.Value) => x.adjEnding true) ≤ Nat.card ↑(Set.range fun (x : Russian.Gender.Value) => x.adjEnding false)

Greenberg's Universal 37 as its corollary.

inductive Corbett1998.Russian.Tense : Type

The tenses the verb's agreement distinguishes.

• nonpast : Tense
• past : Tense

@[instance_reducible]

instance Corbett1998.Russian.instDecidableEqTense : DecidableEq Tense

Equations

• Corbett1998.Russian.instDecidableEqTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1998.Russian.instReprTense : Repr Tense

Equations

• Corbett1998.Russian.instReprTense = { reprPrec := Corbett1998.Russian.instReprTense.repr }

def Corbett1998.Russian.instReprTense.repr : Tense → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1998.Russian.instFintypeTense : Fintype Tense

Equations

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

def Corbett1998.Russian.verbFeatures : Tense → Finset Agreement.Dimension

Verbs agree in person and number, in the past tense in gender and number.

Equations

• Corbett1998.Russian.verbFeatures Corbett1998.Russian.Tense.nonpast = {Agreement.Dimension.person, Agreement.Dimension.number}
• Corbett1998.Russian.verbFeatures Corbett1998.Russian.Tense.past = {Agreement.Dimension.gender, Agreement.Dimension.number}

theorem Corbett1998.Russian.gender_mem_verbFeatures_iff (t : Tense) : Agreement.Dimension.gender ∈ verbFeatures t ↔ t = Tense.past

Gender agreement on the verb is confined to the past tense.

theorem Corbett1998.Russian.profile_verb : Russian.Agreement.profile Agreement.Target.verb = verbFeatures Tense.nonpast ∪ verbFeatures Tense.past

The fragment's verb profile is the union over the tenses.

def Corbett1998.Polar {G : Type u_1} {N : Type u_2} {F : Type u_3} (f : G → N → F) : Prop

An exponent of two features is polar when changing either value alone changes the form and changing both leaves it unchanged.

Equations

• Corbett1998.Polar f = ∀ ⦃g g' : G⦄ ⦃n n' : N⦄, g ≠ g' → n ≠ n' → f g n = f g' n' ∧ f g n ≠ f g' n ∧ f g n ≠ f g n'

@[instance_reducible]

instance Corbett1998.instDecidablePolarOfFintypeOfDecidableEq {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} [Fintype G] [Fintype N] [DecidableEq G] [DecidableEq N] [DecidableEq F] : Decidable (Polar f)

Equations

• Corbett1998.instDecidablePolarOfFintypeOfDecidableEq = id inferInstance

theorem Corbett1998.Polar.flip {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} (h : Polar f) : Polar (_root_.flip f)

Polarity is symmetric in the two features.

theorem Corbett1998.Polar.card_le_two {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} [Fintype G] [Nontrivial N] (h : Polar f) : Fintype.card G ≤ 2

Polarity needs two-valued features: with three values of one feature, two of them would share a form.

theorem Corbett1998.Polar.card_le_two' {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} [Fintype N] [Nontrivial G] (h : Polar f) : Fintype.card N ≤ 2

The other feature likewise.

theorem Corbett1998.Polar.card_eq_two {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} [Fintype G] [Nontrivial G] [Nontrivial N] (h : Polar f) : Fintype.card G = 2

Polar features are two-valued.

theorem Corbett1998.Polar.injective {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} [Nontrivial N] (h : Polar f) (n : N) : Function.Injective fun (x : G) => f x n

Within one value of the other feature, a polar exponent keeps every distinction.

theorem Corbett1998.Polar.parallel {G : Type u_1} {N : Type u_2} {F : Type u_3} {f : G → N → F} [Nontrivial N] (h : Polar f) (n n' : N) : Corbett1991.Parallel (fun (x : G) => f x n) fun (x : G) => f x n'

Polarity is syncretism across the numbers and none within them: in Corbett's typology, a parallel system.

theorem Corbett1998.Somali.polar_article : Polar Somali.Gender.Value.article

Table 9.1: the article is polar.

theorem Corbett1998.Somali.not_polar_verbPrefix : ¬Polar Somali.Gender.Value.verbPrefix

The verbal prefix is not, (11)–(14): the plural prefix of either gender is the masculine singular's, another syncretism.

theorem Corbett1998.Somali.verbPrefix_plural (g : Somali.Gender.Value) : g.verbPrefix true = Somali.Gender.Value.masc.verbPrefix false

The plural prefix of either gender is the masculine singular's.

theorem Corbett1998.Somali.article_nin : Somali.Gender.nin.article true = Somali.Gender.nin.article false

Nor are all nouns in the polarity system: nin 'man' keeps -kii in the plural.

theorem Corbett1998.Somali.parallel_article : Corbett1991.Parallel (fun (x : Somali.Gender.Value) => x.article false) fun (x : Somali.Gender.Value) => x.article true

In the typology of gender the article is a parallel system and the verb a convergent one.

theorem Corbett1998.Somali.convergent_verbPrefix : Corbett1991.Convergent (fun (x : Somali.Gender.Value) => x.verbPrefix false) fun (x : Somali.Gender.Value) => x.verbPrefix true

The verbal prefix converges on one plural form.

The effect of the target on the forms available (§4)

inductive Corbett1998.UpperSorbian.Item : Type

The two verbal targets of (17).

• finiteVerb : Item
• participle : Item

@[instance_reducible]

instance Corbett1998.UpperSorbian.instDecidableEqItem : DecidableEq Item

Equations

• Corbett1998.UpperSorbian.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1998.UpperSorbian.instReprItem : Repr Item

Equations

• Corbett1998.UpperSorbian.instReprItem = { reprPrec := Corbett1998.UpperSorbian.instReprItem.repr }

def Corbett1998.UpperSorbian.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1998.UpperSorbian.instFintypeItem : Fintype Item

Equations

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

def Corbett1998.UpperSorbian.Item.key : Item → String

The row key of each target.

Equations

• Corbett1998.UpperSorbian.Item.finiteVerb.key = "finiteVerb"
• Corbett1998.UpperSorbian.Item.participle.key = "participle"

def Corbett1998.UpperSorbian.features : Item → Finset Agreement.Dimension

The finite verb agrees in number and person, the participle in number and gender.

Equations

• Corbett1998.UpperSorbian.features Corbett1998.UpperSorbian.Item.finiteVerb = {Agreement.Dimension.number, Agreement.Dimension.person}
• Corbett1998.UpperSorbian.features Corbett1998.UpperSorbian.Item.participle = {Agreement.Dimension.number, Agreement.Dimension.gender}

theorem Corbett1998.UpperSorbian.not_uniform : ¬∃ (D : Finset Agreement.Dimension), ∀ (i : Item), features i = D

Agreement features cannot be stated at the level of the language.

theorem Corbett1998.Latin.facilis_factorsThrough_acer : Function.FactorsThrough Latin.Gender.facilis.nomSg Latin.Gender.acer.nomSg ∧ ¬Function.FactorsThrough Latin.Gender.acer.nomSg Latin.Gender.facilis.nomSg

Table 9.2: facilis distinguishes only part of what acer does, and felix nothing of what facilis does: each class's forms factor through the previous, never conversely.

theorem Corbett1998.Latin.felix_factorsThrough_facilis : Function.FactorsThrough Latin.Gender.felix.nomSg Latin.Gender.facilis.nomSg ∧ ¬Function.FactorsThrough Latin.Gender.facilis.nomSg Latin.Gender.felix.nomSg

And felix distinguishes nothing of what facilis does.

The effect of the target on the form selected (§5)

def Corbett1998.Chichewa.sharedFormRules : List (Corbett1991.Rule Chichewa.Gender.Noun Chichewa.Gender.SubjPrefix)

Coordinated plural nouns that would take one target form take it.

Equations

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

def Corbett1998.Chichewa.semanticRules : List (Corbett1991.Rule Chichewa.Gender.Noun Chichewa.Gender.SubjPrefix)

The regular rule: humans take the plural of gender 1/2 and the rest the plural of 7/8.

Equations

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

def Corbett1998.Chichewa.rules : List (Corbett1991.Rule Chichewa.Gender.Noun Chichewa.Gender.SubjPrefix)

The shared form is preferred; the regular rule applies where there is none.

Equations

• Corbett1998.Chichewa.rules = Corbett1998.Chichewa.sharedFormRules ++ Corbett1998.Chichewa.semanticRules

theorem Corbett1998.Chichewa.resolve_of_shared {cs : List Chichewa.Gender.Noun} (hne : cs ≠ []) {f : Chichewa.Gender.SubjPrefix} (h : ∀ c ∈ cs, c.gender.plSubjPrefix = f) : Corbett1991.resolve rules cs = some f

Syncretism licenses agreement, (18) and (19): conjuncts sharing a form take it.

theorem Corbett1998.Chichewa.resolve_of_ne {cs : List Chichewa.Gender.Noun} (ha : ∃ c ∈ cs, c.gender.plSubjPrefix ≠ Chichewa.Gender.SubjPrefix.a) (hz : ∃ c ∈ cs, c.gender.plSubjPrefix ≠ Chichewa.Gender.SubjPrefix.zi) : Corbett1991.resolve rules cs = Corbett1991.resolve semanticRules cs

Were the forms not syncretic, the regular rule would apply.

theorem Corbett1998.Chichewa.resolve_semanticRules (cs : List Chichewa.Gender.Noun) : Corbett1991.resolve semanticRules cs = some (if ∀ c ∈ cs, c.human = true then Chichewa.Gender.SubjPrefix.a else Chichewa.Gender.SubjPrefix.zi)

The regular rule on its own: gender 1/2 for humans, 7/8 for the rest.

theorem Corbett1998.Chichewa.resolve_mphaka_galu_ana_lalanje : Corbett1991.resolve rules [Chichewa.Gender.mphaka, Chichewa.Gender.galu] = some Chichewa.Gender.SubjPrefix.a ∧ Corbett1991.resolve rules [Chichewa.Gender.ana, Chichewa.Gender.lalanje] = some Chichewa.Gender.SubjPrefix.a

Corbett's Gender adds the cats and dogs, and the children and oranges, humans and not, both by the shared form.

The chapter's examples

theorem Corbett1998.russian_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "russ1263" → ∀ g ∈ row.parse? "gender" [("masc", Russian.Gender.Value.masc), ("fem", Russian.Gender.Value.fem), ("neut", Russian.Gender.Value.neut)], ∀ pl ∈ row.parse? "number" [("sg", false), ("pl", true)], ∀ e ∈ row.parse? "ending" [("yj", Russian.Gender.AdjEnding.yj), ("aja", Russian.Gender.AdjEnding.aja), ("oe", Russian.Gender.AdjEnding.oe), ("ye", Russian.Gender.AdjEnding.ye)], e = g.adjEnding pl

Russian adjectives, (1)–(4): the ending is the fragment's by gender and number.

theorem Corbett1998.marind_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "nucl1622" → ∀ g ∈ row.parse? "gender" [("I", CoastalMarind.Gender.gI), ("II", CoastalMarind.Gender.gII), ("III", CoastalMarind.Gender.gIII), ("IV", CoastalMarind.Gender.gIV)], (∀ a ∈ row.feature? "adjective", a = CoastalMarind.light g) ∧ ∀ d ∈ row.feature? "demonstrative", d = CoastalMarind.demonstrative g

Marind, (6)–(9): the adjective and the demonstrative are the fragment's by gender.

theorem Corbett1998.upperSorbian_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "uppe1395" → ∀ (i : UpperSorbian.Item), ∀ D ∈ row.parse? i.key [("number,person", {Agreement.Dimension.number, Agreement.Dimension.person}), ("number,gender", {Agreement.Dimension.number, Agreement.Dimension.gender})], UpperSorbian.features i = D

Upper Sorbian, (17): each target agrees in the features the row records for it.

theorem Corbett1998.somali_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "soma1255" → ∀ n ∈ row.parse? "noun" (List.map (fun (n : Somali.Gender.Noun) => (n.form, n)) Somali.Gender.allNouns), ∀ pl ∈ row.parse? "number" [("sg", false), ("pl", true)], (∀ a ∈ row.parse? "article" [("kii", Somali.Gender.Article.kii), ("tii", Somali.Gender.Article.tii)], a = n.article pl) ∧ ∀ v ∈ row.parse? "verb" [("y", Somali.Gender.VerbPrefix.y), ("t", Somali.Gender.VerbPrefix.t)], v = n.gender.verbPrefix pl

Somali, (11)–(14) and nin: the article is the noun's by number and the verbal prefix the gender's.

theorem Corbett1998.chichewa_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "nyan1308" → ∀ a ∈ row.parse? "conjunct1" (List.map (fun (n : Chichewa.Gender.Noun) => (n.form, n)) Chichewa.Gender.allNouns), ∀ b ∈ row.parse? "conjunct2" (List.map (fun (n : Chichewa.Gender.Noun) => (n.form, n)) Chichewa.Gender.allNouns), ∀ p ∈ row.parse? "prefix" [("a", Chichewa.Gender.SubjPrefix.a), ("zi", Chichewa.Gender.SubjPrefix.zi)], Corbett1991.resolve Chichewa.rules [a, b] = some p

Chichewa, (18) and (19): the verb's prefix is the rules' resolution of the conjuncts.