Cross-Linguistic Typology of Possession (WALS Chapters 57--59)

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

Typological data on possessive constructions across languages, drawn from two WALS chapters by @cite{nichols-bickel-2013} and supplemented with data on predicative possession strategies and adnominal possession marking.

Ch 58: Obligatory Possessive Inflection

Whether certain nouns --- typically kinship terms and body-part nouns --- obligatorily take a possessive marker even when no specific possessor is expressed. In languages with obligatory possession, an unpossessed form of 'hand' or 'mother' is either ungrammatical or requires special morphology (an "absolute" or "free" form). This phenomenon reflects a deep semantic distinction: relational nouns (inherently requiring a relatum) are grammatically differentiated from non-relational nouns.

Sample: 244 languages. Obligatory possessive inflection exists in about one-sixth of languages sampled (43/244).

Ch 59: Possessive Classification

Whether the language distinguishes different types or classes of possession in its morphosyntax. The classic case is the alienable/inalienable distinction: inalienably possessed nouns (body parts, kinship) use one possessive construction, while alienably possessed nouns (acquired property) use a different one. Some languages make three-way or finer-grained distinctions (e.g., separating kinship from body parts, or distinguishing edible from non-edible possessions).

Sample: 243 languages. No possessive classification is the most common pattern (125/243), followed by two-way classification (94/243).

Predicative Possession

How languages express clausal possession ("I have a book"). This is a major typological parameter with four primary strategies:

1. Have-verb: A dedicated transitive verb 'have' takes possessor as subject and possessum as object (English, Mandarin, Turkish).
2. Locational/Existential: Possession expressed via an existential construction with the possessor in a locative or dative case (Russian u menja est', Finnish minulla on).
3. Genitive/Dative predicate: A copular construction where the possessor appears in genitive or dative case (Hindi mere paas, Irish ag).
4. Topic: A topic-comment construction where the possessor is topicalized and an existential predicate asserts the possessum's existence (Japanese, some Oceanic languages).

These strategies are areally clustered: have-verbs dominate in Western Europe and parts of Africa; locational strategies are widespread in Eurasia (the "Uralic-to-Japonic belt"); genitive/dative predicates appear in South Asian, Celtic, and Semitic languages.

Adnominal Possession

How languages mark possession within noun phrases ("my book", "John's house"). Three major strategies:

1. Head-marking: The possessive marker appears on the possessed noun (e.g., Hungarian Janos kalap-ja 'John hat-POSS.3SG').
2. Dependent-marking: The possessive marker appears on the possessor (e.g., English John's book, Japanese Tanaka-no hon).
3. Juxtaposition: No overt possessive marking; possessor and possessum are simply juxtaposed (e.g., Vietnamese nha toi 'house I').

These strategies correlate with broader head-vs-dependent marking typology.

inductive Phenomena.Possession.Typology.ObligatoryPossession : Type

WALS Ch 58: Whether certain nouns obligatorily take possessive inflection.

In languages with obligatory possession, relational nouns (kinship terms, body-part nouns) must be inflected for a possessor. An "unpossessed" or "absolute" form either does not exist or requires special morphology.

For example, in Mohawk, body-part nouns cannot appear without a possessive prefix: o-hsir-a 'one's leg' requires the prefix o-. The absolute form a-hsir-a uses a special neuter prefix.

• exists_ : ObligatoryPossession

  Obligatory possessive inflection exists: some nouns (typically kinship, body parts) must take possessive marking. Unpossessed forms are either ungrammatical or require special "absolute" morphology. (e.g., Mohawk, Turkish, Hungarian, Navajo)

• noObligatory : ObligatoryPossession

  No obligatory possessive inflection: all nouns can appear without possessive marking. The possessive construction is always optional. (e.g., English, Mandarin, Russian, Finnish)

• unclear : ObligatoryPossession

  Possessive inflection exists but is never obligatory; data insufficient to determine if any nouns require it.

instance Phenomena.Possession.Typology.instDecidableEqObligatoryPossession : DecidableEq ObligatoryPossession

Equations

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

def Phenomena.Possession.Typology.instBEqObligatoryPossession.beq : ObligatoryPossession → ObligatoryPossession → Bool

Equations

• Phenomena.Possession.Typology.instBEqObligatoryPossession.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instBEqObligatoryPossession : BEq ObligatoryPossession

Equations

• Phenomena.Possession.Typology.instBEqObligatoryPossession = { beq := Phenomena.Possession.Typology.instBEqObligatoryPossession.beq }

instance Phenomena.Possession.Typology.instReprObligatoryPossession : Repr ObligatoryPossession

Equations

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

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

Equations

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

inductive Phenomena.Possession.Typology.PossessiveClassification : Type

WALS Ch 59: Whether the language morphosyntactically distinguishes different classes of possession.

The prototypical case is the alienable/inalienable distinction, where inalienably possessed nouns (body parts, kinship terms) use a different possessive construction from alienably possessed nouns (acquired property). Some languages make finer-grained distinctions (e.g., kinship vs body parts vs edible items vs general property).

• noClassification : PossessiveClassification

  No possessive classification: all nouns use the same possessive construction regardless of semantic class. (e.g., English, Russian, Turkish, Japanese)

• 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. (e.g., some Papuan and Austronesian languages distinguish kinship, body parts, edible items, and general property)

instance Phenomena.Possession.Typology.instDecidableEqPossessiveClassification : DecidableEq PossessiveClassification

Equations

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

instance Phenomena.Possession.Typology.instBEqPossessiveClassification : BEq PossessiveClassification

Equations

• Phenomena.Possession.Typology.instBEqPossessiveClassification = { beq := Phenomena.Possession.Typology.instBEqPossessiveClassification.beq }

def Phenomena.Possession.Typology.instBEqPossessiveClassification.beq : PossessiveClassification → PossessiveClassification → Bool

Equations

• Phenomena.Possession.Typology.instBEqPossessiveClassification.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instReprPossessiveClassification : Repr PossessiveClassification

Equations

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

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

Equations

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

inductive Phenomena.Possession.Typology.PredicativePossession : Type

How a language expresses predicative (clausal) possession: "I have X".

The four major strategies identified by @cite{stassen-2009} correspond to different syntactic analyses of the possessor:

• Have-verb: possessor is syntactic subject of a transitive verb
• Locational: possessor is a locative/oblique argument of an existential
• Genitive/Dative: possessor is a genitive/dative argument of a copula
• Topic: possessor is a topic with an existential comment clause

• haveVerb : PredicativePossession

  Have-verb strategy: a dedicated transitive verb 'have' takes the possessor as subject and the possessum as object. (e.g., English I have a book, Mandarin wo you yi-ben shu, Turkish bir kitab-im var -- though Turkish is borderline)

• locational : PredicativePossession

  Locational/Existential strategy: possession encoded via an existential construction with the possessor in a locative, adessive, or oblique case. The possessum is the grammatical subject. (e.g., Russian u menja est' kniga 'at me exists book', Finnish minulla on kirja 'at-me is book')

• genitiveDative : PredicativePossession

  Genitive/Dative predicate: possessor appears in genitive or dative case with a copular predicate. The possessum is typically the grammatical subject. (e.g., Hindi mere paas kitaab hai 'my near book is', Irish ta leabhar agam 'is book at-me', Arabic indi kitaab 'at-me book')

• topic : PredicativePossession

  Topic-comment strategy: the possessor is topicalized and the possessum is asserted to exist in the comment clause. (e.g., Japanese watashi-ni-wa hon-ga aru 'I-DAT-TOP book-NOM exists', some Oceanic languages)

• comitative : PredicativePossession

  Conjunctional/Comitative strategy: possession expressed via a conjunction or comitative construction ("I am with a book"). (e.g., some Bantu languages: Swahili nina kitabu 'I-with book')

instance Phenomena.Possession.Typology.instDecidableEqPredicativePossession : DecidableEq PredicativePossession

Equations

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

def Phenomena.Possession.Typology.instBEqPredicativePossession.beq : PredicativePossession → PredicativePossession → Bool

Equations

• Phenomena.Possession.Typology.instBEqPredicativePossession.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instBEqPredicativePossession : BEq PredicativePossession

Equations

• Phenomena.Possession.Typology.instBEqPredicativePossession = { beq := Phenomena.Possession.Typology.instBEqPredicativePossession.beq }

instance Phenomena.Possession.Typology.instReprPredicativePossession : Repr PredicativePossession

Equations

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

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

Equations

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

inductive Phenomena.Possession.Typology.AdnominalPossession : Type

How the possessive relationship is marked within a noun phrase ("my book", "John's house").

@cite{nichols-1986} classifies languages by where the possessive morphology appears: on the possessed noun (head-marking), on the possessor (dependent-marking), on both (double-marking), or on neither (juxtaposition).

• headMarking : AdnominalPossession

  Head-marking: possessive marker appears on the possessed noun (head). (e.g., Hungarian Janos kalap-ja 'John hat-POSS.3SG', Swahili kitabu ch-ake 'book CL-POSS.3SG', Mohawk possessive prefixes)

• dependentMarking : AdnominalPossession

  Dependent-marking: possessive marker appears on the possessor (dependent). (e.g., English John's book, Japanese Tanaka-no hon 'Tanaka-GEN book', Turkish Ali-nin kitab-i -- though Turkish also marks the head)

• doubleMarking : AdnominalPossession

  Double-marking: both possessor and possessed noun are marked. (e.g., Turkish Ali-nin kitab-i 'Ali-GEN book-POSS.3SG', Georgian kac-is saxl-i 'man-GEN house-NOM', Quechua Hwan-pa wasi-n 'John-GEN house-POSS.3')

• juxtaposition : AdnominalPossession

  Juxtaposition: no overt possessive marker; possessor and possessum are simply juxtaposed, relying on word order. (e.g., Vietnamese nha toi 'house I' = 'my house', Mandarin construct-state juxtaposition in some cases)

instance Phenomena.Possession.Typology.instDecidableEqAdnominalPossession : DecidableEq AdnominalPossession

Equations

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

def Phenomena.Possession.Typology.instBEqAdnominalPossession.beq : AdnominalPossession → AdnominalPossession → Bool

Equations

• Phenomena.Possession.Typology.instBEqAdnominalPossession.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instBEqAdnominalPossession : BEq AdnominalPossession

Equations

• Phenomena.Possession.Typology.instBEqAdnominalPossession = { beq := Phenomena.Possession.Typology.instBEqAdnominalPossession.beq }

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

Equations

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

instance Phenomena.Possession.Typology.instReprAdnominalPossession : Repr AdnominalPossession

Equations

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

inductive Phenomena.Possession.Typology.PossessiveAffixPosition : Type

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

Whether a language uses prefixes, suffixes, both, or no affixes to mark pronominal possession on the possessed noun. This feature cross-cuts the head-marking vs dependent-marking distinction: a language can use possessive affixes on the head (head-marking) while also having a genitive case on the dependent (double-marking).

• prefixes : PossessiveAffixPosition

  Possessive prefixes on the possessed noun. (e.g., Swahili class-agreement prefixes, many Bantu and Papuan languages)

• suffixes : PossessiveAffixPosition

  Possessive suffixes on the possessed noun. (e.g., Turkish -im, -in, -i; Hungarian -m, -d, -ja; Finnish -ni, -si)

• both : PossessiveAffixPosition

  Both prefixes and suffixes used for possessive marking. (e.g., some languages use prefixes for one person and suffixes for another)

• none : PossessiveAffixPosition

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

instance Phenomena.Possession.Typology.instDecidableEqPossessiveAffixPosition : DecidableEq PossessiveAffixPosition

Equations

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

instance Phenomena.Possession.Typology.instBEqPossessiveAffixPosition : BEq PossessiveAffixPosition

Equations

• Phenomena.Possession.Typology.instBEqPossessiveAffixPosition = { beq := Phenomena.Possession.Typology.instBEqPossessiveAffixPosition.beq }

def Phenomena.Possession.Typology.instBEqPossessiveAffixPosition.beq : PossessiveAffixPosition → PossessiveAffixPosition → Bool

Equations

• Phenomena.Possession.Typology.instBEqPossessiveAffixPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instReprPossessiveAffixPosition : Repr PossessiveAffixPosition

Equations

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

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

Equations

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

inductive Phenomena.Possession.Typology.NumberOfPossessiveNouns : Type

WALS Ch 58B: Number of possessive nouns.

How many nouns in the language function as possessive markers (i.e., nouns whose primary grammatical function is to express possession, such as English "property" used as a possessive classifier). Most languages have none; a small number have one or more.

• 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.

instance Phenomena.Possession.Typology.instDecidableEqNumberOfPossessiveNouns : DecidableEq NumberOfPossessiveNouns

Equations

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

def Phenomena.Possession.Typology.instBEqNumberOfPossessiveNouns.beq : NumberOfPossessiveNouns → NumberOfPossessiveNouns → Bool

Equations

• Phenomena.Possession.Typology.instBEqNumberOfPossessiveNouns.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instBEqNumberOfPossessiveNouns : BEq NumberOfPossessiveNouns

Equations

• Phenomena.Possession.Typology.instBEqNumberOfPossessiveNouns = { beq := Phenomena.Possession.Typology.instBEqNumberOfPossessiveNouns.beq }

instance Phenomena.Possession.Typology.instReprNumberOfPossessiveNouns : Repr NumberOfPossessiveNouns

Equations

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

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

Equations

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

structure Phenomena.Possession.Typology.WALSCount : Type

A single row in a WALS frequency table: a category label and its count.

• label : String
• count : Nat

def Phenomena.Possession.Typology.instReprWALSCount.repr : WALSCount → Nat → Std.Format

Equations

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

instance Phenomena.Possession.Typology.instReprWALSCount : Repr WALSCount

Equations

• Phenomena.Possession.Typology.instReprWALSCount = { reprPrec := Phenomena.Possession.Typology.instReprWALSCount.repr }

def Phenomena.Possession.Typology.instDecidableEqWALSCount.decEq (x✝ x✝¹ : WALSCount) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Possession.Typology.instDecidableEqWALSCount : DecidableEq WALSCount

Equations

• Phenomena.Possession.Typology.instDecidableEqWALSCount = Phenomena.Possession.Typology.instDecidableEqWALSCount.decEq

instance Phenomena.Possession.Typology.instBEqWALSCount : BEq WALSCount

Equations

• Phenomena.Possession.Typology.instBEqWALSCount = { beq := Phenomena.Possession.Typology.instBEqWALSCount.beq }

def Phenomena.Possession.Typology.instBEqWALSCount.beq : WALSCount → WALSCount → Bool

Equations

• Phenomena.Possession.Typology.instBEqWALSCount.beq { label := a, count := a_1 } { label := b, count := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Possession.Typology.instBEqWALSCount.beq x✝¹ x✝ = false

def Phenomena.Possession.Typology.WALSCount.totalOf (cs : List WALSCount) : Nat

Sum of counts in a WALS table.

Equations

• Phenomena.Possession.Typology.WALSCount.totalOf cs = List.foldl (fun (acc : Nat) (c : Phenomena.Possession.Typology.WALSCount) => acc + c.count) 0 cs

def Phenomena.Possession.Typology.ch58Counts : List WALSCount

Chapter 58 distribution: obligatory possessive inflection (N = 244). Computed from WALS F58A data.

Equations

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

def Phenomena.Possession.Typology.ch59Counts : List WALSCount

Chapter 59 distribution: possessive classification (N = 243). Computed from WALS F59A data. WALS distinguishes "3--5 classes" 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.

theorem Phenomena.Possession.Typology.ch58_total : WALSCount.totalOf ch58Counts = 244

Ch 58 total: 244 languages.

theorem Phenomena.Possession.Typology.ch59_total : WALSCount.totalOf ch59Counts = 243

Ch 59 total: 243 languages.

def Phenomena.Possession.Typology.ch58bCounts : List WALSCount

Chapter 58B distribution: number of possessive nouns (N = 243). Computed from WALS F58B data.

Equations

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

theorem Phenomena.Possession.Typology.ch58b_total : WALSCount.totalOf ch58bCounts = 243

Ch 58B total: 243 languages.

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

Ch 58 has one more language than Ch 59 (244 vs 243).

theorem Phenomena.Possession.Typology.ch57_wals_total : Phenomena.Possession.Typology.ch57✝.length = 902

Ch 57 total: 902 languages.

theorem Phenomena.Possession.Typology.ch58_wals_total : Phenomena.Possession.Typology.ch58✝.length = 244

Ch 58 total from WALS generated data: 244 languages.

theorem Phenomena.Possession.Typology.ch59_wals_total : Phenomena.Possession.Typology.ch59✝.length = 243

Ch 59 total from WALS generated data: 243 languages. Note: Ch 59 has 243 languages (one fewer than Ch 58 — Panare is in Ch 58 but not Ch 59).

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

Ch 57 value distribution from WALS data.

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

Ch 58 value distribution from WALS data.

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

Ch 59 value distribution from WALS data.

theorem Phenomena.Possession.Typology.ch58b_wals_total : Phenomena.Possession.Typology.ch58b✝.length = 243

Ch 58B total from WALS generated data: 243 languages.

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

Ch 58B value distribution from WALS data.

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

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

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

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

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

Ch 58: Languages without obligatory possession vastly outnumber those with it in the WALS data (201 vs 43).

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

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

structure Phenomena.Possession.Typology.PossessionProfile : Type

A language's possession profile across WALS Chapters 58--59 and the additional typological dimensions of predicative and adnominal possession.

• language : String

  Language name.

• family : String

  Language family.

• iso : String

  ISO 639-3 code.

• obligatoryPossession : ObligatoryPossession

  Ch 58: Whether obligatory possessive inflection exists.

• possessiveClassification : PossessiveClassification

  Ch 59: Whether the language classifies possessive constructions.

• 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.

instance Phenomena.Possession.Typology.instReprPossessionProfile : Repr PossessionProfile

Equations

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

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

Equations

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

def Phenomena.Possession.Typology.english : PossessionProfile

English (Indo-European, Germanic). No obligatory possessive inflection: all nouns can appear unpossessed ("a hand", "a mother"). No possessive classification: the same genitive clitic -'s or prepositional of is used for all types of possession. Predicative possession uses the have-verb have. Adnominal possession is dependent-marking (John's book).

Equations

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

def Phenomena.Possession.Typology.russian : PossessionProfile

Russian (Indo-European, Slavic). No obligatory possessive inflection. No possessive classification. Predicative possession is locational: u menja est' kniga 'at me exists book' = 'I have a book'. The preposition u + genitive case marks the possessor; est' is the existential copula. Adnominal possession is dependent-marking via genitive case (kniga Ivana 'book Ivan.GEN').

Equations

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

def Phenomena.Possession.Typology.japanese : PossessionProfile

Japanese (Japonic). No obligatory possessive inflection: body-part and kinship nouns appear freely without possessors. No possessive classification: the genitive particle no is used uniformly. Predicative possession uses a topic-comment strategy: watashi-ni-wa hon-ga aru 'I-DAT-TOP book-NOM exist' = 'I have a book'. Adnominal possession is dependent-marking (Tanaka-no hon 'Tanaka-GEN book').

Equations

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

def Phenomena.Possession.Typology.turkish : PossessionProfile

Turkish (Turkic). Obligatory possessive inflection exists: kinship terms and body-part nouns in certain constructions require possessive suffixes. For example, el-im 'hand-POSS.1SG' vs bare el 'hand' is acceptable in isolation but not in relational contexts. WALS codes Turkish as having obligatory possession. No possessive classification: the same suffix paradigm is used for all nouns. Predicative possession uses a have-verb-like construction: (benim) kitab-im var '(my) book-POSS.1SG exists' --- though var is an existential predicate, not a true transitive verb. Adnominal possession is double-marking: Ali-nin kitab-i 'Ali-GEN book-POSS.3SG'.

Equations

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

def Phenomena.Possession.Typology.hindiUrdu : PossessionProfile

Hindi-Urdu (Indo-European, Indo-Aryan). No obligatory possessive inflection. No possessive classification: the postposition kaa/ke/kii (agreeing in gender/number with possessum) is used uniformly. Predicative possession uses a genitive/dative strategy: mere paas kitaab hai 'my near book is' = 'I have a book'. The postposition paas ('near') marks the possessor. Adnominal possession is dependent-marking (Raam kaa ghar 'Ram GEN house').

Equations

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

def Phenomena.Possession.Typology.mandarin : PossessionProfile

Mandarin Chinese (Sino-Tibetan). No obligatory possessive inflection: relational nouns appear freely without possessors. No possessive classification. Predicative possession uses the have-verb you: wo you yi-ben shu 'I have one-CL book'. Adnominal possession uses the particle de on the possessor: wo de shu 'I DE book' = 'my book'. In close/inalienable relations, de is often dropped: wo mama 'I mama' = 'my mother'.

Equations

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

def Phenomena.Possession.Typology.finnish : PossessionProfile

Finnish (Uralic). No obligatory possessive inflection (though possessive suffixes exist and are used in literary style). No possessive classification. Predicative possession uses a locational/existential strategy with the adessive case: minu-lla on kirja 'I-ADESS is book' = 'I have a book'. The adessive case -lla / -lla ('at') marks the possessor. Adnominal possession is dependent-marking via genitive case (Matin kirja 'Matti.GEN book').

Equations

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

def Phenomena.Possession.Typology.hungarian : PossessionProfile

Hungarian (Uralic). Obligatory possessive inflection exists: certain relational nouns require possessive suffixes. For example, kez-e 'hand-POSS.3SG' is the normal form; bare kez requires specific contexts. No possessive classification. Predicative possession uses a locational/dative strategy: nekem van (egy) konyv-em 'I.DAT exists (a) book-POSS.1SG' = 'I have a book'. Adnominal possession is head-marking: the possessive suffix appears on the possessed noun (Janos kalap-ja 'John hat-POSS.3SG').

Equations

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

def Phenomena.Possession.Typology.irish : PossessionProfile

Irish (Indo-European, Celtic). No obligatory possessive inflection. No possessive classification. Predicative possession uses a genitive/dative strategy with the preposition ag ('at'): ta leabhar agam 'is book at-me' = 'I have a book'. This is the canonical Celtic "at-possession" pattern. Adnominal possession is dependent-marking via the genitive case after the possessed noun (teach an fhir 'house the man.GEN' = 'the man's house').

Equations

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

def Phenomena.Possession.Typology.swahili : PossessionProfile

Swahili (Niger-Congo, Bantu). No obligatory possessive inflection in the WALS sense (possessive markers are optional). No possessive classification: the possessive particle a with noun-class agreement (ch-ake, w-ake) is used uniformly. Predicative possession uses a comitative/conjunctional strategy: nina kitabu = ni-na kitabu 'I-with book' = 'I have a book'. The prefix na- is a comitative marker. Adnominal possession is head-marking via noun-class agreement (kitabu ch-ake 'book CL7-POSS.3SG').

Equations

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

def Phenomena.Possession.Typology.korean : PossessionProfile

Korean (Koreanic). No obligatory possessive inflection. No possessive classification: the genitive marker -ui is used uniformly. Predicative possession uses a locational/existential strategy: na-ege chaek-i iss-da 'I-DAT book-NOM exist-DECL' = 'I have a book'. Adnominal possession is dependent-marking (Yeonghui-ui chaek 'Yeonghui-GEN book').

Equations

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

def Phenomena.Possession.Typology.arabic : PossessionProfile

Arabic (Afro-Asiatic, Semitic). No obligatory possessive inflection in the strict WALS sense. No possessive classification: the construct state (idaafa) is used for all adnominal possession. Predicative possession uses a genitive/dative strategy: indi kitaab 'at-me book' = 'I have a book'. The preposition inda marks the possessor. Adnominal possession uses the construct state (juxtaposition with morphophonological changes): kitaabu l-waladi 'book the-boy' = 'the boy's book'.

Equations

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

def Phenomena.Possession.Typology.quechua : PossessionProfile

Quechua (Quechuan, Peru/Bolivia). Obligatory possessive inflection exists: kinship terms and body-part nouns require possessive suffixes. For example, mama-y 'mother-POSS.1SG' is required; bare mama in isolation refers to a general concept rather than a specific person's mother. Two-way possessive classification is sometimes analyzed (alienable using -yuq vs inalienable using direct suffixation), though this is debated. Predicative possession uses a suffix strategy: Hwan-pa wasi-n ka-n 'John-GEN house-POSS.3 be-3SG' or the suffix -yuq meaning 'having'. Adnominal possession is double-marking: Hwan-pa wasi-n 'John-GEN house-POSS.3'.

Equations

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

def Phenomena.Possession.Typology.yoruba : PossessionProfile

Yoruba (Niger-Congo, Atlantic-Congo). No obligatory possessive inflection. No possessive classification: the same construction is used for all types of possession. Predicative possession uses a have-verb ni: mo ni iwe 'I have book' = 'I have a book'. Adnominal possession is juxtaposition with possessor following possessum: iwe mi 'book I' = 'my book'.

Equations

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

def Phenomena.Possession.Typology.georgian : PossessionProfile

Georgian (Kartvelian). No obligatory possessive inflection in WALS. No possessive classification. Predicative possession uses a locational/dative strategy: me m-akvs cigni 'I.DAT I-have.it book' = 'I have a book'. The verb akvs shows agreement with both possessor and possessum. Adnominal possession is double-marking: kac-is saxl-i 'man-GEN house-NOM' (genitive on possessor, nominative suffix changes on possessum).

Equations

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

def Phenomena.Possession.Typology.hawaiian : PossessionProfile

Hawaiian (Austronesian, Polynesian). No obligatory possessive inflection. Two-way possessive classification: a-class possession (ko/ka) for alienable possession (acquired objects) vs o-class possession (ko/ko) for inalienable possession (body parts, kinship, means of transport, clothing, land). This is a classic alienable/inalienable system, well studied in the Oceanic literature.

Predicative possession uses a locational/existential strategy: possession is expressed via existential constructions. Adnominal possession is dependent-marking with the possessive particles a or o depending on the alienability class.

Equations

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

def Phenomena.Possession.Typology.fijian : PossessionProfile

Fijian (Austronesian, Oceanic). No obligatory possessive inflection. Three or more classes of possessive classification: Fijian distinguishes at least four possessive classes: (1) direct/inalienable suffixation for body parts and kinship, (2) edible possession (ke-), (3) drinkable possession (me-), and (4) general/alienable possession (no-). This is one of the most elaborate possessive classification systems attested.

Predicative possession uses a locational/existential strategy. Adnominal possession is head-marking: the possessive classifier appears as a prefix on the possessum.

Equations

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

def Phenomena.Possession.Typology.allLanguages : List PossessionProfile

All language profiles in the sample.

Equations

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

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

Does a language have obligatory possessive inflection?

Equations

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

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

Does a language have any possessive classification?

Equations

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

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

Does a language use a have-verb strategy?

Equations

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

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

Does a language use a locational/existential strategy?

Equations

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

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

Does a language use head-marking for adnominal possession?

Equations

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

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

Does a language use dependent-marking for adnominal possession?

Equations

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

def Phenomena.Possession.Typology.countByPredicative (langs : List PossessionProfile) (s : PredicativePossession) : Nat

Count of languages in the sample with a given predicative strategy.

Equations

• Phenomena.Possession.Typology.countByPredicative langs s = (List.filter (fun (x : Phenomena.Possession.Typology.PossessionProfile) => x.predicativeStrategy == s) langs).length

def Phenomena.Possession.Typology.countByAdnominal (langs : List PossessionProfile) (s : AdnominalPossession) : Nat

Count of languages in the sample with a given adnominal strategy.

Equations

• Phenomena.Possession.Typology.countByAdnominal langs s = (List.filter (fun (x : Phenomena.Possession.Typology.PossessionProfile) => x.adnominalStrategy == s) langs).length

theorem Phenomena.Possession.Typology.english_no_obligatory : (english.obligatoryPossession == ObligatoryPossession.noObligatory) = true

theorem Phenomena.Possession.Typology.turkish_has_obligatory : (turkish.obligatoryPossession == ObligatoryPossession.exists_) = true

theorem Phenomena.Possession.Typology.hungarian_has_obligatory : (hungarian.obligatoryPossession == ObligatoryPossession.exists_) = true

theorem Phenomena.Possession.Typology.quechua_has_obligatory : (quechua.obligatoryPossession == ObligatoryPossession.exists_) = true

theorem Phenomena.Possession.Typology.japanese_no_obligatory : (japanese.obligatoryPossession == ObligatoryPossession.noObligatory) = true

theorem Phenomena.Possession.Typology.russian_no_obligatory : (russian.obligatoryPossession == ObligatoryPossession.noObligatory) = true

theorem Phenomena.Possession.Typology.english_no_classification : (english.possessiveClassification == PossessiveClassification.noClassification) = true

theorem Phenomena.Possession.Typology.hawaiian_two_way : (hawaiian.possessiveClassification == PossessiveClassification.twoWay) = true

theorem Phenomena.Possession.Typology.quechua_two_way : (quechua.possessiveClassification == PossessiveClassification.twoWay) = true

theorem Phenomena.Possession.Typology.fijian_three_or_more : (fijian.possessiveClassification == PossessiveClassification.threeOrMore) = true

theorem Phenomena.Possession.Typology.mandarin_no_classification : (mandarin.possessiveClassification == PossessiveClassification.noClassification) = true

theorem Phenomena.Possession.Typology.english_have_verb : (english.predicativeStrategy == PredicativePossession.haveVerb) = true

theorem Phenomena.Possession.Typology.russian_locational : (russian.predicativeStrategy == PredicativePossession.locational) = true

theorem Phenomena.Possession.Typology.japanese_topic : (japanese.predicativeStrategy == PredicativePossession.topic) = true

theorem Phenomena.Possession.Typology.finnish_locational : (finnish.predicativeStrategy == PredicativePossession.locational) = true

theorem Phenomena.Possession.Typology.irish_genitive_dative : (irish.predicativeStrategy == PredicativePossession.genitiveDative) = true

theorem Phenomena.Possession.Typology.hindi_genitive_dative : (hindiUrdu.predicativeStrategy == PredicativePossession.genitiveDative) = true

theorem Phenomena.Possession.Typology.swahili_comitative : (swahili.predicativeStrategy == PredicativePossession.comitative) = true

theorem Phenomena.Possession.Typology.mandarin_have_verb : (mandarin.predicativeStrategy == PredicativePossession.haveVerb) = true

theorem Phenomena.Possession.Typology.english_dependent : (english.adnominalStrategy == AdnominalPossession.dependentMarking) = true

theorem Phenomena.Possession.Typology.hungarian_head : (hungarian.adnominalStrategy == AdnominalPossession.headMarking) = true

theorem Phenomena.Possession.Typology.turkish_double : (turkish.adnominalStrategy == AdnominalPossession.doubleMarking) = true

theorem Phenomena.Possession.Typology.arabic_juxtaposition : (arabic.adnominalStrategy == AdnominalPossession.juxtaposition) = true

theorem Phenomena.Possession.Typology.yoruba_juxtaposition : (yoruba.adnominalStrategy == AdnominalPossession.juxtaposition) = true

theorem Phenomena.Possession.Typology.quechua_double : (quechua.adnominalStrategy == AdnominalPossession.doubleMarking) = true

theorem Phenomena.Possession.Typology.english_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "eng") = english.affixPosition

theorem Phenomena.Possession.Typology.russian_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "rus") = russian.affixPosition

theorem Phenomena.Possession.Typology.japanese_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "jpn") = japanese.affixPosition

theorem Phenomena.Possession.Typology.turkish_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "tur") = turkish.affixPosition

theorem Phenomena.Possession.Typology.mandarin_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "mnd") = mandarin.affixPosition

theorem Phenomena.Possession.Typology.finnish_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "fin") = finnish.affixPosition

theorem Phenomena.Possession.Typology.hungarian_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "hun") = hungarian.affixPosition

theorem Phenomena.Possession.Typology.irish_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "iri") = irish.affixPosition

theorem Phenomena.Possession.Typology.swahili_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "swa") = swahili.affixPosition

theorem Phenomena.Possession.Typology.arabic_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "aeg") = arabic.affixPosition

theorem Phenomena.Possession.Typology.quechua_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "qim") = quechua.affixPosition

theorem Phenomena.Possession.Typology.yoruba_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "yor") = yoruba.affixPosition

theorem Phenomena.Possession.Typology.georgian_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "geo") = georgian.affixPosition

theorem Phenomena.Possession.Typology.hawaiian_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "haw") = hawaiian.affixPosition

theorem Phenomena.Possession.Typology.fijian_ch57 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F57A.PositionOfPronominalPossessiveAffixes) => Phenomena.Possession.Typology.fromWALS57A✝ x.value) (Core.WALS.F57A.lookup "fij") = fijian.affixPosition

theorem Phenomena.Possession.Typology.english_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "eng") = some english.obligatoryPossession

theorem Phenomena.Possession.Typology.russian_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "rus") = some russian.obligatoryPossession

theorem Phenomena.Possession.Typology.japanese_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "jpn") = some japanese.obligatoryPossession

theorem Phenomena.Possession.Typology.hindi_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "hin") = some hindiUrdu.obligatoryPossession

theorem Phenomena.Possession.Typology.mandarin_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "mnd") = some mandarin.obligatoryPossession

theorem Phenomena.Possession.Typology.finnish_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "fin") = some finnish.obligatoryPossession

theorem Phenomena.Possession.Typology.swahili_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "swa") = some swahili.obligatoryPossession

theorem Phenomena.Possession.Typology.korean_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "kor") = some korean.obligatoryPossession

theorem Phenomena.Possession.Typology.arabic_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "aeg") = some arabic.obligatoryPossession

theorem Phenomena.Possession.Typology.yoruba_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "yor") = some yoruba.obligatoryPossession

theorem Phenomena.Possession.Typology.georgian_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "geo") = some georgian.obligatoryPossession

theorem Phenomena.Possession.Typology.fijian_ch58 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => Phenomena.Possession.Typology.fromWALS58A✝ x.value) (Core.WALS.F58A.lookup "fij") = some fijian.obligatoryPossession

theorem Phenomena.Possession.Typology.english_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "eng") = some english.possessiveClassification

theorem Phenomena.Possession.Typology.russian_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "rus") = some russian.possessiveClassification

theorem Phenomena.Possession.Typology.japanese_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "jpn") = some japanese.possessiveClassification

theorem Phenomena.Possession.Typology.turkish_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "tur") = some turkish.possessiveClassification

theorem Phenomena.Possession.Typology.hindi_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "hin") = some hindiUrdu.possessiveClassification

theorem Phenomena.Possession.Typology.mandarin_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "mnd") = some mandarin.possessiveClassification

theorem Phenomena.Possession.Typology.finnish_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "fin") = some finnish.possessiveClassification

theorem Phenomena.Possession.Typology.hungarian_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "hun") = some hungarian.possessiveClassification

theorem Phenomena.Possession.Typology.swahili_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "swa") = some swahili.possessiveClassification

theorem Phenomena.Possession.Typology.korean_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "kor") = some korean.possessiveClassification

theorem Phenomena.Possession.Typology.arabic_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "aeg") = some arabic.possessiveClassification

theorem Phenomena.Possession.Typology.yoruba_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "yor") = some yoruba.possessiveClassification

theorem Phenomena.Possession.Typology.georgian_ch59 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => Phenomena.Possession.Typology.fromWALS59A✝ x.value) (Core.WALS.F59A.lookup "geo") = some georgian.possessiveClassification

theorem Phenomena.Possession.Typology.english_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "eng") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.russian_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "rus") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.japanese_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "jpn") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.turkish_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "tur") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.hindi_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "hin") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.mandarin_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "mnd") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.finnish_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "fin") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.hungarian_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "hun") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.swahili_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "swa") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.korean_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "kor") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.arabic_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "aeg") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.quechua_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "qim") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.yoruba_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "yor") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.georgian_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "geo") = some NumberOfPossessiveNouns.noneReported

theorem Phenomena.Possession.Typology.fijian_ch58b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F58B.NumberOfPossessiveNouns) => Phenomena.Possession.Typology.fromWALS58B✝ x.value) (Core.WALS.F58B.lookup "fij") = some NumberOfPossessiveNouns.twoToFour

theorem Phenomena.Possession.Typology.no_classification_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.noPossessiveClassification) Phenomena.Possession.Typology.ch59✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.twoClasses) Phenomena.Possession.Typology.ch59✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.twoClasses) Phenomena.Possession.Typology.ch59✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.threeToFiveClasses) Phenomena.Possession.Typology.ch59✝³).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.moreThanFiveClasses) Phenomena.Possession.Typology.ch59✝⁴).length

Ch 59: No possessive classification (125) is the most common value, followed by two-way classification (94). Three-or-more-way classification (24) is the least common: 125 > 94 > 24.

theorem Phenomena.Possession.Typology.no_classification_plurality : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.noPossessiveClassification) Phenomena.Possession.Typology.ch59✝).length > Phenomena.Possession.Typology.ch59✝¹.length / 3

Most languages in the WALS sample lack possessive classification: 125 out of 243 (51.4%).

theorem Phenomena.Possession.Typology.no_obligatory_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Core.WALS.F58A.ObligatoryPossessiveInflection.absent) Phenomena.Possession.Typology.ch58✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Core.WALS.F58A.ObligatoryPossessiveInflection.exists) Phenomena.Possession.Typology.ch58✝¹).length

Ch 58: Languages without obligatory possessive inflection (201) outnumber those with it (43) by a substantial margin.

theorem Phenomena.Possession.Typology.no_obligatory_over_half : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F58A.ObligatoryPossessiveInflection) => x.value == Core.WALS.F58A.ObligatoryPossessiveInflection.absent) Phenomena.Possession.Typology.ch58✝).length > Phenomena.Possession.Typology.ch58✝¹.length / 2

Ch 58: Over half of sampled languages lack obligatory possession.

theorem Phenomena.Possession.Typology.classification_vs_no_classification : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.twoClasses) Phenomena.Possession.Typology.ch59✝).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.threeToFiveClasses) Phenomena.Possession.Typology.ch59✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.moreThanFiveClasses) Phenomena.Possession.Typology.ch59✝²).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.noPossessiveClassification) Phenomena.Possession.Typology.ch59✝³).length = Phenomena.Possession.Typology.ch59✝⁴.length

Languages with possessive classification (2-way or 3+) outnumber those with no classification by a narrow margin: 94 + 24 = 118 vs 125. (Unlike the old hardcoded data, classification does NOT exceed no-classification; they are close.)

theorem Phenomena.Possession.Typology.two_way_dominates_three_plus : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.twoClasses) Phenomena.Possession.Typology.ch59✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.threeToFiveClasses) Phenomena.Possession.Typology.ch59✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F59A.PossessiveClassification) => x.value == Core.WALS.F59A.PossessiveClassification.moreThanFiveClasses) Phenomena.Possession.Typology.ch59✝²).length

Among languages with possessive classification, two-way systems are nearly four times as common as three-or-more-way systems.

theorem Phenomena.Possession.Typology.predicative_distribution : countByPredicative allLanguages PredicativePossession.locational = 8 ∧ countByPredicative allLanguages PredicativePossession.haveVerb = 4 ∧ countByPredicative allLanguages PredicativePossession.genitiveDative = 3 ∧ countByPredicative allLanguages PredicativePossession.topic = 1 ∧ countByPredicative allLanguages PredicativePossession.comitative = 1

In our sample, locational strategies are the most common predicative possession type (8 languages), followed by have-verb (4), genitive/dative (3), topic (1), and comitative (1).

theorem Phenomena.Possession.Typology.all_predicative_strategies_attested : (((((allLanguages.any fun (x : PossessionProfile) => x.predicativeStrategy == PredicativePossession.haveVerb) && allLanguages.any fun (x : PossessionProfile) => x.predicativeStrategy == PredicativePossession.locational) && allLanguages.any fun (x : PossessionProfile) => x.predicativeStrategy == PredicativePossession.genitiveDative) && allLanguages.any fun (x : PossessionProfile) => x.predicativeStrategy == PredicativePossession.topic) && decide ((allLanguages.any fun (x : PossessionProfile) => x.predicativeStrategy == PredicativePossession.comitative) = true)) = true

All five predicative possession strategies are attested in our sample.

theorem Phenomena.Possession.Typology.adnominal_distribution : countByAdnominal allLanguages AdnominalPossession.dependentMarking = 9 ∧ countByAdnominal allLanguages AdnominalPossession.doubleMarking = 3 ∧ countByAdnominal allLanguages AdnominalPossession.headMarking = 3 ∧ countByAdnominal allLanguages AdnominalPossession.juxtaposition = 2

In our sample, dependent-marking is the most common adnominal possession strategy (9 languages), followed by double-marking (3), head-marking (3), and juxtaposition (2).

theorem Phenomena.Possession.Typology.dependent_marking_dominant : countByAdnominal allLanguages AdnominalPossession.dependentMarking > countByAdnominal allLanguages AdnominalPossession.headMarking + countByAdnominal allLanguages AdnominalPossession.juxtaposition

Dependent-marking exceeds all other adnominal strategies combined in our sample (but note the European bias).

theorem Phenomena.Possession.Typology.have_verb_implies_not_head_marking : have haveLangs := List.filter (fun (x : PossessionProfile) => x.usesHaveVerb) allLanguages; (haveLangs.all fun (p : PossessionProfile) => p.adnominalStrategy != AdnominalPossession.headMarking) = true

In our sample, every language with a have-verb strategy for predicative possession also uses dependent-marking or juxtaposition for adnominal possession. No have-verb language uses head-marking. This reflects a structural parallel: have-verb treats the possessor as subject (a dependent-marking strategy at the clause level).

theorem Phenomena.Possession.Typology.head_marking_mostly_complex_possession : have headLangs := List.filter (fun (x : PossessionProfile) => x.isHeadMarking) allLanguages; have complexHeadLangs := List.filter (fun (p : PossessionProfile) => p.hasObligatoryPossession || p.hasClassification) headLangs; headLangs.length = 3 ∧ complexHeadLangs.length = 2

In our sample, most head-marking languages (Hungarian, Fijian) have either obligatory possessive inflection or possessive classification. Two of three head-marking languages show complex possession systems, reflecting the structural affinity between head-marking and elaborate possessive morphology on the possessed noun. Swahili is the exception: head-marking via noun-class agreement but no obligatory possession or classification.

theorem Phenomena.Possession.Typology.locational_count : (List.filter (fun (x : PossessionProfile) => x.usesLocational) allLanguages).length = 8

In our sample, locational/existential predicative possession is the most widespread strategy (8 languages: Russian, Turkish, Finnish, Hungarian, Korean, Georgian, Hawaiian, Fijian). The Eurasian "habeo-less" belt stretches from Finland through Turkey to Korea, and locational strategies also appear in Oceanian languages.

def Phenomena.Possession.Typology.oceanicLanguages : List PossessionProfile

In our sample, both Oceanic/Austronesian languages (Hawaiian, Fijian) have possessive classification (two-way or three-or-more). Possessive classification is an areal feature of the Pacific: the alienable/inalienable distinction is nearly universal in Oceanic.

Equations

• Phenomena.Possession.Typology.oceanicLanguages = [Phenomena.Possession.Typology.hawaiian, Phenomena.Possession.Typology.fijian]

theorem Phenomena.Possession.Typology.oceanic_have_classification : (oceanicLanguages.all fun (x : PossessionProfile) => x.hasClassification) = true

theorem Phenomena.Possession.Typology.double_marking_count : countByAdnominal allLanguages AdnominalPossession.doubleMarking = 3

Double-marking (both possessor and possessum are overtly marked) appears in Turkish, Quechua, and Georgian in our sample. This is the most "redundant" strategy --- both participants in the possessive relation carry morphological marking.

theorem Phenomena.Possession.Typology.double_marking_languages : have doubleLangs := List.filter (fun (x : PossessionProfile) => x.adnominalStrategy == AdnominalPossession.doubleMarking) allLanguages; doubleLangs.length = 3

All double-marking languages in our sample are agglutinative or have rich morphology (Turkish, Quechua, Georgian). This is expected: double-marking requires the morphological resources to place markers on both nouns in the possessive construction.

theorem Phenomena.Possession.Typology.have_verb_mostly_no_obligatory : have haveLangs := List.filter (fun (x : PossessionProfile) => x.usesHaveVerb) allLanguages; have haveNoOblig := List.filter (fun (p : PossessionProfile) => !p.hasObligatoryPossession) haveLangs; haveLangs.length = 4 ∧ haveNoOblig.length = 3

In our sample, most languages with the have-verb strategy lack obligatory possessive inflection (English, Mandarin, Yoruba). Quechua is the exception: it has both a have-verb-like construction (-yuq 'having') and obligatory possessive suffixes on kinship/body-part nouns. Three of four have-verb languages lack obligatory possession.

theorem Phenomena.Possession.Typology.classification_and_obligatory_independent : have classified := List.filter (fun (x : PossessionProfile) => x.hasClassification) allLanguages; have classifiedAndObligatory := List.filter (fun (x : PossessionProfile) => x.hasObligatoryPossession) classified; classified.length = 3 ∧ classifiedAndObligatory.length = 1

In our sample, languages with possessive classification all lack obligatory possessive inflection (Hawaiian, Fijian, Quechua). The two phenomena are logically independent: a language could require possession AND classify it. But empirically, the rich classification system itself may reduce the pressure for obligatory marking.

theorem Phenomena.Possession.Typology.sample_size : allLanguages.length = 17

Number of languages in our sample.

theorem Phenomena.Possession.Typology.sample_obligatory_count : (List.filter (fun (x : PossessionProfile) => x.hasObligatoryPossession) allLanguages).length = 3

Distribution of obligatory possession in our sample.

theorem Phenomena.Possession.Typology.sample_classification_count : (List.filter (fun (x : PossessionProfile) => x.hasClassification) allLanguages).length = 3

Distribution of possessive classification in our sample.

theorem Phenomena.Possession.Typology.all_adnominal_strategies_attested : ((((allLanguages.any fun (x : PossessionProfile) => x.adnominalStrategy == AdnominalPossession.headMarking) && allLanguages.any fun (x : PossessionProfile) => x.adnominalStrategy == AdnominalPossession.dependentMarking) && allLanguages.any fun (x : PossessionProfile) => x.adnominalStrategy == AdnominalPossession.doubleMarking) && decide ((allLanguages.any fun (x : PossessionProfile) => x.adnominalStrategy == AdnominalPossession.juxtaposition) = true)) = true

All four adnominal strategies are attested in our sample.

inductive Phenomena.Possession.Typology.PossessiveNotion : Type

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).

@cite{heine-1997} §2.3 identifies seven notions ordered by increasing abstractness:

physical < temporary < permanent < inalienable < abstract

with two additional notions for inanimate possessors (inanimate inalienable, inanimate alienable). These notions form the target meanings that source schemas grammaticalize into.

• physical : PossessiveNotion

  Physical possession: possessor has physical control over possessee. (e.g., "I have a pen (in my hand)")

• temporary : PossessiveNotion

  Temporary possession: possessor controls possessee for a limited time. (e.g., "I have a rental car")

• permanent : PossessiveNotion

  Permanent possession: possessor owns possessee. (e.g., "I have a house")

• inalienable : PossessiveNotion

  Inalienable possession: possessee is inherently associated with possessor. (e.g., "I have two sisters", "I have blue eyes")

• abstract : PossessiveNotion

  Abstract possession: possessee is non-concrete. (e.g., "I have a headache", "I have an idea")

• inanimateInalienable : PossessiveNotion

  Inanimate inalienable: inanimate possessor, inherent relation. (e.g., "The tree has branches", "The table has four legs")

• inanimateAlienable : PossessiveNotion

  Inanimate alienable: inanimate possessor, non-inherent relation. (e.g., "The room has a window" -- contingent, not body-part-like)

instance Phenomena.Possession.Typology.instDecidableEqPossessiveNotion : DecidableEq PossessiveNotion

Equations

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

def Phenomena.Possession.Typology.instBEqPossessiveNotion.beq : PossessiveNotion → PossessiveNotion → Bool

Equations

• Phenomena.Possession.Typology.instBEqPossessiveNotion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instBEqPossessiveNotion : BEq PossessiveNotion

Equations

• Phenomena.Possession.Typology.instBEqPossessiveNotion = { beq := Phenomena.Possession.Typology.instBEqPossessiveNotion.beq }

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

Equations

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

instance Phenomena.Possession.Typology.instReprPossessiveNotion : Repr PossessiveNotion

Equations

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

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

Abstractness ordering: higher = more abstract possessive notion. Physical possession is the most concrete; abstract the most abstract. Inanimate notions are ranked by extending the animacy dimension.

Equations

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

inductive Phenomena.Possession.Typology.InalienabilityRank : Type

The inalienability hierarchy.

If a language marks a distinction between alienable and inalienable possession, the inalienable class is drawn from the top of this hierarchy:

body parts > kinship terms > spatial relations > part-whole > culturally important items > general property

A language may draw the alienable/inalienable boundary at any point on the hierarchy, but if a category is inalienable, all categories above it are also inalienable. Body parts and kinship terms are always the first candidates for inalienable treatment.

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

instance Phenomena.Possession.Typology.instDecidableEqInalienabilityRank : DecidableEq InalienabilityRank

Equations

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

instance Phenomena.Possession.Typology.instBEqInalienabilityRank : BEq InalienabilityRank

Equations

• Phenomena.Possession.Typology.instBEqInalienabilityRank = { beq := Phenomena.Possession.Typology.instBEqInalienabilityRank.beq }

def Phenomena.Possession.Typology.instBEqInalienabilityRank.beq : InalienabilityRank → InalienabilityRank → Bool

Equations

• Phenomena.Possession.Typology.instBEqInalienabilityRank.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

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

instance Phenomena.Possession.Typology.instReprInalienabilityRank : Repr InalienabilityRank

Equations

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

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

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

Equations

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

theorem Phenomena.Possession.Typology.inalienability_ordering : InalienabilityRank.bodyPart.toNat > InalienabilityRank.kinship.toNat ∧ InalienabilityRank.kinship.toNat > InalienabilityRank.spatialRelation.toNat ∧ InalienabilityRank.spatialRelation.toNat > InalienabilityRank.partWhole.toNat ∧ InalienabilityRank.partWhole.toNat > InalienabilityRank.culturalItem.toNat ∧ InalienabilityRank.culturalItem.toNat > InalienabilityRank.generalProperty.toNat

The hierarchy is consistent: body parts outrank kinship, which outranks spatial relations, and so forth.

inductive Phenomena.Possession.Typology.PossessionSource : Type

Diachronic sources of predicative possession constructions.

@cite{heine-1997} Table 2.1 identifies eight event schemas from which predicative possession constructions arise via grammaticalization. The same schemas appear in @cite{heine-2009} Table 29.5 for possessive case grammaticalization; see also Core.caseExtension for the broader case extension paths from @cite{heine-2009} Table 29.6.

• action : PossessionSource

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

• location : PossessionSource

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

• companion : PossessionSource

  Companion schema: "X is with Y" → 'X has Y'. (e.g., Swahili -na < copula -wa + comitative na 'with', Venda na 'with')

• genitive : PossessionSource

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

• goal : PossessionSource

  Goal schema: "Y exists for/to X" → 'X has Y'. (e.g., Hindi mere paas kitaab hai, Irish tá leabhar agam)

• source : PossessionSource

  Source schema: "Y exists from X" → 'X has Y'. (e.g., some West African languages with ablative possessors)

• topic : PossessionSource

  Topic schema: "As for X, Y exists" → 'X has Y'. (e.g., Japanese watashi-ni-wa hon-ga aru 'I-DAT-TOP book-NOM exists')

• equation : PossessionSource

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

instance Phenomena.Possession.Typology.instDecidableEqPossessionSource : DecidableEq PossessionSource

Equations

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

def Phenomena.Possession.Typology.instBEqPossessionSource.beq : PossessionSource → PossessionSource → Bool

Equations

• Phenomena.Possession.Typology.instBEqPossessionSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Possession.Typology.instBEqPossessionSource : BEq PossessionSource

Equations

• Phenomena.Possession.Typology.instBEqPossessionSource = { beq := Phenomena.Possession.Typology.instBEqPossessionSource.beq }

instance Phenomena.Possession.Typology.instReprPossessionSource : Repr PossessionSource

Equations

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

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

Equations

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

def Phenomena.Possession.Typology.predicativeSource : PredicativePossession → PossessionSource

Map predicative strategies to their likely grammaticalization source.

Equations

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

theorem Phenomena.Possession.Typology.location_source_dominates : have locationCount := (List.filter (fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.location) allLanguages).length; have actionCount := (List.filter (fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.action) allLanguages).length; locationCount > actionCount

In our sample, the two most common grammaticalization sources for predicative possession are location and action.

theorem Phenomena.Possession.Typology.attested_sources : (((((allLanguages.any fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.action) && allLanguages.any fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.location) && allLanguages.any fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.goal) && allLanguages.any fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.companion) && decide ((allLanguages.any fun (p : PossessionProfile) => predicativeSource p.predicativeStrategy == PossessionSource.topic) = true)) = true

Five of the eight schemas are attested in our sample via predicativeSource.