Possession — typological feature substrate

Theory-neutral classification enums for possession, following the WALS possession chapters ([DH13b]). Per-language values are bare defs in Fragments/<Lang>/Possession.lean, consumed by Studies/Heine1997 and Studies/KampanarouAlexiadou2026. Bare-root Possession namespace under Features/, like Features/Case.

Main definitions

Obligatoriness and Classification (WALS 58A and 59A, [NB13d]), PredicativeStrategy ([Sta09b] four-way; [Sta13a] adds Genitive), AdnominalMarking ([Nic86]; WALS 24A, [NB13a]), Notion and Source ([Hei97], [Hei09a]), InalienabilityRank ([Aik12]), and the neutral Alienability cut.

Notes

These enums adopt specific frameworks, not field-wide consensus: PredicativeStrategy is Stassen's typology (Genitive is his WALS 117A addition, grouped with Locational as "Oblique Possessive"); Classification collapses Mayan/Oceanic multi-class systems into threeOrMore; Source (Heine's event schemas) and PredicativeStrategy are parallel typologies bridged by predicativeSource.

References

• [NB13d], [NB13a], [DH13b] — the WALS chapters (24A, 58A, 59A)
• [Sta09b], [Sta13a] — predicative possession (WALS 117A)
• [Nic86] — head- vs dependent-marking
• [Hei97], [Hei09a] — possessive notions and source schemas
• [Aik12] — inalienability

inductive Possession.Obligatoriness : Type

Whether some nouns (kinship, body parts) require possessive marking (WALS 58A).

• exists_ : Obligatoriness

  Obligatory possessive inflection exists (Mohawk, Navajo).

• noObligatory : Obligatoriness

  No obligatory possessive inflection (English, Russian).

• unclear : Obligatoriness

  Inflection exists but is never obligatory; data insufficient.

@[instance_reducible]

instance Possession.instDecidableEqObligatoriness : DecidableEq Obligatoriness

Equations

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

def Possession.instReprObligatoriness.repr : Obligatoriness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Possession.instReprObligatoriness : Repr Obligatoriness

Equations

• Possession.instReprObligatoriness = { reprPrec := Possession.instReprObligatoriness.repr }

inductive Possession.Classification : Type

Whether possession is morphosyntactically classified, typically by alienability (WALS 59A).

• noClassification : Classification

  One construction for all nouns (English, Russian).

• twoWay : Classification

  Two-way, typically alienable vs inalienable (Ewe, Rapanui).

• threeOrMore : Classification

  Three or more possessive classes.

@[instance_reducible]

instance Possession.instDecidableEqClassification : DecidableEq Classification

Equations

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

def Possession.instReprClassification.repr : Classification → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Possession.instReprClassification : Repr Classification

Equations

• Possession.instReprClassification = { reprPrec := Possession.instReprClassification.repr }

inductive Possession.PredicativeStrategy : Type

Stassen's classification of how a language predicates possession ("I have X"), with the Genitive type added in WALS 117A.

• haveVerb : PredicativeStrategy

  Transitive 'have' verb (English, Mandarin).

• locational : PredicativeStrategy

  Existential with possessor in a locative/oblique (Russian, Finnish, Irish, Hindi).

• genitive : PredicativeStrategy

  Existential with possessor in the genitive, "X's Y exists" (Turkish var).

• topic : PredicativeStrategy

  Possessor topicalized over an existential comment (Japanese).

• comitative : PredicativeStrategy

  Comitative "I am with Y" (Swahili -na).

@[instance_reducible]

instance Possession.instDecidableEqPredicativeStrategy : DecidableEq PredicativeStrategy

Equations

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

def Possession.instReprPredicativeStrategy.repr : PredicativeStrategy → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Possession.instReprPredicativeStrategy : Repr PredicativeStrategy

Equations

• Possession.instReprPredicativeStrategy = { reprPrec := Possession.instReprPredicativeStrategy.repr }

inductive Possession.AdnominalMarking : Type

The locus of marking inside the possessive NP (WALS 24A).

• headMarking : AdnominalMarking

  Marker on the possessed head noun (Hungarian, Swahili).

• dependentMarking : AdnominalMarking

  Marker on the possessor (English 's, Japanese no).

• doubleMarking : AdnominalMarking

  Both possessor and head marked (Turkish, Georgian).

• zeroMarking : AdnominalMarking

  No overt marker; word order alone (WALS "no marking"; Vietnamese).

@[instance_reducible]

instance Possession.instDecidableEqAdnominalMarking : DecidableEq AdnominalMarking

Equations

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

@[instance_reducible]

instance Possession.instReprAdnominalMarking : Repr AdnominalMarking

Equations

• Possession.instReprAdnominalMarking = { reprPrec := Possession.instReprAdnominalMarking.repr }

def Possession.instReprAdnominalMarking.repr : AdnominalMarking → Nat → Std.Format

Equations

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

inductive Possession.Notion : Type

Heine's semantic targets of possession, as opposed to Source, the diachronic origin.

• physical : Notion

  Physical possession ("a pen in my hand").

• temporary : Notion

  Temporary possession ("a rental car").

• permanent : Notion

  Permanent possession ("a house").

• inalienable : Notion

  Inalienable possession ("two sisters", "blue eyes").

• abstract : Notion

  Abstract possession ("a headache", "an idea").

• inanimateInalienable : Notion

  Inanimate inalienable ("the tree has branches").

• inanimateAlienable : Notion

  Inanimate alienable ("the room has a window").

@[instance_reducible]

instance Possession.instDecidableEqNotion : DecidableEq Notion

Equations

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

@[instance_reducible]

instance Possession.instReprNotion : Repr Notion

Equations

• Possession.instReprNotion = { reprPrec := Possession.instReprNotion.repr }

def Possession.instReprNotion.repr : Notion → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Possession.instReprNotion.repr Possession.Notion.physical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Notion.physical")).group prec✝
• Possession.instReprNotion.repr Possession.Notion.temporary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Notion.temporary")).group prec✝
• Possession.instReprNotion.repr Possession.Notion.permanent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Notion.permanent")).group prec✝
• Possession.instReprNotion.repr Possession.Notion.abstract prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Notion.abstract")).group prec✝

inductive Possession.InalienabilityRank : Type

Coarse inalienability cline, body parts and kinship ranking highest. toNat is an operationalization for comparison rather than a claimed universal, since Nichols and Aikhenvald treat kinship and body parts as co-central.

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

@[instance_reducible]

instance Possession.instDecidableEqInalienabilityRank : DecidableEq InalienabilityRank

Equations

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

@[instance_reducible]

instance Possession.instReprInalienabilityRank : Repr InalienabilityRank

Equations

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

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

Equations

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

def Possession.InalienabilityRank.toNat : InalienabilityRank → Nat

Numeric rank (higher = more likely inalienable); see InalienabilityRank.

Equations

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

inductive Possession.Source : Type

Heine's diachronic source schemas of predicative possession.

• action : Source

  Action "X takes Y" (English have < OE habban).

• location : Source

  Location "Y is at X" (Finnish adessive, Russian u).

• companion : Source

  Companion "X is with Y" (Swahili -na).

• genitive : Source

  Genitive "X's Y exists" (Turkish var).

• goal : Source

  Goal "Y exists for X" (Hindi, Irish).

• source : Source

  Source "Y exists from X".

• topic : Source

  Topic "as for X, Y exists" (Japanese).

• equation : Source

  Equation "Y is X's" (Scots Gaelic).

@[instance_reducible]

instance Possession.instDecidableEqSource : DecidableEq Source

Equations

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

@[instance_reducible]

instance Possession.instReprSource : Repr Source

Equations

• Possession.instReprSource = { reprPrec := Possession.instReprSource.repr }

def Possession.instReprSource.repr : Source → Nat → Std.Format

Equations

• Possession.instReprSource.repr Possession.Source.action prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.action")).group prec✝
• Possession.instReprSource.repr Possession.Source.location prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.location")).group prec✝
• Possession.instReprSource.repr Possession.Source.companion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.companion")).group prec✝
• Possession.instReprSource.repr Possession.Source.genitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.genitive")).group prec✝
• Possession.instReprSource.repr Possession.Source.goal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.goal")).group prec✝
• Possession.instReprSource.repr Possession.Source.source prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.source")).group prec✝
• Possession.instReprSource.repr Possession.Source.topic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.topic")).group prec✝
• Possession.instReprSource.repr Possession.Source.equation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Possession.Source.equation")).group prec✝

def Possession.predicativeSource : PredicativeStrategy → Source

Likely grammaticalization source of each predicative strategy.

Equations

• Possession.predicativeSource Possession.PredicativeStrategy.haveVerb = Possession.Source.action
• Possession.predicativeSource Possession.PredicativeStrategy.locational = Possession.Source.location
• Possession.predicativeSource Possession.PredicativeStrategy.genitive = Possession.Source.genitive
• Possession.predicativeSource Possession.PredicativeStrategy.topic = Possession.Source.topic
• Possession.predicativeSource Possession.PredicativeStrategy.comitative = Possession.Source.companion

The neutral alienability cut

inductive Possession.Alienability : Type

Neutral alienable/inalienable cut, low in Features so the typological Classification, DM PossessionType, and V&J PossessionRelationType can coarsen onto it instead of re-stipulating the contrast.

• inalienable : Alienability
• alienable : Alienability

@[instance_reducible]

instance Possession.instDecidableEqAlienability : DecidableEq Alienability

Equations

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

def Possession.instReprAlienability.repr : Alienability → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Possession.instReprAlienability : Repr Alienability

Equations

• Possession.instReprAlienability = { reprPrec := Possession.instReprAlienability.repr }

def Possession.Classification.drawsAlienabilityCut : Classification → Bool

A language draws the alienability cut iff it classifies possession at all.

Equations

• Possession.Classification.noClassification.drawsAlienabilityCut = false
• x✝.drawsAlienabilityCut = true

def Possession.InalienabilityRank.alienabilityAt (cut : InalienabilityRank) : InalienabilityRank → Alienability

Coarsening of the cline that counts ranks at or above cut as inalienable.

Equations

• cut.alienabilityAt r = if cut.toNat ≤ r.toNat then Possession.Alienability.inalienable else Possession.Alienability.alienable