Pronoun — typological survey (WALS)

[DH13b] [nichols-peterson-2013]

The cross-linguistic WALS-survey facet of the pronoun object: the friendly feature enums (Chs 39–48) and phonological-shape enums (Chs 136–137), their fromWALS* converters, the iso-keyed accessors that read a language's value from the Data.WALS layer, and the distribution theorems.

A language's WALS pronoun fact is a function of its ISO code (Pronoun.genderDistinction "kor"), derived from Data.WALS — there is no per-language Profile bundle (that was write-only and is gone). When a study needs to ground a Fragment analysis against WALS, it states a decide-checked theorem over the accessor in that study file.

Main declarations

• Pronoun.genderDistinction, politeness, inclusiveExclusive, … — iso-keyed accessors for the WALS Chs 39–48 feature-system survey, derived from Data.WALS via the fromWALS* converters.
• Pronoun.mtPattern, mIn1sg, nmPattern, mIn2sg — iso-keyed accessors for the M-T / N-M phonological-shape survey, WALS Chs 136–137 ([nichols-peterson-2013]).
• Pronoun.Plurality — how independent personal pronouns encode number, WALS Ch 35. The canonical home for this pronoun-paradigm feature; the per-language values are carried by Morphology.Number.PluralityProfile (which bundles it with the nominal-plurality Chs 33/34/36).

inductive Pronoun.InclusiveExclusive : Type

WALS Ch 39: inclusive/exclusive distinction in independent pronouns.

• noWe : InclusiveExclusive

  No first-person plural pronoun at all.

• weEqualsI : InclusiveExclusive

  'We' = 'I' (no number distinction in 1st person).

• noDistinction : InclusiveExclusive

  1st-pl exists but no incl/excl distinction.

• onlyInclusive : InclusiveExclusive

  Only inclusive form; no dedicated exclusive pronoun.

• inclusiveExclusive : InclusiveExclusive

  Full inclusive/exclusive distinction in 1st-pl.

@[implicit_reducible]

instance Pronoun.instDecidableEqInclusiveExclusive : DecidableEq InclusiveExclusive

Equations

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

def Pronoun.instReprInclusiveExclusive.repr : InclusiveExclusive → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprInclusiveExclusive : Repr InclusiveExclusive

Equations

• Pronoun.instReprInclusiveExclusive = { reprPrec := Pronoun.instReprInclusiveExclusive.repr }

inductive Pronoun.InclusiveExclusivePamaNyungan : Type

WALS Ch 39B: incl/excl forms in Pama-Nyungan languages (areal sub-feature).

• noOpposition : InclusiveExclusivePamaNyungan

  No incl/excl opposition in 1st-pl.

• differentiated : InclusiveExclusivePamaNyungan

  Inclusive and exclusive forms differentiated.

@[implicit_reducible]

instance Pronoun.instDecidableEqInclusiveExclusivePamaNyungan : DecidableEq InclusiveExclusivePamaNyungan

Equations

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

@[implicit_reducible]

instance Pronoun.instReprInclusiveExclusivePamaNyungan : Repr InclusiveExclusivePamaNyungan

Equations

• Pronoun.instReprInclusiveExclusivePamaNyungan = { reprPrec := Pronoun.instReprInclusiveExclusivePamaNyungan.repr }

def Pronoun.instReprInclusiveExclusivePamaNyungan.repr : InclusiveExclusivePamaNyungan → ℕ → Std.Format

Equations

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

inductive Pronoun.InclusiveExclusiveVerbal : Type

WALS Ch 40: incl/excl distinction in verbal inflection.

• noPersonMarking : InclusiveExclusiveVerbal

  No person marking on verbs at all.

• weEqualsI : InclusiveExclusiveVerbal

  'We' verbal form = 'I' form.

• noDistinction : InclusiveExclusiveVerbal

  Person marking exists but no incl/excl.

• onlyInclusive : InclusiveExclusiveVerbal

  Only inclusive marking in verbal inflection.

• inclusiveExclusive : InclusiveExclusiveVerbal

  Full incl/excl distinction in verbal inflection.

@[implicit_reducible]

instance Pronoun.instDecidableEqInclusiveExclusiveVerbal : DecidableEq InclusiveExclusiveVerbal

Equations

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

def Pronoun.instReprInclusiveExclusiveVerbal.repr : InclusiveExclusiveVerbal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprInclusiveExclusiveVerbal : Repr InclusiveExclusiveVerbal

Equations

• Pronoun.instReprInclusiveExclusiveVerbal = { reprPrec := Pronoun.instReprInclusiveExclusiveVerbal.repr }

inductive Pronoun.GenderDistinction : Type

WALS Ch 44: where gender distinctions appear in the pronoun paradigm.

• in3rdAndOtherPersons : GenderDistinction

  Gender in 3rd person AND in 1st/2nd person (e.g., Arabic, Hebrew).

• in3rdPersonIncludingNonSg : GenderDistinction

  Gender in 3rd person only, including non-singular forms (e.g., Polish, Albanian).

• in3rdPersonSgOnly : GenderDistinction

  Gender in 3rd person singular only (e.g., English he/she/it).

• in1stOr2ndOnly : GenderDistinction

  Gender in 1st or 2nd person but not 3rd (rare; e.g., Iraqw).

• in3rdPersonNonSgOnly : GenderDistinction

  Gender in 3rd person non-singular only (extremely rare).

• noGenderDistinctions : GenderDistinction

  No gender distinctions in pronouns (e.g., Finnish, Turkish, Japanese).

@[implicit_reducible]

instance Pronoun.instDecidableEqGenderDistinction : DecidableEq GenderDistinction

Equations

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

def Pronoun.instReprGenderDistinction.repr : GenderDistinction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprGenderDistinction : Repr GenderDistinction

Equations

• Pronoun.instReprGenderDistinction = { reprPrec := Pronoun.instReprGenderDistinction.repr }

inductive Pronoun.PolitenessDistinction : Type

WALS Ch 45: politeness (honorific/formality) distinctions in pronouns.

• none : PolitenessDistinction

  No politeness distinction (e.g., English).

• binary : PolitenessDistinction

  Binary T/V distinction (e.g., French tu/vous, German du/Sie).

• multiple : PolitenessDistinction

  Multiple levels (e.g., Japanese, Hindi, Tagalog).

• pronounsAvoided : PolitenessDistinction

  Pronouns avoided entirely for politeness; titles/kin terms used instead (e.g., Korean, Thai).

@[implicit_reducible]

instance Pronoun.instDecidableEqPolitenessDistinction : DecidableEq PolitenessDistinction

Equations

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

@[implicit_reducible]

instance Pronoun.instReprPolitenessDistinction : Repr PolitenessDistinction

Equations

• Pronoun.instReprPolitenessDistinction = { reprPrec := Pronoun.instReprPolitenessDistinction.repr }

def Pronoun.instReprPolitenessDistinction.repr : PolitenessDistinction → ℕ → Std.Format

Equations

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

inductive Pronoun.IndefiniteType : Type

WALS Ch 46: morphological source of indefinite pronouns.

• interrogativeBased : IndefiniteType

  Based on interrogative forms (e.g., Japanese dare-ka 'who-Q' = 'someone').

• genericNounBased : IndefiniteType

  Based on generic nouns (e.g., English 'somebody' = 'some' + 'body').

• special : IndefiniteType

  Special, dedicated forms unrelated to interrogatives or generic nouns.

• mixed : IndefiniteType

  Mixed: some interrogative-based, others generic-noun-based.

• existentialConstruction : IndefiniteType

  Existential construction used instead of indefinite pronouns.

@[implicit_reducible]

instance Pronoun.instDecidableEqIndefiniteType : DecidableEq IndefiniteType

Equations

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

def Pronoun.instReprIndefiniteType.repr : IndefiniteType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprIndefiniteType : Repr IndefiniteType

Equations

• Pronoun.instReprIndefiniteType = { reprPrec := Pronoun.instReprIndefiniteType.repr }

inductive Pronoun.IntensifierReflexive : Type

WALS Ch 47: relationship between intensifiers and reflexives.

• identical : IntensifierReflexive

  Identical forms ('she herself did it' / 'she saw herself').

• differentiated : IntensifierReflexive

  Different, morphologically unrelated forms.

@[implicit_reducible]

instance Pronoun.instDecidableEqIntensifierReflexive : DecidableEq IntensifierReflexive

Equations

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

@[implicit_reducible]

instance Pronoun.instReprIntensifierReflexive : Repr IntensifierReflexive

Equations

• Pronoun.instReprIntensifierReflexive = { reprPrec := Pronoun.instReprIntensifierReflexive.repr }

def Pronoun.instReprIntensifierReflexive.repr : IntensifierReflexive → ℕ → Std.Format

Equations

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

inductive Pronoun.PersonMarkingOnAdpositions : Type

WALS Ch 48: whether adpositions bear person-marking morphology.

• noAdpositions : PersonMarkingOnAdpositions

  Language has no adpositions (head-marking or caseless).

• noPersonMarking : PersonMarkingOnAdpositions

  Adpositions exist but bear no person marking.

• pronounsOnly : PersonMarkingOnAdpositions

  Only pronominal complements trigger person marking (e.g., Hebrew be-xa 'in-you').

• pronounsAndNouns : PersonMarkingOnAdpositions

  Both pronominal and nominal complements trigger person marking.

@[implicit_reducible]

instance Pronoun.instDecidableEqPersonMarkingOnAdpositions : DecidableEq PersonMarkingOnAdpositions

Equations

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

@[implicit_reducible]

instance Pronoun.instReprPersonMarkingOnAdpositions : Repr PersonMarkingOnAdpositions

Equations

• Pronoun.instReprPersonMarkingOnAdpositions = { reprPrec := Pronoun.instReprPersonMarkingOnAdpositions.repr }

def Pronoun.instReprPersonMarkingOnAdpositions.repr : PersonMarkingOnAdpositions → ℕ → Std.Format

Equations

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

WALS converters (Chs 39, 39B, 40, 44–48)

def Pronoun.fromWALS39A : Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns → InclusiveExclusive

Equations

• Pronoun.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.noWe = Pronoun.InclusiveExclusive.noWe
• Pronoun.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.weTheSameAsI = Pronoun.InclusiveExclusive.weEqualsI
• Pronoun.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.noInclusiveExclusive = Pronoun.InclusiveExclusive.noDistinction
• Pronoun.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.onlyInclusive = Pronoun.InclusiveExclusive.onlyInclusive
• Pronoun.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.inclusiveExclusive = Pronoun.InclusiveExclusive.inclusiveExclusive

def Pronoun.fromWALS39B : Data.WALS.F39B.InclusiveExclusiveFormsInPamaNyungan → InclusiveExclusivePamaNyungan

Equations

• Pronoun.fromWALS39B Data.WALS.F39B.InclusiveExclusiveFormsInPamaNyungan.noInclusiveExclusiveOpposition = Pronoun.InclusiveExclusivePamaNyungan.noOpposition
• Pronoun.fromWALS39B Data.WALS.F39B.InclusiveExclusiveFormsInPamaNyungan.inclusiveAndExclusiveDifferentiated = Pronoun.InclusiveExclusivePamaNyungan.differentiated

def Pronoun.fromWALS40A : Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection → InclusiveExclusiveVerbal

Equations

• Pronoun.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.noPersonMarking = Pronoun.InclusiveExclusiveVerbal.noPersonMarking
• Pronoun.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.weTheSameAsI = Pronoun.InclusiveExclusiveVerbal.weEqualsI
• Pronoun.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.noInclusiveExclusive = Pronoun.InclusiveExclusiveVerbal.noDistinction
• Pronoun.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.onlyInclusive = Pronoun.InclusiveExclusiveVerbal.onlyInclusive
• Pronoun.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.inclusiveExclusive = Pronoun.InclusiveExclusiveVerbal.inclusiveExclusive

def Pronoun.fromWALS44A : Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns → GenderDistinction

Equations

• Pronoun.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.in3rdPerson1stAndOr2ndPerson = Pronoun.GenderDistinction.in3rdAndOtherPersons
• Pronoun.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonOnlyButAlsoNonSingular = Pronoun.GenderDistinction.in3rdPersonIncludingNonSg
• Pronoun.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonSingularOnly = Pronoun.GenderDistinction.in3rdPersonSgOnly
• Pronoun.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v1stOr2ndPersonButNot3rd = Pronoun.GenderDistinction.in1stOr2ndOnly
• Pronoun.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonNonSingularOnly = Pronoun.GenderDistinction.in3rdPersonNonSgOnly
• Pronoun.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.noGenderDistinctions = Pronoun.GenderDistinction.noGenderDistinctions

def Pronoun.fromWALS45A : Data.WALS.F45A.PolitenessDistinctionsInPronouns → PolitenessDistinction

Equations

• Pronoun.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.noPolitenessDistinction = Pronoun.PolitenessDistinction.none
• Pronoun.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.binaryPolitenessDistinction = Pronoun.PolitenessDistinction.binary
• Pronoun.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.multiplePolitenessDistinctions = Pronoun.PolitenessDistinction.multiple
• Pronoun.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.pronounsAvoidedForPoliteness = Pronoun.PolitenessDistinction.pronounsAvoided

def Pronoun.fromWALS46A : Data.WALS.F46A.IndefinitePronouns → IndefiniteType

Equations

• Pronoun.fromWALS46A Data.WALS.F46A.IndefinitePronouns.interrogativeBased = Pronoun.IndefiniteType.interrogativeBased
• Pronoun.fromWALS46A Data.WALS.F46A.IndefinitePronouns.genericNounBased = Pronoun.IndefiniteType.genericNounBased
• Pronoun.fromWALS46A Data.WALS.F46A.IndefinitePronouns.special = Pronoun.IndefiniteType.special
• Pronoun.fromWALS46A Data.WALS.F46A.IndefinitePronouns.mixed = Pronoun.IndefiniteType.mixed
• Pronoun.fromWALS46A Data.WALS.F46A.IndefinitePronouns.existentialConstruction = Pronoun.IndefiniteType.existentialConstruction

def Pronoun.fromWALS47A : Data.WALS.F47A.IntensifierReflexive → IntensifierReflexive

Equations

• Pronoun.fromWALS47A Data.WALS.F47A.IntensifierReflexive.identical = Pronoun.IntensifierReflexive.identical
• Pronoun.fromWALS47A Data.WALS.F47A.IntensifierReflexive.differentiated = Pronoun.IntensifierReflexive.differentiated

def Pronoun.fromWALS48A : Data.WALS.F48A.PersonMarkingOnAdpositions → PersonMarkingOnAdpositions

Equations

• Pronoun.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.noAdpositions = Pronoun.PersonMarkingOnAdpositions.noAdpositions
• Pronoun.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.noPersonMarking = Pronoun.PersonMarkingOnAdpositions.noPersonMarking
• Pronoun.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.pronounsOnly = Pronoun.PersonMarkingOnAdpositions.pronounsOnly
• Pronoun.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.pronounsAndNouns = Pronoun.PersonMarkingOnAdpositions.pronounsAndNouns

Per-language WALS accessors (Chs 39–48)

Each pronoun-system feature is a function of a language's ISO 639-3 code, derived from the Data.WALS layer through the fromWALS* converters — no per-language stipulation, replacing the former hand-stipulated Profile bundle. A fragment attaches a feature as a Lang.pronoun… one-liner over its iso; none means WALS did not sample that language for that chapter.

def Pronoun.inclusiveExclusive (iso : String) : Option InclusiveExclusive

WALS Ch 39: incl/excl distinction in independent pronouns.

Equations

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

def Pronoun.inclusiveExclusiveVerbal (iso : String) : Option InclusiveExclusiveVerbal

WALS Ch 40: incl/excl distinction in verbal inflection.

Equations

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

def Pronoun.genderDistinction (iso : String) : Option GenderDistinction

WALS Ch 44: gender distinctions in the pronoun paradigm.

Equations

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

def Pronoun.politeness (iso : String) : Option PolitenessDistinction

WALS Ch 45: politeness distinctions in pronouns.

Equations

• Pronoun.politeness iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => Pronoun.fromWALS45A x.value) (Data.WALS.F45A.lookupISO iso)

def Pronoun.indefiniteType (iso : String) : Option IndefiniteType

WALS Ch 46: indefinite-pronoun strategy.

Equations

• Pronoun.indefiniteType iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => Pronoun.fromWALS46A x.value) (Data.WALS.F46A.lookupISO iso)

def Pronoun.intensifierReflexive (iso : String) : Option IntensifierReflexive

WALS Ch 47: intensifier–reflexive relationship.

Equations

• Pronoun.intensifierReflexive iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F47A.IntensifierReflexive) => Pronoun.fromWALS47A x.value) (Data.WALS.F47A.lookupISO iso)

def Pronoun.personMarkingAdpositions (iso : String) : Option PersonMarkingOnAdpositions

WALS Ch 48: person marking on adpositions.

Equations

• Pronoun.personMarkingAdpositions iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F48A.PersonMarkingOnAdpositions) => Pronoun.fromWALS48A x.value) (Data.WALS.F48A.lookupISO iso)

Distribution theorems

theorem Pronoun.noDistinction_is_majority_ch39 : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns) => x.value == Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.noInclusiveExclusive) Pronoun.ch39✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns) => x.value == Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.inclusiveExclusive) Pronoun.ch39✝).length

Majority of languages (120/200) make no inclusive/exclusive distinction in independent pronouns.

theorem Pronoun.noGender_is_majority_ch44 : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.noGenderDistinctions) Pronoun.ch44✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonSingularOnly) Pronoun.ch44✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonOnlyButAlsoNonSingular) Pronoun.ch44✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.in3rdPerson1stAndOr2ndPerson) Pronoun.ch44✝).length

No gender distinctions in pronouns is the majority pattern (254/378 = 67.2%).

theorem Pronoun.noPoliteness_is_majority_ch45 : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.noPolitenessDistinction) Pronoun.ch45✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.binaryPolitenessDistinction) Pronoun.ch45✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.multiplePolitenessDistinctions) Pronoun.ch45✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.pronounsAvoidedForPoliteness) Pronoun.ch45✝).length

Most languages lack politeness distinctions in pronouns (136/207 = 65.7%).

Phonological shape (WALS Chs 136–137, [nichols-peterson-2013])

inductive Pronoun.MTPattern : Type

M-T pronoun pattern (WALS Ch 136A, [nichols-peterson-2013]): whether 1SG has /m/ and 2SG has /t/, a widespread cross-linguistic pattern hypothesized to reflect deep genealogical signal.

• absent : MTPattern

  No M-T pattern in the pronoun paradigm.

• paradigmatic : MTPattern

  M-T pattern is paradigmatic (systematic across forms).

• nonParadigmatic : MTPattern

  M-T pattern is non-paradigmatic (sporadic).

@[implicit_reducible]

instance Pronoun.instDecidableEqMTPattern : DecidableEq MTPattern

Equations

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

def Pronoun.instReprMTPattern.repr : MTPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprMTPattern : Repr MTPattern

Equations

• Pronoun.instReprMTPattern = { reprPrec := Pronoun.instReprMTPattern.repr }

inductive Pronoun.MIn1SG : Type

Whether 1SG has an m-initial or m-containing form (WALS Ch 136B).

• absent : MIn1SG
• present : MIn1SG

@[implicit_reducible]

instance Pronoun.instDecidableEqMIn1SG : DecidableEq MIn1SG

Equations

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

@[implicit_reducible]

instance Pronoun.instReprMIn1SG : Repr MIn1SG

Equations

• Pronoun.instReprMIn1SG = { reprPrec := Pronoun.instReprMIn1SG.repr }

def Pronoun.instReprMIn1SG.repr : MIn1SG → ℕ → Std.Format

Equations

• Pronoun.instReprMIn1SG.repr Pronoun.MIn1SG.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.MIn1SG.absent")).group prec✝
• Pronoun.instReprMIn1SG.repr Pronoun.MIn1SG.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.MIn1SG.present")).group prec✝

inductive Pronoun.NMPattern : Type

N-M pronoun pattern (WALS Ch 137A, [nichols-peterson-2013]): whether 1SG has /n/ and 2SG has /m/.

• absent : NMPattern
• paradigmatic : NMPattern
• nonParadigmatic : NMPattern

@[implicit_reducible]

instance Pronoun.instDecidableEqNMPattern : DecidableEq NMPattern

Equations

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

def Pronoun.instReprNMPattern.repr : NMPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprNMPattern : Repr NMPattern

Equations

• Pronoun.instReprNMPattern = { reprPrec := Pronoun.instReprNMPattern.repr }

inductive Pronoun.MIn2SG : Type

Whether 2SG has an m-initial or m-containing form (WALS Ch 137B).

• absent : MIn2SG
• present : MIn2SG

@[implicit_reducible]

instance Pronoun.instDecidableEqMIn2SG : DecidableEq MIn2SG

Equations

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

def Pronoun.instReprMIn2SG.repr : MIn2SG → ℕ → Std.Format

Equations

• Pronoun.instReprMIn2SG.repr Pronoun.MIn2SG.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.MIn2SG.absent")).group prec✝
• Pronoun.instReprMIn2SG.repr Pronoun.MIn2SG.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.MIn2SG.present")).group prec✝

@[implicit_reducible]

instance Pronoun.instReprMIn2SG : Repr MIn2SG

Equations

• Pronoun.instReprMIn2SG = { reprPrec := Pronoun.instReprMIn2SG.repr }

def Pronoun.fromWALS136A : Data.WALS.F136A.MTPronouns → MTPattern

Equations

• Pronoun.fromWALS136A Data.WALS.F136A.MTPronouns.noMTPronouns = Pronoun.MTPattern.absent
• Pronoun.fromWALS136A Data.WALS.F136A.MTPronouns.mTPronounsParadigmatic = Pronoun.MTPattern.paradigmatic
• Pronoun.fromWALS136A Data.WALS.F136A.MTPronouns.mTPronounsNonParadigmatic = Pronoun.MTPattern.nonParadigmatic

def Pronoun.fromWALS136B : Data.WALS.F136B.MInFirstPersonSingular → MIn1SG

Equations

• Pronoun.fromWALS136B Data.WALS.F136B.MInFirstPersonSingular.noMInFirstPersonSingular = Pronoun.MIn1SG.absent
• Pronoun.fromWALS136B Data.WALS.F136B.MInFirstPersonSingular.mInFirstPersonSingular = Pronoun.MIn1SG.present

def Pronoun.fromWALS137A : Data.WALS.F137A.NMPronouns → NMPattern

Equations

• Pronoun.fromWALS137A Data.WALS.F137A.NMPronouns.noNMPronouns = Pronoun.NMPattern.absent
• Pronoun.fromWALS137A Data.WALS.F137A.NMPronouns.nMPronounsParadigmatic = Pronoun.NMPattern.paradigmatic
• Pronoun.fromWALS137A Data.WALS.F137A.NMPronouns.nMPronounsNonParadigmatic = Pronoun.NMPattern.nonParadigmatic

def Pronoun.fromWALS137B : Data.WALS.F137B.MInSecondPersonSingular → MIn2SG

Equations

• Pronoun.fromWALS137B Data.WALS.F137B.MInSecondPersonSingular.noMInSecondPersonSingular = Pronoun.MIn2SG.absent
• Pronoun.fromWALS137B Data.WALS.F137B.MInSecondPersonSingular.mInSecondPersonSingular = Pronoun.MIn2SG.present

Per-language pronoun-shape accessors (Chs 136–137)

def Pronoun.mtPattern (iso : String) : Option MTPattern

WALS Ch 136A: M-T pronoun pattern, for the language with ISO iso.

Equations

• Pronoun.mtPattern iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F136A.MTPronouns) => Pronoun.fromWALS136A x.value) (Data.WALS.F136A.lookupISO iso)

def Pronoun.mIn1sg (iso : String) : Option MIn1SG

WALS Ch 136B: /m/ in 1SG.

Equations

• Pronoun.mIn1sg iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F136B.MInFirstPersonSingular) => Pronoun.fromWALS136B x.value) (Data.WALS.F136B.lookupISO iso)

def Pronoun.nmPattern (iso : String) : Option NMPattern

WALS Ch 137A: N-M pronoun pattern.

Equations

• Pronoun.nmPattern iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F137A.NMPronouns) => Pronoun.fromWALS137A x.value) (Data.WALS.F137A.lookupISO iso)

def Pronoun.mIn2sg (iso : String) : Option MIn2SG

WALS Ch 137B: /m/ in 2SG.

Equations

• Pronoun.mIn2sg iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F137B.MInSecondPersonSingular) => Pronoun.fromWALS137B x.value) (Data.WALS.F137B.lookupISO iso)

structure Pronoun.MTCounts : Type

WALS Ch 136A distribution: M-T pronoun patterns ([nichols-peterson-2013], n = 230).

• absent : ℕ
• paradigmatic : ℕ
• nonParadigmatic : ℕ

def Pronoun.instReprMTCounts.repr : MTCounts → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprMTCounts : Repr MTCounts

Equations

• Pronoun.instReprMTCounts = { reprPrec := Pronoun.instReprMTCounts.repr }

def Pronoun.MTCounts.total (c : MTCounts) : ℕ

Equations

• c.total = c.absent + c.paradigmatic + c.nonParadigmatic

def Pronoun.walsMT : MTCounts

WALS Ch 136A counts (230 languages).

Equations

• Pronoun.walsMT = { absent := 200, paradigmatic := 27, nonParadigmatic := 3 }

theorem Pronoun.mt_pronouns_minority : walsMT.absent > walsMT.paradigmatic + walsMT.nonParadigmatic

The M-T pronoun pattern is a clear minority cross-linguistically: only 30/230 languages (~13%) show any form of it; 200/230 lack it entirely. Despite its visibility in Indo-European, it is not a typological default.

Clusivity bridge

def Pronoun.InclusiveExclusive.fromClusivity : Features.Clusivity.System → InclusiveExclusive

WALS Ch 39 image of a Cysouw first-person-complex type (Features.Clusivity.System): WALS Ch 39 (Cysouw's own chapter) collapses the minimal/augmented split, so the map is many-to-one — given a WALS value, the paradigm type is underdetermined.

Equations

• Pronoun.InclusiveExclusive.fromClusivity Features.Clusivity.System.noWe = Pronoun.InclusiveExclusive.noWe
• Pronoun.InclusiveExclusive.fromClusivity Features.Clusivity.System.unifiedWe = Pronoun.InclusiveExclusive.noDistinction
• Pronoun.InclusiveExclusive.fromClusivity Features.Clusivity.System.onlyInclusive = Pronoun.InclusiveExclusive.onlyInclusive
• Pronoun.InclusiveExclusive.fromClusivity Features.Clusivity.System.inclusiveExclusive = Pronoun.InclusiveExclusive.inclusiveExclusive
• Pronoun.InclusiveExclusive.fromClusivity Features.Clusivity.System.minimalAugmented = Pronoun.InclusiveExclusive.inclusiveExclusive

Pronoun plurality (WALS Ch 35)

inductive Pronoun.Plurality : Type

WALS Ch 35: how independent personal pronouns encode number. The canonical home for this pronoun-paradigm feature; Morphology.Number.PluralityProfile carries the per-language values alongside the nominal-plurality chapters (33/34/36).

• noIndependentPronouns : Plurality

  No independent subject pronouns (e.g., Acoma).

• numberIndifferent : Plurality

  Same form for sg and pl (e.g., Pirahã ti 'I/we').

• personNumberAffixes : Plurality

  Both person and number are affixal.

• personNumberStem : Plurality

  Person+number fused in stem (e.g., Dogon mi/emme).

• pnStemPronominalAffix : Plurality

  Person-number stem + pronominal plural affix.

• pnStemNominalAffix : Plurality

  Person-number stem + nominal plural affix (e.g., Russian).

• personStemPronominalAffix : Plurality

  Person stem + pronominal plural affix (e.g., Chuvash).

• personStemNominalAffix : Plurality

  Person stem + nominal plural affix (e.g., Mandarin -men).

@[implicit_reducible]

instance Pronoun.instDecidableEqPlurality : DecidableEq Plurality

Equations

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

def Pronoun.instBEqPlurality.beq : Plurality → Plurality → Bool

Equations

• Pronoun.instBEqPlurality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Pronoun.instBEqPlurality : BEq Plurality

Equations

• Pronoun.instBEqPlurality = { beq := Pronoun.instBEqPlurality.beq }

def Pronoun.instReprPlurality.repr : Plurality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instReprPlurality : Repr Plurality

Equations

• Pronoun.instReprPlurality = { reprPrec := Pronoun.instReprPlurality.repr }

def Pronoun.fromWALS35A : Data.WALS.F35A.PronounPlurality → Plurality

WALS Ch 35 raw values → the friendly Plurality labels.

Equations

• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.noIndependentSubjectPronouns = Pronoun.Plurality.noIndependentPronouns
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.numberIndifferentPronouns = Pronoun.Plurality.numberIndifferent
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.personNumberAffixes = Pronoun.Plurality.personNumberAffixes
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.personNumberStem = Pronoun.Plurality.personNumberStem
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.personNumberStemPronominalPluralAffix = Pronoun.Plurality.pnStemPronominalAffix
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.personNumberStemNominalPluralAffix = Pronoun.Plurality.pnStemNominalAffix
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.personStemPronominalPluralAffix = Pronoun.Plurality.personStemPronominalAffix
• Pronoun.fromWALS35A Data.WALS.F35A.PronounPlurality.personStemNominalPluralAffix = Pronoun.Plurality.personStemNominalAffix

theorem Pronoun.personNumberStem_is_plurality (other : Data.WALS.F35A.PronounPlurality) : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F35A.PronounPlurality) => x.value == Data.WALS.F35A.PronounPlurality.personNumberStem) Pronoun.ch35✝).length ≥ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F35A.PronounPlurality) => x.value == other) Pronoun.ch35✝).length

A fused person-number stem is the single most common pronoun-plurality strategy cross-linguistically (114/261 languages in WALS Ch 35).