Gender systems

This file defines a language's gender system over its own carrier of controller genders, the comparative labels cross-linguistic comparison uses for them, and the assigned system that gives every noun a controller gender.

A gender is a class of nouns that take the same agreements, so a language's genders are language-particular: there is no universal inventory of gender values as there is of number and person values, only a vocabulary of comparative labels, masculine, feminine, neuter, common, animate and inanimate, that a system's genders may partially bear. The carrier of controller genders is a type parameter, as the index type of a basis is, and the number of genders is its cardinality; a carrier is faithful to agreement evidence when distinct genders are distinguished by some target. The rules assigning nouns to genders are the assignment systems of Syntax/Gender/Assignment.lean.

Main definitions

• Gender: the comparative labels; the Universal Dependencies realization is in Morphology/Word/UD.lean.
• Gender.Faithful: a carrier is faithful to agreement evidence when the evidence is injective.

Main results

• Gender.Faithful.card_le_pow: f forms on each of t targets support at most f ^ t controller genders.
• Gender.factorsThrough_of_faithful: when a faithful carrier mediates agreement, assignment factors through agreement behaviour, genders as agreement classes by theorem rather than by stipulation.

Implementation notes

• The carrier is the controller-gender partition: singular and plural of one noun are one gender. Classifiers and declension classes trigger no agreement and are not carriers.
• The carrier makes no claim about where gender sits in the nominal spine; that is study content. Languages lacking gender, the majority, declare no carrier.
• Kramer's two-class minimum is the hypothesis Nontrivial G on the consumers that need it: one agreement pattern for all nouns is the absence of a system.
• Assignment systems, feature decompositions of the labels and the agreement classes of nouns are separate modules; fragments' gender enums are carriers, and a fragment's toLabel maps its carrier into the comparative labels.

References

• [Cor91] — genders as agreement classes, crediting [Hoc58]
• [Zal64] — agreement classes
• [Kra15] — the two-class minimum
• [CF16] — canonical gender
• [Har14a] — the universal calculi of number and person, which gender lacks

inductive Gender : Type

Comparative-concept labels for controller genders ([Cor91]).

These are the descriptive labels cross-linguistic comparison uses for a language's agreement classes — not a universal value inventory. A language's actual genders are its own carrier, which a fragment's toLabel maps into this vocabulary.

• masculine : Gender

  The masculine holds male humans and higher animates, and is the default in many sex-based systems.

• feminine : Gender

  The feminine holds female humans and higher animates, and is marked in many sex-based systems.

• neuter : Gender

  The neuter is neither masculine nor feminine, and is the inanimate default in three-gender systems.

• common : Gender

  The common gender merges masculine and feminine (Swedish, Danish).

• animate : Gender

  The animate holds animate referents in animacy-based systems (Algonquian).

• inanimate : Gender

  The inanimate holds inanimate referents in animacy-based systems.

@[instance_reducible]

instance instDecidableEqGender : DecidableEq Gender

Equations

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

def instReprGender.repr : Gender → ℕ → Std.Format

Equations

• instReprGender.repr Gender.masculine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.masculine")).group prec✝
• instReprGender.repr Gender.feminine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.feminine")).group prec✝
• instReprGender.repr Gender.neuter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.neuter")).group prec✝
• instReprGender.repr Gender.common prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.common")).group prec✝
• instReprGender.repr Gender.animate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.animate")).group prec✝
• instReprGender.repr Gender.inanimate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.inanimate")).group prec✝

@[instance_reducible]

instance instReprGender : Repr Gender

Equations

• instReprGender = { reprPrec := instReprGender.repr }

@[instance_reducible]

instance instFintypeGender : Fintype Gender

Equations

• instFintypeGender = { elems := { val := ↑Gender.enumList, nodup := Gender.enumList_nodup }, complete := instFintypeGender._proof_1 }

Carriers

A gender system is language-particular: its values are the language's own controller genders, supplied as the carrier type G, a fragment's gender enum. The comparative labels above enter only through a fragment's partial map into them; the carrier itself is not constrained to fit them, which is what accommodates Bantu-scale inventories that no label vocabulary covers.

Agreement faithfulness

Agreement evidence for a carrier G is a behaviour map agr : G → T → F, the form each target shows for each gender. The carrier is faithful to the evidence when distinct genders are distinguished by some target; a carrier that is not faithful has posited a spurious distinction, since two genders that agree alike everywhere are one gender. The target and form types are parameters: the substrate is neutral about what counts as a target, which is where [Kra15]'s strict-Agree and loose-covariation definitions of gender differ.

@[reducible, inline]

abbrev Gender.Faithful {G : Type u_1} {T : Type u_2} {F : Type u_3} (agr : G → T → F) : Prop

A carrier G of controller genders is faithful to agreement evidence agr when distinct genders are distinguished by some target's form.

It is an abbrev so that Function.Injective's decidability instance (under [Fintype G], [DecidableEq T], [DecidableEq F]) applies and concrete fragments discharge faithfulness by decide.

Equations

• Gender.Faithful agr = Function.Injective agr

theorem Gender.Faithful.card_le_pow {G : Type u_1} {T : Type u_2} {F : Type u_3} [Fintype G] [Fintype T] [Fintype F] [DecidableEq T] {agr : G → T → F} (h : Faithful agr) : Fintype.card G ≤ Fintype.card F ^ Fintype.card T

A language whose agreement morphology shows f forms on each of t targets supports at most f ^ t controller genders.

Assignment and agreement

An assignment gives every noun one controller gender, the Canonical Gender Principle of [CF16]. When noun-level agreement is the per-gender behaviour of the assigned gender and the carrier is faithful, assignment factors through observable agreement behaviour: genders are agreement classes in [Zal64]'s sense, the starting point of [Cor91]'s definition. Corbett's controller genders discount subgenders, inquorate genders and overdifferentiated targets on the way from agreement classes to genders, and those steps are not modelled here.

theorem Gender.factorsThrough_of_faithful {G : Type u_1} {N : Type u_2} {T : Type u_3} {F : Type u_4} {assign : N → G} {nounAgr : N → T → F} {agr : G → T → F} (med : nounAgr = agr ∘ assign) (faith : Faithful agr) : Function.FactorsThrough assign nounAgr

Genders are agreement classes by derivation, not stipulation. If noun-level agreement nounAgr is the per-gender behaviour agr of the assigned gender and the carrier is faithful, then gender assignment factors through observable agreement behaviour.