Gender — comparative labels and per-language systems

[Cor91] [Kra15] [Kra20] [CF16] [SS20]

Gender has no universal value inventory. A gender is a language-particular equivalence class of agreement behavior ([Cor91], crediting [Hoc58]; [Kra15] def (1) p. 65; [SS20] fn. 1) — so, unlike Number and Person, whose values a universal feature calculus labels language-independently ([Har14a], [Har16a]), the root Gender type is not a canonical value inventory but a vocabulary of comparative-concept labels. The canonical object is Gender.System: a language's own finite carrier of controller genders. [Kra15]'s gender feature calculus generates at most three genders (Table 11.1); beyond that it requires per-class identity features (§11.2.2) — a language-particular carrier in all but name. This file encodes the carrier directly, the way Basis ι R M takes the index type as a parameter.

Main declarations

• Gender — the six comparative labels (sex-based masculine, feminine, neuter, common; animacy-based animate, inanimate), with realization Gender.toUD and ingestion Gender.fromUD — UD.Gender is realization vocabulary, exactly as UD.Number/UD.Person are for Number/Person.
• Gender.System — a language's gender system over its own carrier G of controller genders: a partial comparative labeling and a morphosyntactic default. The gender count is Fintype.card G, and [Kra15]'s two-class minimum (def (7i), p. 70) is the mathlib typeclass Nontrivial G — one agreement pattern for all nouns is the absence of a system, not a one-gender system.
• Gender.Faithful — distinct genders are distinguished by some agreement target: injectivity of per-gender agreement behavior. Yields Gender.Faithful.card_le_pow: a language whose agreement shows f forms on each of t targets supports at most f ^ t controller genders.
• Gender.System.Assigned — a system with noun-level assignment. SemanticCore is [Kra15]'s (7ii) ([Dah00]'s generalization: assignment is semantically determined on a nonempty core of animate nouns; "no language assigns genders completely randomly or completely formally", p. 70). assign_factorsThrough derives the Hockett–Corbett definition as a theorem: when agreement is mediated by gender and the carrier is faithful, assignment factors through observable agreement behavior.

Implementation notes

• Carrier discipline. G is the controller-gender partition: singular and plural of one noun are one gender (Bantu "Class 1/2" convention, [Kra15] p. 252). Classifiers and declension class are out of scope — they do not trigger agreement ([Kra15] §4.1.1); nominal form classes (deriflection, [GF19]) are a distinct dimension and must not be conflated with the carrier.
• Locus-neutral. System makes no claim about where gender sits in the nominal spine (n vs Num vs D); locus claims are study content.
• Languages lacking gender — the majority ([Kra15] §11.2.4) — declare no System.
• Feature decompositions of the labels, interpretation, and resolution are separate modules; fragments' fine-grained gender enums are System carriers, and their ad-hoc label maps are the label field.

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 the carrier of its Gender.System; label maps them (partially) into this vocabulary.

• masculine : Gender

  Masculine: male humans/higher animates; default in many sex-based systems.

• feminine : Gender

  Feminine: female humans/higher animates; marked in many sex-based systems.

• neuter : Gender

  Neuter: neither masculine nor feminine; inanimate default in 3-gender systems.

• common : Gender

  Common: merged masculine + feminine (Swedish, Danish).

• animate : Gender

  Animate: animate referents in animacy-based systems (Algonquian).

• inanimate : Gender

  Inanimate: inanimate referents in animacy-based systems.

@[implicit_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✝

@[implicit_reducible]

instance instReprGender : Repr Gender

Equations

• instReprGender = { reprPrec := instReprGender.repr }

@[implicit_reducible]

instance instFintypeGender : Fintype Gender

Equations

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

Realization: Universal Dependencies

UD.Gender is the surface tagset corpora annotate, not an analytical inventory: animacy-based labels have no UD realization.

def Gender.toUD : Gender → Option UD.Gender

Realize a comparative label as a UD gender tag, where one exists.

Equations

• Gender.masculine.toUD = some UD.Gender.Masc
• Gender.feminine.toUD = some UD.Gender.Fem
• Gender.neuter.toUD = some UD.Gender.Neut
• Gender.common.toUD = some UD.Gender.Com
• Gender.animate.toUD = none
• Gender.inanimate.toUD = none

def Gender.fromUD : UD.Gender → Gender

Ingest a UD gender tag. Total: every UD gender has a comparative label.

Equations

• Gender.fromUD UD.Gender.Masc = Gender.masculine
• Gender.fromUD UD.Gender.Fem = Gender.feminine
• Gender.fromUD UD.Gender.Neut = Gender.neuter
• Gender.fromUD UD.Gender.Com = Gender.common

@[simp]

theorem Gender.toUD_fromUD (u : UD.Gender) : (fromUD u).toUD = some u

theorem Gender.fromUD_of_toUD_eq_some {g : Gender} {u : UD.Gender} : g.toUD = some u → fromUD u = g

Labels with a UD realization round-trip.

Gender systems

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 the partial label field — the carrier itself is not constrained to fit them, which is what accommodates Bantu-scale inventories that no label vocabulary covers.

structure Gender.System (G : Type u_2) : Type u_2

A language's gender system over its own carrier G of controller genders ([Cor91]; [Kra15]).

The gender count is Fintype.card G; the two-class minimum is the hypothesis Nontrivial G on consumers that need it. Languages without gender agreement declare no System.

• label : G → Option Gender

  Partial comparative labeling of the controller genders. Bantu-style classes typically map to none outside a human/animate core.

• default : G

  The morphosyntactic default: the gender realized when there are no gender features to agree with. Per-system data, not derivable ([Kra15]: feminine defaults are attested).

Agreement faithfulness

[Cor91]'s definition operationalized. Agreement evidence for a carrier G is a behavior map agr : G → T → F — for each gender, the form each target shows. 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 (two "genders" that agree alike everywhere are one gender). Target and form types are parameters: the substrate is neutral about what counts as a target (predicate, attributive, pronoun), which is where strict-Agree vs loose-covariation definitions of gender-hood differ ([Kra15] §4.1.2).

@[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.

An abbrev so that Function.Injective's decidability instance (under [Fintype G], [DecidableEq T], [DecidableEq F]) applies: 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.

Assigned systems and the semantic core

The assigned tier adds the noun-level assignment function — the Canonical Gender Principle that each noun has a single gender value ([CF16]) is its functionality. [Kra15]'s (7ii) lives here: no attested system assigns gender completely randomly or completely formally; some nonempty core of animate nouns is assigned by interpretation.

structure Gender.System.Assigned (N : Type u_6) (G : Type u_7) extends Gender.System G : Type (max u_6 u_7)

A gender system together with its assignment: every noun of N gets exactly one controller gender. Paradigm-only fragments stay at the System tier.

• label : G → Option Gender
• default : G
• assign : N → G

  Gender assignment.

def Gender.System.Assigned.SemanticCore {G : Type u_1} {N : Type u_2} {σ : Type u_5} (S : Assigned N G) (core : Set N) (sem : N → σ) : Prop

The assignment has a semantic core: a nonempty set of nouns on which a semantic classification sem determines gender ([Kra15], after [Dah00]). Arbitrary assignment is permitted off the core.

Equations

• S.SemanticCore core sem = (core.Nonempty ∧ Function.FactorsThroughOn S.assign sem core)

def Gender.System.Assigned.Mediates {G : Type u_1} {N : Type u_2} {T : Type u_3} {F : Type u_4} (S : Assigned N G) (nounAgr : N → T → F) (agr : G → T → F) : Prop

The system mediates noun-level agreement evidence nounAgr via the per-gender behavior agr: a noun's agreement behavior is its gender's.

Equations

• S.Mediates nounAgr agr = ∀ (n : N), nounAgr n = agr (S.assign n)

theorem Gender.System.Assigned.assign_factorsThrough {G : Type u_1} {N : Type u_2} {T : Type u_3} {F : Type u_4} (S : Assigned N G) {nounAgr : N → T → F} {agr : G → T → F} (med : S.Mediates nounAgr agr) (faith : Faithful agr) : Function.FactorsThrough S.assign nounAgr

The Hockett–Corbett definition of gender, derived rather than stipulated: if agreement is mediated by gender and the carrier is faithful, then gender assignment factors through observable agreement behavior.