Corbett (1991): Gender

The book's typology of gender. Gender is a property of nouns shown only in agreement, and a language's genders are the classes of nouns that take the same agreements. Nouns are assigned to them by rules reading their meaning or their form: the semantic rules take precedence, the formal rules, morphological or phonological, sort the semantic residue, and no system is formal alone (Gender.AssignmentSystem). Tamil, Russian, Swahili, Afar and Hausa instantiate the schema on their fragments, and the assignment systems of chapters 2 and 3 are surveyed by kind and by the semantic criteria their rules use (survey).

Counting the genders starts from agreement classes, the sets of nouns taking identical agreements in every form on every target, distinguishes the controller genders into which nouns fall from the target genders marked on agreeing elements, and reads Greenberg's universal that the plural never distinguishes more genders than the singular off the map between the two numbers' target genders, parallel, convergent or crossed, exhibited here for French, German, Tamil, Romanian, Lak and Slovene. Nouns whose meaning and form conflict may be hybrid, taking semantic agreement on some targets and syntactic agreement on others, and the hybrids of the book's summary table respect the Agreement Hierarchy (hybrids_respectHierarchy); the Bantu data of §8.3 divide the attributive position into the possessive and the other modifiers (FinePosition), and the corpus proportions of feminine agreement with Russian vrač respect the hierarchy too.

Conjoined controllers are resolved by ordered rules of two shapes, one conjunct of a kind or all conjuncts of a kind, reading the conjuncts' person, meaning or gender; the rules of person, of number and of gender are stated for Czech, Tamil, Archi, Luganda, French, Slovene, Icelandic, Latin, Polish, Romanian, Serbo-Croat and Ojibwa, and a language's resolution is never less semantic than its assignment. The judgments the book reports are the rows of Data/Examples/Corbett1991.json.

Implementation notes

• The assignment systems are the substrate's, typed by the meaning their semantic rules read and the form their formal rules read; the fragments' natural-gender flag stands in for the referent's sex. Corbett's irregular third declension of Russian is the study's refinement of the fragment's declension classes.
• Agreement classes, target genders and the map between two numbers' target genders are the substrate's Gender.agreementClasses, Gender.targetGenders and Gender.Parallel, Gender.Convergent and Gender.Crossed. Subgenders, inquorate genders and consistent agreement patterns are described in the book's prose and not formalised.
• A hybrid noun is an Agreement.Hybrid, its availability profile over the positions of Agreement.Position, or over FinePosition where the book divides the attributive; it respects the hierarchy when the profile is antitone on the positions where it is recorded, and the same predicate serves the corpus proportions.
• Resolution rules are the substrate's Agreement.ResolutionRule, applied in order to a list of conjunct descriptors and returning no form when no rule applies, the book's ineffable coordinations; the descriptors are persons, genders, semantic features, or fragment nouns as each language requires. Optional rules are recorded as rows. The number rules count the conjuncts, which no resolution rule can (Slovene.numberResolve_ne_resolve), so they are stated directly and shown to be the substrate's Number.System.resolve folded over the conjuncts, except that a coordination of plurals alone resolves nothing, the book's restriction that keeps gender resolution from being triggered. The gender carriers of French, Lak, Slovene and Ojibwa are declared in the study, there being no fragments for them; the Icelandic rules read the fragment nouns' genders, and the Romanian ones the nouns.
• Not modelled: the psycholinguistic evidence of chapter 4, the morphology of agreement and its limits in chapter 5, syncretism and neutral agreement in chapter 7, the diachrony of chapters 8 to 10, Russian acronyms and indeclinables, Chichewa's target-gender rule for plural conjuncts, the Polish optional resolution rules, and the case and distance effects within a position of the hierarchy (§8.1.2), which are rows only.

TODO

• Subgenders as minimally different agreement classes, and consistent agreement patterns, want the full paradigm tables of the book's chapter 6 in the Russian fragment.
• The corpus-level reading of the hierarchy, proportions of semantic agreement per target, is recorded for vrač only.
• The generalization of §9.8, that resolution is never less semantic than assignment: a rule reads gender or meaning when its sort factors through that map (Agreement.ResolutionRule.resolve_factorsThrough), but the languages' conjuncts are not yet typed by both.

References

• G. G. Corbett, Gender (1991)
• G. G. Corbett, The agreement hierarchy (1979)
• G. G. Corbett, Hierarchies, Targets and Controllers (1983)
• A. A. Zaliznjak, K voprosu o grammatičeskix kategorijax roda i oduševlennosti (1964)
• J. H. Greenberg, Some universals of grammar (1963)
• C. F. Hockett, A Course in Modern Linguistics (1958)
• B. Heine, African noun class systems (1982)
• T. Givón, The resolution of gender conflicts in Bantu conjunction (1970)
• R. M. W. Dixon, The Dyirbal Language of North Queensland (1972)
• G. R. Tucker, W. E. Lambert, A. A. Rigault, The French Speaker's Skill with Grammatical Gender (1977)

Assignment systems

inductive Corbett1991.Criterion : Type

A semantic opposition on which gender assignment can rest (§2.3) is one of de la Grasserie's types or of the criteria the book adds. Sex is one opposition here, though the book separates systems singling out females (Diyari, Dizi) from those singling out males (Kala Lagaw Ya).

• animacy : Criterion
• rationality : Criterion
• humanness : Criterion
• sex : Criterion
• strength : Criterion
• size : Criterion
• evaluation : Criterion
• insect : Criterion
• edibility : Criterion
• liquidity : Criterion
• abstractness : Criterion
• canine : Criterion
• huntingWeapon : Criterion
• lustre : Criterion

@[instance_reducible]

instance Corbett1991.instDecidableEqCriterion : DecidableEq Criterion

Equations

• Corbett1991.instDecidableEqCriterion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.instReprCriterion : Repr Criterion

Equations

• Corbett1991.instReprCriterion = { reprPrec := Corbett1991.instReprCriterion.repr }

def Corbett1991.instReprCriterion.repr : Criterion → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.instFintypeCriterion : Fintype Criterion

Equations

• Corbett1991.instFintypeCriterion = { elems := { val := ↑Corbett1991.Criterion.enumList, nodup := Corbett1991.Criterion.enumList_nodup }, complete := Corbett1991.instFintypeCriterion._proof_1 }

inductive Corbett1991.AssignmentKind : Type

The book's typology of assignment systems.

• strictSemantic : AssignmentKind
• predominantlySemantic : AssignmentKind
• morphological : AssignmentKind
• phonological : AssignmentKind

@[instance_reducible]

instance Corbett1991.instDecidableEqAssignmentKind : DecidableEq AssignmentKind

Equations

• Corbett1991.instDecidableEqAssignmentKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.instReprAssignmentKind : Repr AssignmentKind

Equations

• Corbett1991.instReprAssignmentKind = { reprPrec := Corbett1991.instReprAssignmentKind.repr }

def Corbett1991.instReprAssignmentKind.repr : AssignmentKind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.instFintypeAssignmentKind : Fintype AssignmentKind

Equations

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

structure Corbett1991.SurveyEntry : Type

A language of chapters 2 and 3 with the kind of its assignment system and the semantic criteria its rules use, as this study reads the book's tables; the book draws up no such list itself.

• language : String

  The language, under the book's name.

• glottocode : String
• kind : AssignmentKind

  The kind of assignment system the book describes.

• criteria : List Criterion

  The semantic criteria the book's rules for the language use.

@[instance_reducible]

instance Corbett1991.instDecidableEqSurveyEntry : DecidableEq SurveyEntry

Equations

• Corbett1991.instDecidableEqSurveyEntry = Corbett1991.instDecidableEqSurveyEntry.decEq

def Corbett1991.instDecidableEqSurveyEntry.decEq (x✝ x✝¹ : SurveyEntry) : Decidable (x✝ = x✝¹)

Equations

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

def Corbett1991.instReprSurveyEntry.repr : SurveyEntry → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.instReprSurveyEntry : Repr SurveyEntry

Equations

• Corbett1991.instReprSurveyEntry = { reprPrec := Corbett1991.instReprSurveyEntry.repr }

def Corbett1991.survey : List SurveyEntry

The assignment systems of chapters 2 and 3 (Tables 2.1 to 2.8 and §3.1 to §3.2).

Equations

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

Tamil: a strict semantic system (§2.1.1)

def Corbett1991.Tamil.sem (n : Tamil.Gender.Noun) : Bool × Option Gender

The rules read rationality and the gender of the referents.

Equations

• Corbett1991.Tamil.sem n = (n.rational, n.naturalGender)

def Corbett1991.Tamil.system : Gender.AssignmentSystem (Bool × Option Gender) Unit Tamil.Gender.Value

Table 2.1 makes male rationals masculine, female rationals feminine and the residue neuter.

Equations

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

theorem Corbett1991.Tamil.isStrictSemantic_system : system.IsStrictSemantic

theorem Corbett1991.Tamil.assign_eq_gender (n : Tamil.Gender.Noun) : n ∈ Tamil.Gender.allNouns → system.assign sem (fun (x : Tamil.Gender.Noun) => ()) n = n.gender

The rules assign every noun of the fragment its gender.

Russian: a morphological system (§3.1.1)

inductive Corbett1991.Russian.Declension : Type

The declensional types of Figure 3.1 are the four paradigms and the irregular third.

• I : Declension
• II : Declension
• III : Declension
• IV : Declension
• irregularIII : Declension

@[instance_reducible]

instance Corbett1991.Russian.instDecidableEqDeclension : DecidableEq Declension

Equations

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

def Corbett1991.Russian.instReprDeclension.repr : Declension → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Russian.instReprDeclension : Repr Declension

Equations

• Corbett1991.Russian.instReprDeclension = { reprPrec := Corbett1991.Russian.instReprDeclension.repr }

@[instance_reducible]

instance Corbett1991.Russian.instFintypeDeclension : Fintype Declension

Equations

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

def Corbett1991.Russian.declension (n : Russian.Gender.Noun) : Option Declension

Corbett's typing of the fragment's declension classes puts znamja and put' in the irregular third declension.

Equations

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

def Corbett1991.Russian.sem (n : Russian.Gender.Noun) : Option Gender

The gender of the referents.

Equations

• Corbett1991.Russian.sem n = n.naturalGender

def Corbett1991.Russian.system : Gender.AssignmentSystem (Option Gender) (Option Declension) Russian.Gender.Value

The rules of §3.1.1 for declinable nouns make males masculine and females feminine, then declension I masculine, declensions II and III feminine and the rest neuter. The rules for acronyms and indeclinables (Figure 3.4) are not modelled.

Equations

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

theorem Corbett1991.Russian.assign_eq_gender (n : Russian.Gender.Noun) : n ∈ Russian.Gender.allNouns → n ≠ Russian.Gender.put' → system.assign sem declension n = n.gender

The rules assign every noun of the fragment its gender, put' excepted, which the book leaves as an isolated exception with an irregular lexical marker.

theorem Corbett1991.Russian.djadja_precedence : system.formal (declension Russian.Gender.djadja) = some Russian.Gender.Value.fem ∧ system.assign sem declension Russian.Gender.djadja = Russian.Gender.Value.masc

The morphological rule would make djadja 'uncle' feminine and the semantic rule makes it masculine; the semantic rule takes precedence.

theorem Corbett1991.Russian.vrac_by_declension : system.assign sem declension Russian.Gender.vrač = Russian.Gender.Value.masc

vrač 'doctor' as a lexeme is not sex-differentiable, so the declension decides; the conflict when it denotes a woman is the hybrid pattern of §8.1.

Swahili: morphological classes and animate concord (§3.1.2)

def Corbett1991.Swahili.sem (n : Swahili.Noun) : Option Swahili.Evaluative × Reference.Animacy

The semantic rules read evaluative derivation and animacy.

Equations

• Corbett1991.Swahili.sem n = (n.evaluative, n.animacy)

def Corbett1991.Swahili.system : Gender.AssignmentSystem (Option Swahili.Evaluative × Reference.Animacy) Swahili.Gender Swahili.Gender

The rules of §3.1.2 send augmentatives to 5/6, diminutives to 7/8 and remaining animates to 1/2, then each morphological class to its own gender, over the fragment's five genders (the book's 11/10 and 15 are not among them). The formal rule is total, so the residue gender is never reached.

Equations

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

theorem Corbett1991.Swahili.assign_eq_gender (n : Swahili.Noun) : n ∈ Swahili.allNouns → system.assign sem Swahili.Noun.morphClass n = n.gender

The rules assign every noun of the fragment its gender.

theorem Corbett1991.Swahili.genderA_semantic (n : Swahili.Noun) : n ∈ Swahili.allNouns → system.assign sem Swahili.Noun.morphClass n = Swahili.Gender.genderA → (system.semantic (sem n)).isSome = true

Gender 1/2 is purely semantic, every noun assigned to it being assigned by a semantic rule.

Afar and Hausa: phonological systems (§3.2.1, §3.2.2)

def Corbett1991.Afar.sem (n : Afar.Gender.Noun) : Option Gender

The gender of the referents.

Equations

• Corbett1991.Afar.sem n = n.naturalGender

def Corbett1991.Afar.system : Gender.AssignmentSystem (Option Gender) Bool Afar.Gender.Value

The referents' gender first; then a citation form ending in an accented vowel is feminine, the rest masculine.

Equations

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

theorem Corbett1991.Afar.assign_eq_gender (n : Afar.Gender.Noun) : n ∈ Afar.Gender.allNouns → n ≠ Afar.Gender.doonik → system.assign sem Afar.Gender.Noun.finalAccentedVowel n = n.gender

The rules assign every noun of the fragment its gender, the isolated exception doònik 'sail-boat' apart.

theorem Corbett1991.Afar.abba_precedence : system.formal Afar.Gender.abba.finalAccentedVowel = some Afar.Gender.Value.fem ∧ system.assign sem Afar.Gender.Noun.finalAccentedVowel Afar.Gender.abba = Afar.Gender.Value.masc

abbà 'father' ends in an accented vowel yet is masculine, the semantic rule taking precedence over the phonological one.

def Corbett1991.Hausa.sem (n : Hausa.Noun) : Option Gender

The gender of the referents.

Equations

• Corbett1991.Hausa.sem n = n.naturalGender

def Corbett1991.Hausa.system : Gender.AssignmentSystem (Option Gender) Bool Gender

The referents' gender first; then a noun in -ā is feminine, the rest masculine.

Equations

• Corbett1991.Hausa.system = { semantic := id, formal := fun (aa : Bool) => if aa = true then some Gender.feminine else none, residue := Gender.masculine }

theorem Corbett1991.Hausa.assign_eq_gender (n : Hausa.Noun) : n ∈ Hausa.allNouns → n ∉ [Hausa.gida, Hausa.kada] → system.assign sem (fun (n : Hausa.Noun) => decide n.EndsInAa) n = n.gender

The rules assign every noun of the fragment its gender apart from gidā 'house' and kadā̀ 'crocodile', two of the -ā masculines of [New00] that the fragment carries; the book says only that the phonological rule has exceptions.

Controller and target genders (chapter 6)

theorem Corbett1991.Romanian.crossed : Gender.Crossed (fun (x : Romanian.Gender.Value) => x.adjForm false) fun (x : Romanian.Gender.Value) => x.adjForm true

Figure 6.1 is a crossed system.

theorem Corbett1991.Romanian.card_range_adjForm : Fintype.card ↑(Set.range Romanian.Gender.Value.adjForm) = 3 ∧ Fintype.card ↑(Gender.targetGenders Romanian.Gender.Value.adjForm false) = 2 ∧ Fintype.card ↑(Gender.targetGenders Romanian.Gender.Value.adjForm true) = 2

Three controller genders over two target genders in each number.

theorem Corbett1991.Romanian.rows (row : Datum) : row ∈ Examples.all → row.language = "roma1327" → ∀ n ∈ row.parse? "noun" (List.map (fun (n : Romanian.Gender.Noun) => (n.form, n)) Romanian.Gender.allNouns), ∀ pl ∈ row.parse? "number" [("singular", false), ("plural", true)], ∀ f ∈ row.parse? "form" [("zero", Romanian.Gender.AdjForm.zero), ("ă", Romanian.Gender.AdjForm.ă), ("i", Romanian.Gender.AdjForm.i), ("e", Romanian.Gender.AdjForm.e)], row.judgment = Judgment.acceptable ↔ n.gender.adjForm pl = f

Every fragment noun takes, in each number, the form of its gender, (5) to (10).

inductive Corbett1991.French.Value : Type

The two genders have one form each in both numbers (Figure 6.6).

• masc : Value
• fem : Value

@[instance_reducible]

instance Corbett1991.French.instDecidableEqValue : DecidableEq Value

Equations

• Corbett1991.French.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett1991.French.instReprValue.repr : Value → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.French.instReprValue : Repr Value

Equations

• Corbett1991.French.instReprValue = { reprPrec := Corbett1991.French.instReprValue.repr }

@[instance_reducible]

instance Corbett1991.French.instFintypeValue : Fintype Value

Equations

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

theorem Corbett1991.French.parallel : Gender.Parallel id id

theorem Corbett1991.German.convergent : Gender.Convergent (fun (g : German.Gender.Value) => German.Determiners.definite (German.Determiners.GenderNumber.sg g) German.Case.nom) fun (x : German.Gender.Value) => German.Determiners.definite German.Determiners.GenderNumber.pl German.Case.nom

The definite article has three forms for the three genders in the nominative singular and one in the plural (Figure 6.7).

inductive Corbett1991.Lak.Value : Type

The four genders of Lak and the three sets of verbal agreement markers of Figure 6.5.

• I : Value
• II : Value
• III : Value
• IV : Value

@[instance_reducible]

instance Corbett1991.Lak.instDecidableEqValue : DecidableEq Value

Equations

• Corbett1991.Lak.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.Lak.instReprValue : Repr Value

Equations

• Corbett1991.Lak.instReprValue = { reprPrec := Corbett1991.Lak.instReprValue.repr }

def Corbett1991.Lak.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Corbett1991.Lak.instReprValue.repr Corbett1991.Lak.Value.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Corbett1991.Lak.Value.I")).group prec✝
• Corbett1991.Lak.instReprValue.repr Corbett1991.Lak.Value.II prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Corbett1991.Lak.Value.II")).group prec✝
• Corbett1991.Lak.instReprValue.repr Corbett1991.Lak.Value.III prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Corbett1991.Lak.Value.III")).group prec✝
• Corbett1991.Lak.instReprValue.repr Corbett1991.Lak.Value.IV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Corbett1991.Lak.Value.IV")).group prec✝

@[instance_reducible]

instance Corbett1991.Lak.instFintypeValue : Fintype Value

Equations

• Corbett1991.Lak.instFintypeValue = { elems := { val := ↑Corbett1991.Lak.Value.enumList, nodup := Corbett1991.Lak.Value.enumList_nodup }, complete := Corbett1991.Lak.instFintypeValue._proof_1 }

inductive Corbett1991.Lak.Marker : Type

The three sets of forms are prefixal Ø/b/d and internal or suffixal w/w/r.

• zeroW : Marker
• bW : Marker
• dR : Marker

@[instance_reducible]

instance Corbett1991.Lak.instDecidableEqMarker : DecidableEq Marker

Equations

• Corbett1991.Lak.instDecidableEqMarker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.Lak.instReprMarker : Repr Marker

Equations

• Corbett1991.Lak.instReprMarker = { reprPrec := Corbett1991.Lak.instReprMarker.repr }

def Corbett1991.Lak.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Lak.instFintypeMarker : Fintype Marker

Equations

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

def Corbett1991.Lak.Value.sgMarker : Value → Marker

The singular marker of each gender.

Equations

• Corbett1991.Lak.Value.I.sgMarker = Corbett1991.Lak.Marker.zeroW
• Corbett1991.Lak.Value.II.sgMarker = Corbett1991.Lak.Marker.dR
• Corbett1991.Lak.Value.III.sgMarker = Corbett1991.Lak.Marker.bW
• Corbett1991.Lak.Value.IV.sgMarker = Corbett1991.Lak.Marker.dR

def Corbett1991.Lak.Value.plMarker : Value → Marker

The plural marker of each gender.

Equations

• Corbett1991.Lak.Value.I.plMarker = Corbett1991.Lak.Marker.bW
• Corbett1991.Lak.Value.II.plMarker = Corbett1991.Lak.Marker.bW
• Corbett1991.Lak.Value.III.plMarker = Corbett1991.Lak.Marker.bW
• Corbett1991.Lak.Value.IV.plMarker = Corbett1991.Lak.Marker.dR

theorem Corbett1991.Lak.crossed : Gender.Crossed Value.sgMarker Value.plMarker

Figure 6.10 is a crossed system, with three target genders in the singular and two in the plural.

theorem Corbett1991.Lak.card_plMarker_le : Fintype.card ↑(Set.range Value.plMarker) ≤ Fintype.card ↑(Set.range Value.sgMarker)

Universal 37 holds though neither number determines the other.

inductive Corbett1991.Slovene.Value : Type

An agreeing predicate's endings for the three genders in the three numbers (Table 9.5) are parallel between singular and plural and convergent with the dual, where feminine and neuter share a form (Figure 6.11).

• masc : Value
• fem : Value
• neut : Value

@[instance_reducible]

instance Corbett1991.Slovene.instDecidableEqValue : DecidableEq Value

Equations

• Corbett1991.Slovene.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett1991.Slovene.instReprValue.repr : Value → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Slovene.instReprValue : Repr Value

Equations

• Corbett1991.Slovene.instReprValue = { reprPrec := Corbett1991.Slovene.instReprValue.repr }

@[instance_reducible]

instance Corbett1991.Slovene.instFintypeValue : Fintype Value

Equations

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

inductive Corbett1991.Slovene.Ending : Type

The endings of the past active participle.

• zero : Ending
• a : Ending
• o : Ending
• i : Ending
• e : Ending

@[instance_reducible]

instance Corbett1991.Slovene.instDecidableEqEnding : DecidableEq Ending

Equations

• Corbett1991.Slovene.instDecidableEqEnding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett1991.Slovene.instReprEnding.repr : Ending → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Slovene.instReprEnding : Repr Ending

Equations

• Corbett1991.Slovene.instReprEnding = { reprPrec := Corbett1991.Slovene.instReprEnding.repr }

@[instance_reducible]

instance Corbett1991.Slovene.instFintypeEnding : Fintype Ending

Equations

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

def Corbett1991.Slovene.Value.sgEnding : Value → Ending

The singular ending of each gender.

Equations

• Corbett1991.Slovene.Value.masc.sgEnding = Corbett1991.Slovene.Ending.zero
• Corbett1991.Slovene.Value.fem.sgEnding = Corbett1991.Slovene.Ending.a
• Corbett1991.Slovene.Value.neut.sgEnding = Corbett1991.Slovene.Ending.o

def Corbett1991.Slovene.Value.duEnding : Value → Ending

The dual ending of each gender.

Equations

• Corbett1991.Slovene.Value.masc.duEnding = Corbett1991.Slovene.Ending.a
• Corbett1991.Slovene.Value.fem.duEnding = Corbett1991.Slovene.Ending.i
• Corbett1991.Slovene.Value.neut.duEnding = Corbett1991.Slovene.Ending.i

def Corbett1991.Slovene.Value.plEnding : Value → Ending

The plural ending of each gender.

Equations

• Corbett1991.Slovene.Value.masc.plEnding = Corbett1991.Slovene.Ending.i
• Corbett1991.Slovene.Value.fem.plEnding = Corbett1991.Slovene.Ending.e
• Corbett1991.Slovene.Value.neut.plEnding = Corbett1991.Slovene.Ending.a

theorem Corbett1991.Slovene.parallel_sg_pl : Gender.Parallel Value.sgEnding Value.plEnding

theorem Corbett1991.Slovene.convergent_sg_du : Gender.Convergent Value.sgEnding Value.duEnding

theorem Corbett1991.Slovene.convergent_pl_du : Gender.Convergent Value.plEnding Value.duEnding

theorem Corbett1991.Tamil.convergent : Gender.Convergent Tamil.Gender.Value.sgConcord Tamil.Gender.Value.plConcord

In Figure 6.8 three singular target genders converge on two in the plural.

theorem Corbett1991.Tamil.card_plConcord_le : Nat.card ↑(Set.range Tamil.Gender.Value.plConcord) ≤ Nat.card ↑(Set.range Tamil.Gender.Value.sgConcord)

Greenberg's Universal 37 holds in Tamil as a corollary of convergence, a number whose target genders are determined by another's distinguishing no more of them. The book states the universal over target genders because it holds of crossed systems too, Lak above.

Hybrid nouns and the Agreement Hierarchy (chapter 8)

def Corbett1991.frenchTitles : Agreement.Hybrid Agreement.Position

Table 8.1, with the English boat nouns of §6.4.5 and the Bantu hybrids of §8.3.

Equations

• Corbett1991.frenchTitles Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.frenchTitles Agreement.Position.predicate = some Agreement.Availability.syntacticOnly
• Corbett1991.frenchTitles Agreement.Position.relativePronoun = some Agreement.Availability.syntacticOnly
• Corbett1991.frenchTitles Agreement.Position.personalPronoun = some Agreement.Availability.mostlySyntactic

def Corbett1991.madchen : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.madchen Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.madchen Agreement.Position.relativePronoun = some Agreement.Availability.syntacticOnly
• Corbett1991.madchen Agreement.Position.personalPronoun = some Agreement.Availability.both
• Corbett1991.madchen Agreement.Position.predicate = none

def Corbett1991.lajdaki : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.lajdaki Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.lajdaki Agreement.Position.predicate = some Agreement.Availability.syntacticOnly
• Corbett1991.lajdaki Agreement.Position.relativePronoun = some Agreement.Availability.syntacticOnly
• Corbett1991.lajdaki Agreement.Position.personalPronoun = some Agreement.Availability.semanticOnly

def Corbett1991.spanishTitles : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.spanishTitles Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.spanishTitles Agreement.Position.predicate = some Agreement.Availability.semanticOnly
• Corbett1991.spanishTitles Agreement.Position.relativePronoun = some Agreement.Availability.semanticOnly
• Corbett1991.spanishTitles Agreement.Position.personalPronoun = some Agreement.Availability.semanticOnly

def Corbett1991.konkani : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.konkani Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.konkani Agreement.Position.predicate = some Agreement.Availability.semanticOnly
• Corbett1991.konkani Agreement.Position.personalPronoun = some Agreement.Availability.semanticOnly
• Corbett1991.konkani Agreement.Position.relativePronoun = none

def Corbett1991.vrac : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.vrac Agreement.Position.attributive = some Agreement.Availability.mostlySyntactic
• Corbett1991.vrac Agreement.Position.predicate = some Agreement.Availability.both
• Corbett1991.vrac Agreement.Position.relativePronoun = some Agreement.Availability.mostlySemantic
• Corbett1991.vrac Agreement.Position.personalPronoun = some Agreement.Availability.mostlySemantic

def Corbett1991.gazde : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.gazde Agreement.Position.attributive = some Agreement.Availability.mostlySyntactic
• Corbett1991.gazde Agreement.Position.predicate = some Agreement.Availability.both
• Corbett1991.gazde Agreement.Position.relativePronoun = some Agreement.Availability.mostlySemantic
• Corbett1991.gazde Agreement.Position.personalPronoun = some Agreement.Availability.semanticOnly

def Corbett1991.boat : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.boat Agreement.Position.relativePronoun = some Agreement.Availability.syntacticOnly
• Corbett1991.boat Agreement.Position.personalPronoun = some Agreement.Availability.both
• Corbett1991.boat x✝ = none

def Corbett1991.kamwana : Agreement.Hybrid Agreement.Position

kamwana takes gender 12/13 forms normally, and gender 1/2 is also possible for a personal pronoun sufficiently removed from the controller.

Equations

• Corbett1991.kamwana Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.kamwana Agreement.Position.predicate = some Agreement.Availability.syntacticOnly
• Corbett1991.kamwana Agreement.Position.relativePronoun = some Agreement.Availability.syntacticOnly
• Corbett1991.kamwana Agreement.Position.personalPronoun = some Agreement.Availability.mostlySyntactic

def Corbett1991.kilumba : Agreement.Hybrid Agreement.Position

Equations

• Corbett1991.kilumba Agreement.Position.attributive = some Agreement.Availability.syntacticOnly
• Corbett1991.kilumba Agreement.Position.predicate = some Agreement.Availability.both
• Corbett1991.kilumba x✝ = none

def Corbett1991.hybridNames : List (String × Agreement.Hybrid Agreement.Position)

The hybrids of Table 8.1 by the names the rows use.

Equations

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

theorem Corbett1991.hybrids_respectHierarchy (h : String × Agreement.Hybrid Agreement.Position) : h ∈ hybridNames → Agreement.RespectsHierarchy h.2

Every hybrid of Table 8.1 respects the Agreement Hierarchy.

def Corbett1991.vracFeminine : Agreement.Position → Option ℚ

At the corpus level, 16.9 per cent of 3,835 of Panov's respondents favour feminine agreement with vrač for the attributive and 51.7 per cent of 3,806 for the predicate.

Equations

• Corbett1991.vracFeminine Agreement.Position.attributive = some (169 / 1000)
• Corbett1991.vracFeminine Agreement.Position.predicate = some (517 / 1000)
• Corbett1991.vracFeminine x✝ = none

theorem Corbett1991.vracFeminine_respectsHierarchy : Agreement.RespectsHierarchy vracFeminine

The proportion of semantic agreement rises along the hierarchy.

def Corbett1991.StackedAllowed (near far : Agreement.Kind) : Prop

By the stacked-target constraint of §8.1.2, when stacked or parallel targets of one controller differ, the further one shows semantic agreement.

Equations

• Corbett1991.StackedAllowed near far = (near = Agreement.Kind.semantic → far = Agreement.Kind.semantic)

@[instance_reducible]

instance Corbett1991.instDecidableStackedAllowed (near far : Agreement.Kind) : Decidable (StackedAllowed near far)

Equations

• Corbett1991.instDecidableStackedAllowed near far = id inferInstance

Attributive possessives (§8.3)

The last stages of the loss of syntactic agreement in coastal Bantu treat the attributive possessive differently from the other attributive modifiers, a finer division of the hierarchy.

inductive Corbett1991.FinePosition : Type

The positions of the hierarchy with the attributive divided into the possessive and the other attributive modifiers, the possessive above them.

• possessive : FinePosition
• attributive : FinePosition
• predicate : FinePosition
• relativePronoun : FinePosition
• personalPronoun : FinePosition

@[instance_reducible]

instance Corbett1991.instDecidableEqFinePosition : DecidableEq FinePosition

Equations

• Corbett1991.instDecidableEqFinePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett1991.instReprFinePosition.repr : FinePosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.instReprFinePosition : Repr FinePosition

Equations

• Corbett1991.instReprFinePosition = { reprPrec := Corbett1991.instReprFinePosition.repr }

@[instance_reducible]

instance Corbett1991.instFintypeFinePosition : Fintype FinePosition

Equations

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

def Corbett1991.FinePosition.rank : FinePosition → ℕ

The rank of a fine position, the possessive on top.

Equations

• Corbett1991.FinePosition.possessive.rank = 4
• Corbett1991.FinePosition.attributive.rank = 3
• Corbett1991.FinePosition.predicate.rank = 2
• Corbett1991.FinePosition.relativePronoun.rank = 1
• Corbett1991.FinePosition.personalPronoun.rank = 0

theorem Corbett1991.FinePosition.rank_injective : Function.Injective rank

@[instance_reducible]

instance Corbett1991.FinePosition.instLinearOrder : LinearOrder FinePosition

Equations

• Corbett1991.FinePosition.instLinearOrder = LinearOrder.lift' Corbett1991.FinePosition.rank Corbett1991.FinePosition.rank_injective

def Corbett1991.FinePosition.toPosition : FinePosition → Agreement.Position

The position of the hierarchy a fine position divides.

Equations

• Corbett1991.FinePosition.possessive.toPosition = Agreement.Position.attributive
• Corbett1991.FinePosition.attributive.toPosition = Agreement.Position.attributive
• Corbett1991.FinePosition.predicate.toPosition = Agreement.Position.predicate
• Corbett1991.FinePosition.relativePronoun.toPosition = Agreement.Position.relativePronoun
• Corbett1991.FinePosition.personalPronoun.toPosition = Agreement.Position.personalPronoun

theorem Corbett1991.FinePosition.toPosition_monotone : Monotone toPosition

The finer division refines the hierarchy.

def Corbett1991.rafiki : Agreement.Hybrid FinePosition

Swahili rafiki 'friend', (47) to (49), is an animate of morphological class 9/10 with gender 1/2 agreement throughout, class 9/10 agreement remaining possible on an attributive possessive alone.

Equations

• Corbett1991.rafiki Corbett1991.FinePosition.possessive = some Agreement.Availability.both
• Corbett1991.rafiki Corbett1991.FinePosition.attributive = some Agreement.Availability.semanticOnly
• Corbett1991.rafiki Corbett1991.FinePosition.predicate = some Agreement.Availability.semanticOnly
• Corbett1991.rafiki x✝ = none

def Corbett1991.ngombe : Agreement.Hybrid FinePosition

With Kami ng'ombe 'cows' and mbudzi 'goats', (54) and (55), syntactic agreement of the predicate is rejected and both forms are accepted on attributives other than the possessive, which the book reports with class 10 agreement only.

Equations

• Corbett1991.ngombe Corbett1991.FinePosition.possessive = some Agreement.Availability.syntacticOnly
• Corbett1991.ngombe Corbett1991.FinePosition.attributive = some Agreement.Availability.both
• Corbett1991.ngombe Corbett1991.FinePosition.predicate = some Agreement.Availability.semanticOnly
• Corbett1991.ngombe x✝ = none

def Corbett1991.fineHybridNames : List (String × Agreement.Hybrid FinePosition)

The Bantu hybrids of §8.3 by the names the rows use.

Equations

• Corbett1991.fineHybridNames = [("rafiki", Corbett1991.rafiki), ("ng'ombe", Corbett1991.ngombe), ("mbudzi", Corbett1991.ngombe)]

theorem Corbett1991.fineHybrids_respectHierarchy (h : String × Agreement.Hybrid FinePosition) : h ∈ fineHybridNames → Agreement.RespectsHierarchy h.2

The Bantu hybrids respect the finer hierarchy.

The judgments of chapter 8

A row with a hybrid, a target and an agreement feature is a use of a hybrid noun at a position of the hierarchy, acceptable exactly when the hybrid's availability there admits the agreement; a row with near and far features is a pair of stacked targets. The hybrids are listed by the names the rows use.

def Corbett1991.positionNames : List (String × Agreement.Position)

The positions of the hierarchy by the names the rows use.

Equations

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

def Corbett1991.finePositionNames : List (String × FinePosition)

The fine positions by the names the rows use.

Equations

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

def Corbett1991.kindNames : List (String × Agreement.Kind)

The two agreements by the names the rows use.

Equations

• Corbett1991.kindNames = [("syntactic", Agreement.Kind.syntactic), ("semantic", Agreement.Kind.semantic)]

theorem Corbett1991.hybrid_rows (row : Datum) : row ∈ Examples.all → ∀ h ∈ hybridNames, row.feature? "hybrid" = some h.1 → ∀ t ∈ row.parse? "target" positionNames, ∀ k ∈ row.parse? "agreement" kindNames, row.judgment = Judgment.acceptable ↔ ∃ a ∈ h.2 t, a.Allows k

theorem Corbett1991.fine_rows (row : Datum) : row ∈ Examples.all → ∀ h ∈ fineHybridNames, row.feature? "hybrid" = some h.1 → ∀ t ∈ row.parse? "target" finePositionNames, ∀ k ∈ row.parse? "agreement" kindNames, row.judgment = Judgment.acceptable ↔ ∃ a ∈ h.2 t, a.Allows k

theorem Corbett1991.hybrid_rows_covered (row : Datum) : row ∈ Examples.all → ∀ n ∈ row.feature? "hybrid", (n ∈ List.map Prod.fst hybridNames ∨ n ∈ List.map Prod.fst fineHybridNames) ∧ ∀ t ∈ row.feature? "target", t ∈ List.map Prod.fst finePositionNames

Every row naming a hybrid names one of Table 8.1 or one of §8.3, at a position one of the two theorems reads.

theorem Corbett1991.stacked_rows (row : Datum) : row ∈ Examples.all → ∀ near ∈ row.parse? "near" kindNames, ∀ far ∈ row.parse? "far" kindNames, row.judgment = Judgment.acceptable ↔ StackedAllowed near far

Resolution (chapter 9)

def Corbett1991.personRules : List (Agreement.ResolutionRule Person Person)

The person resolution rules of §9.1.1, Czech's and claimed universal, give the first person if a conjunct is first person, else the second if one is second, else the third.

Equations

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

theorem Corbett1991.resolve_personRules_pair (a : Person) : a ∈ [Person.first, Person.second, Person.third] → ∀ b ∈ [Person.first, Person.second, Person.third], Agreement.ResolutionRule.resolve personRules [a, b] = some (a ⊔ b).coarsen

On the three persons the rules are the substrate's resolution coarsened to the three persons, the union of the conjuncts' participant sets without clusivity.

def Corbett1991.numberResolve (ns : Number.System) (cs : List Number) : Option Number

By the number resolution rules of §9.1.2, two singular conjuncts alone take the dual where the system has one, any other coordination with a non-plural conjunct takes the plural, and one of plurals alone resolves nothing, so that gender resolution is not triggered.

Equations

• Corbett1991.numberResolve ns cs = if Number.dual ∈ ns.values ∧ cs = [Number.singular, Number.singular] then some Number.dual else if ∀ c ∈ cs, c = Number.plural then none else some Number.plural

def Corbett1991.Tamil.Rational : Tamil.Gender.Value → Prop

Whether a gender is one of the rational genders.

Equations

• Corbett1991.Tamil.Rational x✝ = (x✝ ≠ Tamil.Gender.Value.neut)

@[instance_reducible]

instance Corbett1991.Tamil.instDecidablePredValueRational : DecidablePred Rational

Equations

• Corbett1991.Tamil.instDecidablePredValueRational v = { decide := !decide (v = Tamil.Gender.Value.neut), reflects_decide := ⋯ }

def Corbett1991.Tamil.rules : List (Agreement.ResolutionRule Tamil.Gender.Value Tamil.Gender.PlConcord)

By §9.3, all rationals take the rational form and all non-rationals the neuter, and a mixture has no resolved form.

Equations

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

theorem Corbett1991.Tamil.resolve_masc_fem : Agreement.ResolutionRule.resolve rules [Tamil.Gender.Value.masc, Tamil.Gender.Value.fem] = some Tamil.Gender.PlConcord.rational

Masculine and feminine together resolve to the rational form, (16).

theorem Corbett1991.Tamil.resolve_masc_neut : Agreement.ResolutionRule.resolve rules [Tamil.Gender.Value.masc, Tamil.Gender.Value.neut] = none

A rational and a non-rational cannot be resolved, (18).

theorem Corbett1991.Tamil.resolve_factorsThrough : Function.FactorsThrough (Agreement.ResolutionRule.resolve rules) (List.map fun (x : Tamil.Gender.Value) => decide (Rational x))

Under a strict semantic assignment with a semantic resolution, the resolved form is a function of the conjuncts' rationality.

inductive Corbett1991.Archi.PlForm : Type

The plural target genders are I/II for rationals and III/IV for the rest (Figure 6.12).

• I_II : PlForm
• III_IV : PlForm

@[instance_reducible]

instance Corbett1991.Archi.instDecidableEqPlForm : DecidableEq PlForm

Equations

• Corbett1991.Archi.instDecidableEqPlForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.Archi.instReprPlForm : Repr PlForm

Equations

• Corbett1991.Archi.instReprPlForm = { reprPrec := Corbett1991.Archi.instReprPlForm.repr }

def Corbett1991.Archi.instReprPlForm.repr : PlForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Archi.instFintypePlForm : Fintype PlForm

Equations

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

def Corbett1991.Archi.rules : List (Agreement.ResolutionRule Bool PlForm)

By §9.3, a conjunct denoting a rational brings gender I/II and any other III/IV; the descriptor is rationality, so xalq' 'people' resolves by what it denotes.

Equations

• Corbett1991.Archi.rules = [Agreement.ResolutionRule.any (fun (x : Bool) => x = true) Corbett1991.Archi.PlForm.I_II, Agreement.ResolutionRule.otherwise Corbett1991.Archi.PlForm.III_IV]

theorem Corbett1991.Archi.resolve_rational_nonrational : Agreement.ResolutionRule.resolve rules [true, false] = some PlForm.I_II

inductive Corbett1991.Luganda.PlForm : Type

The resolved forms are the class 2 and class 8 markers.

• cl2 : PlForm
• cl8 : PlForm

@[instance_reducible]

instance Corbett1991.Luganda.instDecidableEqPlForm : DecidableEq PlForm

Equations

• Corbett1991.Luganda.instDecidableEqPlForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett1991.Luganda.instReprPlForm.repr : PlForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Luganda.instReprPlForm : Repr PlForm

Equations

• Corbett1991.Luganda.instReprPlForm = { reprPrec := Corbett1991.Luganda.instReprPlForm.repr }

@[instance_reducible]

instance Corbett1991.Luganda.instFintypePlForm : Fintype PlForm

Equations

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

def Corbett1991.Luganda.rules : List (Agreement.ResolutionRule Bool PlForm)

By §9.3, all humans take class 2, no humans class 8, and a mixture class 8 if resolution is forced at all.

Equations

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

def Corbett1991.French.rulesA : List (Agreement.ResolutionRule Value Value)

The type-A rules of §9.4 give the masculine if a conjunct is masculine and the feminine otherwise.

Equations

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

def Corbett1991.French.rulesB : List (Agreement.ResolutionRule Value Value)

The type-B rules give the feminine if all conjuncts are feminine and the masculine otherwise.

Equations

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

theorem Corbett1991.French.resolve_rulesA_eq_rulesB (cs : List Value) : Agreement.ResolutionRule.resolve rulesA cs = Agreement.ResolutionRule.resolve rulesB cs

With exactly two genders the two formulations are logically equivalent (p. 280), the feminine being the complement of the masculine.

def Corbett1991.Slovene.numbers : Number.System

The numbers of Slovene.

Equations

• Corbett1991.Slovene.numbers = { values := {Number.singular, Number.dual, Number.plural} }

theorem Corbett1991.Slovene.resolve_numbers (a b : Number) : numbers.resolve a b = if a = Number.singular ∧ b = Number.singular then Number.dual else Number.plural

Two Slovene numbers resolve to the dual if both are singular and to the plural otherwise.

theorem Corbett1991.Slovene.numberResolve_eq_resolve (c d : Number) (cs : List Number) (h : ∃ x ∈ c :: d :: cs, x ≠ Number.plural) : numberResolve numbers (c :: d :: cs) = some (List.foldl numbers.resolve c (d :: cs))

When the number rules apply, their forms are semantically justified (p. 264), since a coordination with a non-plural conjunct takes the substrate's resolution of its conjuncts.

theorem Corbett1991.Slovene.numberResolve_ne_resolve (rs : List (Agreement.ResolutionRule Number Number)) : numberResolve numbers ≠ Agreement.ResolutionRule.resolve rs

The number rules count the conjuncts, so no resolution rules state them: two singulars take the dual and three the plural, though the same value occurs in both.

def Corbett1991.Slovene.rules : List (Agreement.ResolutionRule Value Value)

By §9.4, all feminines take the feminine and anything else the masculine, a type-B system in which the neuter never results from resolution.

Equations

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

theorem Corbett1991.Slovene.resolve_neuters : Agreement.ResolutionRule.resolve rules [Value.neut, Value.neut, Value.neut] = some Value.masc ∧ numberResolve numbers [Number.singular, Number.singular, Number.singular] = some Number.plural

Three neuter singulars take the masculine plural, gender resolution triggered by number resolution, (52).

theorem Corbett1991.Slovene.resolve_ne_neut (cs : List Value) : Agreement.ResolutionRule.resolve rules cs ≠ some Value.neut

The neuter is excluded as a resolved form.

def Corbett1991.Icelandic.rules : List (Agreement.ResolutionRule Gender Gender)

By §9.4, homogeneous masculines or feminines keep their gender and any mixture takes the neuter, the semantically justified gender for beings of both sexes; the rules are syntactic, reading the conjuncts' genders.

Equations

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

@[reducible, inline]

abbrev Corbett1991.Latin.Conjunct : Type

A conjunct is described by its gender and the animacy of its referent.

Equations

• Corbett1991.Latin.Conjunct = (Latin.Gender.Value × Reference.Animacy)

def Corbett1991.Latin.rules : List (Agreement.ResolutionRule Conjunct Latin.Gender.Value)

§9.5 has two syntactic rules for homogeneous genders, a semantic rule for humans, and the neuter otherwise.

Equations

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

inductive Corbett1991.Polish.PlForm : Type

The plural agreement forms.

• mascPers : PlForm
• nonMascPers : PlForm

@[instance_reducible]

instance Corbett1991.Polish.instDecidableEqPlForm : DecidableEq PlForm

Equations

• Corbett1991.Polish.instDecidableEqPlForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.Polish.instReprPlForm : Repr PlForm

Equations

• Corbett1991.Polish.instReprPlForm = { reprPrec := Corbett1991.Polish.instReprPlForm.repr }

def Corbett1991.Polish.instReprPlForm.repr : PlForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Polish.instFintypePlForm : Fintype PlForm

Equations

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

def Corbett1991.Polish.rules : List (Agreement.ResolutionRule Bool PlForm)

The obligatory rules of §9.5 give the masculine personal if a conjunct is masculine personal and the non-masculine personal otherwise. The optional rules of (60) to (62) are rows only.

Equations

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

def Corbett1991.Romanian.MaleAnimate (n : Romanian.Gender.Noun) : Prop

Whether a noun denotes a male animate.

Equations

• Corbett1991.Romanian.MaleAnimate n = (Reference.Animacy.animate ≤ n.animacy ∧ n.naturalGender = some Gender.masculine)

@[instance_reducible]

instance Corbett1991.Romanian.instDecidablePredNounMaleAnimate : DecidablePred MaleAnimate

Equations

• Corbett1991.Romanian.instDecidablePredNounMaleAnimate x✝ = id inferInstance

def Corbett1991.Romanian.rules : List (Agreement.ResolutionRule Romanian.Gender.Noun Romanian.Gender.Value)

Collapsed over the fragment's nouns, §9.5 gives the masculine if a conjunct is a male animate or all are masculine, and the feminine otherwise.

Equations

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

theorem Corbett1991.Romanian.resolve_perete_scaun : Agreement.ResolutionRule.resolve rules [Romanian.Gender.perete, Romanian.Gender.scaun] = some Romanian.Gender.Value.fem

A masculine and a neuter inanimate resolve to the feminine, the form the neuter takes in the plural, (69).

def Corbett1991.SerboCroat.stage2 : List (List (Agreement.ResolutionRule (Slovene.Value × Bool) Slovene.Value))

Stage 2 of §9.7, the alternative formulation, stage 1 being Slovene's rules, gives the feminine if all conjuncts are female, optionally the feminine if all are feminine, and the masculine otherwise. The optional rule yields a second grammar.

Equations

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

theorem Corbett1991.SerboCroat.feminine_inanimates_masc : ∃ g ∈ stage2, Agreement.ResolutionRule.resolve g [(Slovene.Value.fem, false), (Slovene.Value.fem, false)] = some Slovene.Value.masc

Feminine inanimates may take the masculine, (77) and (78).

theorem Corbett1991.SerboCroat.females_fem (g : List (Agreement.ResolutionRule (Slovene.Value × Bool) Slovene.Value)) : g ∈ stage2 → Agreement.ResolutionRule.resolve g [(Slovene.Value.fem, true), (Slovene.Value.fem, true)] = some Slovene.Value.fem

Feminine nouns denoting females keep the feminine in both grammars.

inductive Corbett1991.Ojibwa.Value : Type

• animate : Value
• inanimate : Value

@[instance_reducible]

instance Corbett1991.Ojibwa.instDecidableEqValue : DecidableEq Value

Equations

• Corbett1991.Ojibwa.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Corbett1991.Ojibwa.instReprValue : Repr Value

Equations

• Corbett1991.Ojibwa.instReprValue = { reprPrec := Corbett1991.Ojibwa.instReprValue.repr }

def Corbett1991.Ojibwa.instReprValue.repr : Value → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Corbett1991.Ojibwa.instFintypeValue : Fintype Value

Equations

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

def Corbett1991.Ojibwa.rules : List (Agreement.ResolutionRule Value Value)

By §9.7, homogeneous conjuncts keep their gender, and animate and inanimate cannot be conjoined.

Equations

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

theorem Corbett1991.Ojibwa.resolve_mixed : Agreement.ResolutionRule.resolve rules [Value.animate, Value.inanimate] = none

The judgments of chapter 9

A row with a conjuncts and a resolved feature names its conjuncts and the form the predicate shows; it is acceptable exactly when the language's rules select that form.

theorem Corbett1991.czech_rows (row : Datum) : row ∈ Examples.all → row.language = "czec1258" → ∀ cs ∈ row.parse? "conjuncts" [("1+2", [Person.first, Person.second]), ("3+1", [Person.third, Person.first]), ("3+2", [Person.third, Person.second])], ∀ p ∈ row.parse? "resolved" [("1", Person.first), ("2", Person.second)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve personRules cs = some p

theorem Corbett1991.tamil_rows (row : Datum) : row ∈ Examples.all → row.language = "tami1289" → ∀ cs ∈ row.parse? "conjuncts" [("masc+masc", [Tamil.Gender.Value.masc, Tamil.Gender.Value.masc]), ("fem+fem", [Tamil.Gender.Value.fem, Tamil.Gender.Value.fem]), ("fem+masc", [Tamil.Gender.Value.fem, Tamil.Gender.Value.masc]), ("neut+neut", [Tamil.Gender.Value.neut, Tamil.Gender.Value.neut]), ("masc+neut", [Tamil.Gender.Value.masc, Tamil.Gender.Value.neut])], ∀ g ∈ row.parse? "resolved" [("rational", Tamil.Gender.PlConcord.rational), ("neuter", Tamil.Gender.PlConcord.neuter)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Tamil.rules cs = some g

theorem Corbett1991.archi_rows (row : Datum) : row ∈ Examples.all → row.language = "arch1244" → ∀ cs ∈ row.parse? "conjuncts" [("rational+rational", [true, true]), ("rational+nonrational", [true, false]), ("nonrational+nonrational", [false, false])], ∀ g ∈ row.parse? "resolved" [("I/II", Archi.PlForm.I_II), ("III/IV", Archi.PlForm.III_IV)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Archi.rules cs = some g

theorem Corbett1991.luganda_rows (row : Datum) : row ∈ Examples.all → row.language = "gand1255" → ∀ cs ∈ row.parse? "conjuncts" [("human+human+human", [true, true, true]), ("nonhuman+nonhuman+nonhuman+nonhuman", [false, false, false, false]), ("human+nonhuman", [true, false])], ∀ g ∈ row.parse? "resolved" [("2", Luganda.PlForm.cl2), ("8", Luganda.PlForm.cl8)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Luganda.rules cs = some g

theorem Corbett1991.french_rows (row : Datum) : row ∈ Examples.all → row.language = "stan1290" → ∀ cs ∈ row.parse? "conjuncts" [("masc+masc", [French.Value.masc, French.Value.masc]), ("fem+fem", [French.Value.fem, French.Value.fem]), ("masc+fem", [French.Value.masc, French.Value.fem])], ∀ g ∈ row.parse? "resolved" [("masc", French.Value.masc), ("fem", French.Value.fem)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve French.rulesA cs = some g

theorem Corbett1991.slovene_rows (row : Datum) : row ∈ Examples.all → row.language = "slov1268" → ∀ cs ∈ row.parse? "conjuncts" [("masc+fem", [Slovene.Value.masc, Slovene.Value.fem]), ("masc+neut", [Slovene.Value.masc, Slovene.Value.neut]), ("fem+neut", [Slovene.Value.fem, Slovene.Value.neut]), ("neut+neut", [Slovene.Value.neut, Slovene.Value.neut]), ("fem+fem", [Slovene.Value.fem, Slovene.Value.fem]), ("neut+neut+neut", [Slovene.Value.neut, Slovene.Value.neut, Slovene.Value.neut]), ("fem+fem+fem", [Slovene.Value.fem, Slovene.Value.fem, Slovene.Value.fem])], ∀ g ∈ row.parse? "resolved" [("masc", Slovene.Value.masc), ("fem", Slovene.Value.fem)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Slovene.rules cs = some g

theorem Corbett1991.slovene_number_rows (row : Datum) : row ∈ Examples.all → row.language = "slov1268" → ∀ ns ∈ row.parse? "numbers" [("sg+sg", [Number.singular, Number.singular]), ("sg+sg+sg", [Number.singular, Number.singular, Number.singular]), ("sg+du", [Number.singular, Number.dual])], ∀ n ∈ row.parse? "number" [("dual", Number.dual), ("plural", Number.plural)], row.judgment = Judgment.acceptable ↔ numberResolve Slovene.numbers ns = some n

theorem Corbett1991.icelandic_rows (row : Datum) : row ∈ Examples.all → row.language = "icel1247" → ∀ cs ∈ row.parse? "conjuncts" [("masc+fem", [Icelandic.Nouns.drengur, Icelandic.Nouns.telpa]), ("fem+neut", [Icelandic.Nouns.aer, Icelandic.Nouns.lamb])], ∀ g ∈ row.parse? "resolved" [("neut", Gender.neuter)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Icelandic.rules (List.map (fun (x : GenderedNoun Gender) => x.gender) cs) = some g

theorem Corbett1991.polish_rows (row : Datum) : row ∈ Examples.all → row.language = "poli1260" → ∀ cs ∈ row.parse? "conjuncts" [("fem+fem", [false, false]), ("mascPers+fem+fem", [true, false, false])], ∀ g ∈ row.parse? "resolved" [("mascPers", Polish.PlForm.mascPers), ("nonMascPers", Polish.PlForm.nonMascPers)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Polish.rules cs = some g

theorem Corbett1991.latin_rows (row : Datum) : row ∈ Examples.all → row.language = "lati1261" → ∀ cs ∈ row.parse? "conjuncts" [("masc.human+fem.human", [(Latin.Gender.Value.masc, Reference.Animacy.human), (Latin.Gender.Value.fem, Reference.Animacy.human)]), ("masc.inanimate+fem.inanimate", [(Latin.Gender.Value.masc, Reference.Animacy.inanimate), (Latin.Gender.Value.fem, Reference.Animacy.inanimate)])], ∀ g ∈ row.parse? "resolved" [("masc", Latin.Gender.Value.masc), ("neut", Latin.Gender.Value.neut)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Latin.rules cs = some g

theorem Corbett1991.romanian_resolution_rows (row : Datum) : row ∈ Examples.all → row.language = "roma1327" → ∀ cs ∈ row.parse? "conjuncts" [("fată+femeie", [Romanian.Gender.fata, Romanian.Gender.femeie]), ("băiat+bărbat", [Romanian.Gender.baiat, Romanian.Gender.barbat]), ("băiat+fată", [Romanian.Gender.baiat, Romanian.Gender.fata]), ("uşă+perete", [Romanian.Gender.usa, Romanian.Gender.perete]), ("perete+scaun", [Romanian.Gender.perete, Romanian.Gender.scaun]), ("scaun+masă", [Romanian.Gender.scaun, Romanian.Gender.masa]), ("nuc+prun", [Romanian.Gender.nuc, Romanian.Gender.prun]), ("frigider+televizor", [Romanian.Gender.frigider, Romanian.Gender.televizor]), ("uşă+masă", [Romanian.Gender.usa, Romanian.Gender.masa])], ∀ g ∈ row.parse? "resolved" [("masc", Romanian.Gender.Value.masc), ("fem", Romanian.Gender.Value.fem)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Romanian.rules cs = some g

theorem Corbett1991.ojibwa_rows (row : Datum) : row ∈ Examples.all → row.language = "ojib1241" → ∀ cs ∈ row.parse? "conjuncts" [("animate+animate", [Ojibwa.Value.animate, Ojibwa.Value.animate]), ("inanimate+inanimate", [Ojibwa.Value.inanimate, Ojibwa.Value.inanimate]), ("animate+inanimate", [Ojibwa.Value.animate, Ojibwa.Value.inanimate])], ∀ g ∈ row.parse? "resolved" [("animate", Ojibwa.Value.animate), ("inanimate", Ojibwa.Value.inanimate)], row.judgment = Judgment.acceptable ↔ Agreement.ResolutionRule.resolve Ojibwa.rules cs = some g

The judgments of chapter 3

A Swahili row with a noun and a concord feature is acceptable exactly when the concord is the gender the assignment rules give the noun.

theorem Corbett1991.swahili_rows (row : Datum) : row ∈ Examples.all → row.language = "swah1253" → ∀ n ∈ row.parse? "noun" (List.map (fun (n : Swahili.Noun) => (n.form, n)) Swahili.allNouns), ∀ g ∈ row.parse? "concord" [("1/2", Swahili.Gender.genderA), ("3/4", Swahili.Gender.genderB), ("7/8", Swahili.Gender.genderD)], row.judgment = Judgment.acceptable ↔ Swahili.system.assign Swahili.sem Swahili.Noun.morphClass n = g