Possession typology — substrate

@cite{stassen-2009} @cite{nichols-1986} @cite{nichols-bickel-2013} @cite{heine-1997} @cite{wals-2013}

Per-language possession-typology substrate for Fragment import. Mirrors the Linglib/Typology/{Domain}.lean pattern (Case, Phonology, WordOrder).

Substrate enums

• ObligatoryPossession (WALS Ch 58A)
• PossessiveClassification (WALS Ch 59A)
• PredicativePossession (@cite{stassen-2009}): 5-way strategy typology
• AdnominalPossession (@cite{nichols-1986}): head/dep/double/juxtaposition
• PossessiveAffixPosition (WALS Ch 57A)
• NumberOfPossessiveNouns (WALS Ch 58B)
• PossessiveNotion (@cite{heine-1997} §2.3): 7-way semantic targets
• InalienabilityRank: hierarchy of inalienability candidates
• PossessionSource (@cite{heine-1997} Table 2.1): 8 grammaticalization schemas
• PossessionProfile: bundle struct + 6 helper predicates

Theory-laden caveats

Several substrate enums encode specific frameworks, not theory-neutral consensus, despite the file's substrate role:

• PredicativePossession is Stassen 2009's 5-way typology, not field consensus. Heine 1997 splits Genitive/Dative differently (Goal vs Genitive as separable schemas); Creissels (2013, 2019) challenges the Companion vs Locational boundary. WALS Ch 117A (Stassen 2013) endorses these 5 categories — defensible substrate, but not framework-neutral.

• PossessiveClassification (3-way) hides substantial language-internal variation. Chappell & McGregor 1996, Stolz et al. 2008, Aikhenvald & Dixon 2013 argue alienability is a continuum interacting with possessor animacy and possessum semantics. Mayan 3-class systems and Hawaiian a/o-class systems both code as threeOrMore with analytical loss. Future work: a PossessiveSplit substrate indexed by (PossessorClass × PossessumClass) for fine-grained Oceanic / Mayan / Daakaka systems.

• PossessionSource (Heine 1997 8-way) and PredicativePossession (Stassen) coexist as parallel typologies over the same data; predicativeSource is the bridge. This is the right pattern for parallel substrates (cf. Causation's Song-vs-Pylkkänen architecture).

WALS aggregates

WALS chapter aggregate distributions (ch58_distribution, ch59_no_classification_plurality_wals, etc.) live in this file at the substrate layer per the project's "WALS goes to Linglib/Typology/" rule, since they are theory-neutral facts about WALS data, not paper-specific contributions. Cross-linguistic theorems consuming Fragment per-language data live in Phenomena/Possession/Studies/NicholsBickel2013.lean.

inductive Typology.Possession.ObligatoryPossession : Type

WALS Ch 58A: whether some nouns (typically kinship, body parts) require obligatory possessive marking. Unpossessed forms are either ungrammatical or require special "absolute" morphology.

• exists_ : ObligatoryPossession

  Obligatory possessive inflection exists (e.g., Mohawk, Turkish, Hungarian, Navajo).

• noObligatory : ObligatoryPossession

  No obligatory possessive inflection (e.g., English, Mandarin, Russian, Finnish).

• unclear : ObligatoryPossession

  Possessive inflection exists but is never obligatory; data insufficient.

@[implicit_reducible]

instance Typology.Possession.instDecidableEqObligatoryPossession : DecidableEq ObligatoryPossession

Equations

• Typology.Possession.instDecidableEqObligatoryPossession x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Possession.instReprObligatoryPossession : Repr ObligatoryPossession

Equations

• Typology.Possession.instReprObligatoryPossession = { reprPrec := Typology.Possession.instReprObligatoryPossession.repr }

def Typology.Possession.instReprObligatoryPossession.repr : ObligatoryPossession → Nat → Std.Format

Equations

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

inductive Typology.Possession.PossessiveClassification : Type

WALS Ch 59A: whether the language morphosyntactically distinguishes different classes of possession (typically alienable vs inalienable).

• noClassification : PossessiveClassification

  All nouns use the same possessive construction (e.g., English, Russian, Turkish).

• twoWay : PossessiveClassification

  Two-way classification, typically alienable vs inalienable (e.g., Fijian, Hawaiian, many Oceanic and Amazonian languages).

• threeOrMore : PossessiveClassification

  Three or more classes of possession distinguished.

@[implicit_reducible]

instance Typology.Possession.instDecidableEqPossessiveClassification : DecidableEq PossessiveClassification

Equations

• Typology.Possession.instDecidableEqPossessiveClassification x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Possession.instReprPossessiveClassification : Repr PossessiveClassification

Equations

• Typology.Possession.instReprPossessiveClassification = { reprPrec := Typology.Possession.instReprPossessiveClassification.repr }

def Typology.Possession.instReprPossessiveClassification.repr : PossessiveClassification → Nat → Std.Format

Equations

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

inductive Typology.Possession.PredicativePossession : Type

@cite{stassen-2009}: how a language expresses predicative (clausal) possession ("I have X"). The four major strategies correspond to different syntactic analyses of the possessor.

• haveVerb : PredicativePossession

  Have-verb: dedicated transitive verb 'have' (e.g., English I have a book, Mandarin wo you yi-ben shu).

• locational : PredicativePossession

  Locational/Existential: existential construction with possessor in a locative/oblique case (e.g., Russian u menja est' kniga, Finnish minulla on kirja).

• genitiveDative : PredicativePossession

  Genitive/Dative predicate: possessor in genitive or dative with copula (e.g., Hindi mere paas kitaab hai, Irish ta leabhar agam, Arabic indi kitaab).

• topic : PredicativePossession

  Topic-comment: possessor topicalized, possessum in existential comment (e.g., Japanese watashi-ni-wa hon-ga aru).

• comitative : PredicativePossession

  Conjunctional/Comitative: "I am with a book" (e.g., Bantu Swahili nina kitabu 'I-with book').

@[implicit_reducible]

instance Typology.Possession.instDecidableEqPredicativePossession : DecidableEq PredicativePossession

Equations

• Typology.Possession.instDecidableEqPredicativePossession x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Possession.instReprPredicativePossession : Repr PredicativePossession

Equations

• Typology.Possession.instReprPredicativePossession = { reprPrec := Typology.Possession.instReprPredicativePossession.repr }

def Typology.Possession.instReprPredicativePossession.repr : PredicativePossession → Nat → Std.Format

Equations

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

inductive Typology.Possession.AdnominalPossession : Type

@cite{nichols-1986}: how the possessive relation is marked within the NP ("my book", "John's house").

• headMarking : AdnominalPossession

  Head-marking: possessive marker on the possessed noun (head) (e.g., Hungarian Janos kalap-ja, Swahili kitabu ch-ake).

• dependentMarking : AdnominalPossession

  Dependent-marking: possessive marker on the possessor (e.g., English John's book, Japanese Tanaka-no hon).

• doubleMarking : AdnominalPossession

  Double-marking: both possessor and possessed noun marked (e.g., Turkish Ali-nin kitab-i, Georgian kac-is saxl-i).

• juxtaposition : AdnominalPossession

  Juxtaposition: no overt marker; word-order only (e.g., Vietnamese nha toi 'house I' = 'my house').

@[implicit_reducible]

instance Typology.Possession.instDecidableEqAdnominalPossession : DecidableEq AdnominalPossession

Equations

• Typology.Possession.instDecidableEqAdnominalPossession x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Possession.instReprAdnominalPossession : Repr AdnominalPossession

Equations

• Typology.Possession.instReprAdnominalPossession = { reprPrec := Typology.Possession.instReprAdnominalPossession.repr }

def Typology.Possession.instReprAdnominalPossession.repr : AdnominalPossession → Nat → Std.Format

Equations

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

inductive Typology.Possession.PossessiveAffixPosition : Type

WALS Ch 57A: position of pronominal possessive affixes on the noun.

• prefixes : PossessiveAffixPosition

  Possessive prefixes (e.g., Swahili class-agreement prefixes, many Bantu/Papuan).

• suffixes : PossessiveAffixPosition

  Possessive suffixes (e.g., Turkish -im, Hungarian -m, Finnish -ni).

• both : PossessiveAffixPosition

  Both prefixes and suffixes used.

• none : PossessiveAffixPosition

  No possessive affixes; possession marked by independent words/clitics (e.g., English my, Japanese no, Mandarin de).

@[implicit_reducible]

instance Typology.Possession.instDecidableEqPossessiveAffixPosition : DecidableEq PossessiveAffixPosition

Equations

• Typology.Possession.instDecidableEqPossessiveAffixPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Possession.instReprPossessiveAffixPosition.repr : PossessiveAffixPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Possession.instReprPossessiveAffixPosition : Repr PossessiveAffixPosition

Equations

• Typology.Possession.instReprPossessiveAffixPosition = { reprPrec := Typology.Possession.instReprPossessiveAffixPosition.repr }

inductive Typology.Possession.NumberOfPossessiveNouns : Type

WALS Ch 58B: how many nouns in the language function as possessive markers (e.g., English "property" used as a possessive classifier).

• noneReported : NumberOfPossessiveNouns

  No possessive nouns reported.

• one : NumberOfPossessiveNouns

  Exactly one possessive noun.

• twoToFour : NumberOfPossessiveNouns

  Two to four possessive nouns.

• fiveOrMore : NumberOfPossessiveNouns

  Five or more possessive nouns.

@[implicit_reducible]

instance Typology.Possession.instDecidableEqNumberOfPossessiveNouns : DecidableEq NumberOfPossessiveNouns

Equations

• Typology.Possession.instDecidableEqNumberOfPossessiveNouns x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Possession.instReprNumberOfPossessiveNouns : Repr NumberOfPossessiveNouns

Equations

• Typology.Possession.instReprNumberOfPossessiveNouns = { reprPrec := Typology.Possession.instReprNumberOfPossessiveNouns.repr }

def Typology.Possession.instReprNumberOfPossessiveNouns.repr : NumberOfPossessiveNouns → Nat → Std.Format

Equations

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

inductive Typology.Possession.PossessiveNotion : Type

@cite{heine-1997} §2.3: the semantic targets of possessive constructions — what kind of possessive relationship is expressed. Distinct from PossessionSource, which encodes the cognitive source (how the construction arose diachronically). Seven notions ordered by increasing abstractness: physical < temporary < permanent < inalienable < abstract (plus two for inanimate possessors).

• physical : PossessiveNotion

  Physical possession (e.g., "I have a pen in my hand").

• temporary : PossessiveNotion

  Temporary possession (e.g., "I have a rental car").

• permanent : PossessiveNotion

  Permanent possession (e.g., "I have a house").

• inalienable : PossessiveNotion

  Inalienable possession (e.g., "I have two sisters", "blue eyes").

• abstract : PossessiveNotion

  Abstract possession (e.g., "I have a headache", "an idea").

• inanimateInalienable : PossessiveNotion

  Inanimate inalienable (e.g., "The tree has branches").

• inanimateAlienable : PossessiveNotion

  Inanimate alienable (e.g., "The room has a window").

@[implicit_reducible]

instance Typology.Possession.instDecidableEqPossessiveNotion : DecidableEq PossessiveNotion

Equations

• Typology.Possession.instDecidableEqPossessiveNotion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Possession.instReprPossessiveNotion.repr : PossessiveNotion → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Possession.instReprPossessiveNotion : Repr PossessiveNotion

Equations

• Typology.Possession.instReprPossessiveNotion = { reprPrec := Typology.Possession.instReprPossessiveNotion.repr }

def Typology.Possession.PossessiveNotion.abstractness : PossessiveNotion → Nat

Abstractness ordering: higher = more abstract possessive notion.

Equations

• Typology.Possession.PossessiveNotion.physical.abstractness = 0
• Typology.Possession.PossessiveNotion.temporary.abstractness = 1
• Typology.Possession.PossessiveNotion.permanent.abstractness = 2
• Typology.Possession.PossessiveNotion.inalienable.abstractness = 3
• Typology.Possession.PossessiveNotion.abstract.abstractness = 4
• Typology.Possession.PossessiveNotion.inanimateInalienable.abstractness = 5
• Typology.Possession.PossessiveNotion.inanimateAlienable.abstractness = 6

inductive Typology.Possession.InalienabilityRank : Type

The inalienability hierarchy: if a language draws an alienable/inalienable boundary, the inalienable class is drawn from the top. Body parts and kinship terms are always the first candidates.

• bodyPart : InalienabilityRank
• kinship : InalienabilityRank
• spatialRelation : InalienabilityRank
• partWhole : InalienabilityRank
• culturalItem : InalienabilityRank
• generalProperty : InalienabilityRank

@[implicit_reducible]

instance Typology.Possession.instDecidableEqInalienabilityRank : DecidableEq InalienabilityRank

Equations

• Typology.Possession.instDecidableEqInalienabilityRank x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Possession.instReprInalienabilityRank.repr : InalienabilityRank → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Possession.instReprInalienabilityRank : Repr InalienabilityRank

Equations

• Typology.Possession.instReprInalienabilityRank = { reprPrec := Typology.Possession.instReprInalienabilityRank.repr }

def Typology.Possession.InalienabilityRank.toNat : InalienabilityRank → Nat

Numeric rank for comparison (higher = more likely to be inalienable).

Equations

• Typology.Possession.InalienabilityRank.bodyPart.toNat = 5
• Typology.Possession.InalienabilityRank.kinship.toNat = 4
• Typology.Possession.InalienabilityRank.spatialRelation.toNat = 3
• Typology.Possession.InalienabilityRank.partWhole.toNat = 2
• Typology.Possession.InalienabilityRank.culturalItem.toNat = 1
• Typology.Possession.InalienabilityRank.generalProperty.toNat = 0

inductive Typology.Possession.PossessionSource : Type

@cite{heine-1997} Table 2.1 / @cite{heine-2009} Table 29.5: eight diachronic source schemas from which predicative possession constructions arise via grammaticalization.

• action : PossessionSource

  Action: "X takes Y" → 'X has Y' (e.g., English have < OE habban).

• location : PossessionSource

  Location: "Y is at X" → 'X has Y' (e.g., Finnish adessive, Russian u).

• companion : PossessionSource

  Companion: "X is with Y" → 'X has Y' (e.g., Swahili -na, Venda na).

• genitive : PossessionSource

  Genitive: "X's Y exists" → 'X has Y' (e.g., Turkish Hasan-ın inek-i var).

• goal : PossessionSource

  Goal: "Y exists for X" → 'X has Y' (e.g., Hindi mere paas, Irish agam).

• source : PossessionSource

  Source: "Y exists from X" → 'X has Y'.

• topic : PossessionSource

  Topic: "As for X, Y exists" → 'X has Y' (e.g., Japanese watashi-ni-wa).

• equation : PossessionSource

  Equation: "Y is X's" → 'X has Y' (e.g., Scots Gaelic is leam an leabhar).

@[implicit_reducible]

instance Typology.Possession.instDecidableEqPossessionSource : DecidableEq PossessionSource

Equations

• Typology.Possession.instDecidableEqPossessionSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Possession.instReprPossessionSource : Repr PossessionSource

Equations

• Typology.Possession.instReprPossessionSource = { reprPrec := Typology.Possession.instReprPossessionSource.repr }

def Typology.Possession.instReprPossessionSource.repr : PossessionSource → Nat → Std.Format

Equations

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

def Typology.Possession.predicativeSource : PredicativePossession → PossessionSource

Map predicative strategies to their likely grammaticalization source.

Equations

• Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.haveVerb = Typology.Possession.PossessionSource.action
• Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.locational = Typology.Possession.PossessionSource.location
• Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.genitiveDative = Typology.Possession.PossessionSource.goal
• Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.topic = Typology.Possession.PossessionSource.topic
• Typology.Possession.predicativeSource Typology.Possession.PredicativePossession.comitative = Typology.Possession.PossessionSource.companion

structure Typology.Possession.PossessionProfile : Type

A language's possession profile across @cite{wals-2013} chapters 57–59 and the additional typological dimensions of predicative (@cite{stassen-2009}) and adnominal (@cite{nichols-1986}) possession.

• language : String

  Language name (matches LanguageProfile.name when bundled).

• family : String

  Language family.

• iso : String

  ISO 639-3 code (matches LanguageProfile.iso when bundled).

• obligatoryPossession : ObligatoryPossession

  Ch 58: whether obligatory possessive inflection exists.

• possessiveClassification : PossessiveClassification

  Ch 59: whether the language morphosyntactically classifies possession.

• predicativeStrategy : PredicativePossession

  Primary strategy for predicative possession ("I have X").

• adnominalStrategy : AdnominalPossession

  Primary strategy for adnominal possession ("my book").

• affixPosition : Option PossessiveAffixPosition

  Ch 57: position of pronominal possessive affixes, if attested.

• examples : List String

  Illustrative possessive forms or constructions.

• notes : String

  Notes on the possession system.

@[implicit_reducible]

instance Typology.Possession.instReprPossessionProfile : Repr PossessionProfile

Equations

• Typology.Possession.instReprPossessionProfile = { reprPrec := Typology.Possession.instReprPossessionProfile.repr }

def Typology.Possession.instReprPossessionProfile.repr : PossessionProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Possession.instDecidableEqPossessionProfile : DecidableEq PossessionProfile

Equations

• Typology.Possession.instDecidableEqPossessionProfile = Typology.Possession.instDecidableEqPossessionProfile.decEq

def Typology.Possession.instDecidableEqPossessionProfile.decEq (x✝ x✝¹ : PossessionProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Typology.Possession.PossessionProfile.hasObligatoryPossession (p : PossessionProfile) : Bool

Does a language have obligatory possessive inflection?

Equations

• p.hasObligatoryPossession = (p.obligatoryPossession == Typology.Possession.ObligatoryPossession.exists_)

def Typology.Possession.PossessionProfile.hasClassification (p : PossessionProfile) : Bool

Does a language morphosyntactically classify possession?

Equations

• p.hasClassification = (p.possessiveClassification != Typology.Possession.PossessiveClassification.noClassification)

def Typology.Possession.PossessionProfile.usesHaveVerb (p : PossessionProfile) : Bool

Does a language use a have-verb strategy?

Equations

• p.usesHaveVerb = (p.predicativeStrategy == Typology.Possession.PredicativePossession.haveVerb)

def Typology.Possession.PossessionProfile.usesLocational (p : PossessionProfile) : Bool

Does a language use a locational/existential strategy?

Equations

• p.usesLocational = (p.predicativeStrategy == Typology.Possession.PredicativePossession.locational)

def Typology.Possession.PossessionProfile.isHeadMarking (p : PossessionProfile) : Bool

Does a language use head-marking for adnominal possession?

Equations

• p.isHeadMarking = (p.adnominalStrategy == Typology.Possession.AdnominalPossession.headMarking)

def Typology.Possession.PossessionProfile.isDependentMarking (p : PossessionProfile) : Bool

Does a language use dependent-marking for adnominal possession?

Equations

• p.isDependentMarking = (p.adnominalStrategy == Typology.Possession.AdnominalPossession.dependentMarking)

def Typology.Possession.fromWALS57A : Data.WALS.F57A.PositionOfPronominalPossessiveAffixes → PossessiveAffixPosition

WALS Ch 57A → PossessiveAffixPosition.

Equations

• Typology.Possession.fromWALS57A Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.possessivePrefixes = Typology.Possession.PossessiveAffixPosition.prefixes
• Typology.Possession.fromWALS57A Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.possessiveSuffixes = Typology.Possession.PossessiveAffixPosition.suffixes
• Typology.Possession.fromWALS57A Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.prefixesAndSuffixes = Typology.Possession.PossessiveAffixPosition.both
• Typology.Possession.fromWALS57A Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.noPossessiveAffixes = Typology.Possession.PossessiveAffixPosition.none

def Typology.Possession.fromWALS58A : Data.WALS.F58A.ObligatoryPossessiveInflection → ObligatoryPossession

WALS Ch 58A → ObligatoryPossession. WALS only encodes exists/absent; our substrate adds .unclear for languages with optional/disputed coding.

Equations

• Typology.Possession.fromWALS58A Data.WALS.F58A.ObligatoryPossessiveInflection.exists = Typology.Possession.ObligatoryPossession.exists_
• Typology.Possession.fromWALS58A Data.WALS.F58A.ObligatoryPossessiveInflection.absent = Typology.Possession.ObligatoryPossession.noObligatory

def Typology.Possession.fromWALS58B : Data.WALS.F58B.NumberOfPossessiveNouns → NumberOfPossessiveNouns

WALS Ch 58B → NumberOfPossessiveNouns.

Equations

• Typology.Possession.fromWALS58B Data.WALS.F58B.NumberOfPossessiveNouns.noneReported = Typology.Possession.NumberOfPossessiveNouns.noneReported
• Typology.Possession.fromWALS58B Data.WALS.F58B.NumberOfPossessiveNouns.one = Typology.Possession.NumberOfPossessiveNouns.one
• Typology.Possession.fromWALS58B Data.WALS.F58B.NumberOfPossessiveNouns.twoToFour = Typology.Possession.NumberOfPossessiveNouns.twoToFour
• Typology.Possession.fromWALS58B Data.WALS.F58B.NumberOfPossessiveNouns.fiveOrMore = Typology.Possession.NumberOfPossessiveNouns.fiveOrMore

def Typology.Possession.fromWALS59A : Data.WALS.F59A.PossessiveClassification → PossessiveClassification

WALS Ch 59A → PossessiveClassification. WALS distinguishes "3–5 classes" from "more than 5"; we collapse both into .threeOrMore.

Equations

• Typology.Possession.fromWALS59A Data.WALS.F59A.PossessiveClassification.noPossessiveClassification = Typology.Possession.PossessiveClassification.noClassification
• Typology.Possession.fromWALS59A Data.WALS.F59A.PossessiveClassification.twoClasses = Typology.Possession.PossessiveClassification.twoWay
• Typology.Possession.fromWALS59A Data.WALS.F59A.PossessiveClassification.threeToFiveClasses = Typology.Possession.PossessiveClassification.threeOrMore
• Typology.Possession.fromWALS59A Data.WALS.F59A.PossessiveClassification.moreThanFiveClasses = Typology.Possession.PossessiveClassification.threeOrMore

WALSCount + WALSCount.totalOf are imported from Linglib/Data/WALS/Aggregation.lean (shared with the other Typology files that consume WALS distributions).

def Typology.Possession.ch58Counts : List Data.WALS.WALSCount

Ch 58 distribution: obligatory possessive inflection (N = 244).

Equations

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

def Typology.Possession.ch59Counts : List Data.WALS.WALSCount

Ch 59 distribution: possessive classification (N = 243). WALS distinguishes "3–5" from "more than 5"; we collapse both into "Three or more classes".

Equations

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

def Typology.Possession.ch58bCounts : List Data.WALS.WALSCount

Ch 58B distribution: number of possessive nouns (N = 243).

Equations

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

theorem Typology.Possession.ch58_ch59_sample_diff : Data.WALS.WALSCount.totalOf ch58Counts = Data.WALS.WALSCount.totalOf ch59Counts + 1

Ch 58 has one more language than Ch 59 (244 vs 243; Panare is in 58 but not 59).

theorem Typology.Possession.ch57_distribution : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F57A.PositionOfPronominalPossessiveAffixes) => x.value == Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.possessivePrefixes) Typology.Possession.ch57✝).length = 255 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F57A.PositionOfPronominalPossessiveAffixes) => x.value == Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.possessiveSuffixes) Typology.Possession.ch57✝).length = 355 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F57A.PositionOfPronominalPossessiveAffixes) => x.value == Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.prefixesAndSuffixes) Typology.Possession.ch57✝).length = 32 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F57A.PositionOfPronominalPossessiveAffixes) => x.value == Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.noPossessiveAffixes) Typology.Possession.ch57✝).length = 260

Ch 57 value distribution from WALS data.

theorem Typology.Possession.ch58_distribution : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Data.WALS.F58A.ObligatoryPossessiveInflection.exists) Typology.Possession.ch58✝).length = 43 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Data.WALS.F58A.ObligatoryPossessiveInflection.absent) Typology.Possession.ch58✝).length = 201

Ch 58 value distribution from WALS data.

theorem Typology.Possession.ch59_distribution : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F59A.PossessiveClassification) => x.value == Data.WALS.F59A.PossessiveClassification.noPossessiveClassification) Typology.Possession.ch59✝).length = 125 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F59A.PossessiveClassification) => x.value == Data.WALS.F59A.PossessiveClassification.twoClasses) Typology.Possession.ch59✝).length = 94 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F59A.PossessiveClassification) => x.value == Data.WALS.F59A.PossessiveClassification.threeToFiveClasses) Typology.Possession.ch59✝).length = 20 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F59A.PossessiveClassification) => x.value == Data.WALS.F59A.PossessiveClassification.moreThanFiveClasses) Typology.Possession.ch59✝).length = 4

Ch 59 value distribution from WALS data.

theorem Typology.Possession.ch58b_distribution : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.noneReported) Typology.Possession.ch58b✝).length = 233 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.one) Typology.Possession.ch58b✝).length = 3 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.twoToFour) Typology.Possession.ch58b✝).length = 4 ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.fiveOrMore) Typology.Possession.ch58b✝).length = 3

Ch 58B value distribution from WALS data.

theorem Typology.Possession.ch58b_none_reported_dominant : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.noneReported) Typology.Possession.ch58b✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.one) Typology.Possession.ch58b✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.twoToFour) Typology.Possession.ch58b✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58B.NumberOfPossessiveNouns) => x.value == Data.WALS.F58B.NumberOfPossessiveNouns.fiveOrMore) Typology.Possession.ch58b✝).length

Ch 58B: vast majority of languages have no possessive nouns (233/243).

theorem Typology.Possession.ch57_suffixes_most_common : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F57A.PositionOfPronominalPossessiveAffixes) => x.value == Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.possessiveSuffixes) Typology.Possession.ch57✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F57A.PositionOfPronominalPossessiveAffixes) => x.value == Data.WALS.F57A.PositionOfPronominalPossessiveAffixes.possessivePrefixes) Typology.Possession.ch57✝).length

Ch 57: possessive suffixes are the most common affix position.

theorem Typology.Possession.ch58_no_obligatory_majority_wals : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Data.WALS.F58A.ObligatoryPossessiveInflection.absent) Typology.Possession.ch58✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Data.WALS.F58A.ObligatoryPossessiveInflection.exists) Typology.Possession.ch58✝).length * 4

Ch 58: languages without obligatory possession vastly outnumber those with it in WALS data (201 vs 43, > 4×).

theorem Typology.Possession.ch59_no_classification_plurality_wals : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F59A.PossessiveClassification) => x.value == Data.WALS.F59A.PossessiveClassification.noPossessiveClassification) Typology.Possession.ch59✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F59A.PossessiveClassification) => x.value == Data.WALS.F59A.PossessiveClassification.twoClasses) Typology.Possession.ch59✝).length

Ch 59: no-possessive-classification is the most common pattern (125/243), followed by two-way (94/243).