Possession — typological feature substrate

[Sta09b] [Sta13a] [Nic86] [NB13d] [NB13a] [Hei97] [Hei09a] [Aik12] [DH13b]

Theory-neutral classification enums for possession. Per-language values are bare defs in Fragments/<Lang>/Possession.lean, consumed by Studies/NicholsBickel2013, Studies/Heine1997, and Studies/KampanarouAlexiadou2026. Bare-root Possession namespace under Features/, like Features/Case.

Main definitions

Obligatoriness (WALS 58A), Classification (59A), AffixPosition (57A), PredicativeStrategy ([Sta09b] four-way; [Sta13a] adds Genitive), AdnominalMarking ([Nic86]), Notion and Source ([Hei97]), InalienabilityRank, and the neutral Alienability cut. Per-language values are bare defs in Fragments/<Lang>/Possession.lean; cross-linguistic aggregation uses a study-local row in Studies/NicholsBickel2013.lean.

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.

inductive Possession.Obligatoriness : Type

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

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

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

@[implicit_reducible]

instance Possession.instReprObligatoriness : Repr Obligatoriness

Equations

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

inductive Possession.Classification : Type

WALS 59A: whether possession is morphosyntactically classified (alienability).

• noClassification : Classification

  One construction for all nouns (English, Russian).

• twoWay : Classification

  Two-way, typically alienable vs inalienable (Fijian, Hawaiian).

• threeOrMore : Classification

  Three or more possessive classes.

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

@[implicit_reducible]

instance Possession.instReprClassification : Repr Classification

Equations

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

inductive Possession.PredicativeStrategy : Type

How a language predicates possession ("I have X"); [Sta09b] four-way, [Sta13a] (WALS 117A) adds Genitive.

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

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

@[implicit_reducible]

instance Possession.instReprPredicativeStrategy : Repr PredicativeStrategy

Equations

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

inductive Possession.AdnominalMarking : Type

[Nic86]; WALS 24A [NB13a]: locus of NP-internal marking.

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

@[implicit_reducible]

instance Possession.instDecidableEqAdnominalMarking : DecidableEq AdnominalMarking

Equations

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

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

Equations

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

@[implicit_reducible]

instance Possession.instReprAdnominalMarking : Repr AdnominalMarking

Equations

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

inductive Possession.AffixPosition : Type

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

• prefixes : AffixPosition

  Possessive prefixes (Bantu, many Papuan).

• suffixes : AffixPosition

  Possessive suffixes (Turkish, Hungarian, Finnish).

• both : AffixPosition

  Both prefixes and suffixes.

• noAffix : AffixPosition

  No affixes; independent words/clitics (English my, Mandarin de).

@[implicit_reducible]

instance Possession.instDecidableEqAffixPosition : DecidableEq AffixPosition

Equations

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

@[implicit_reducible]

instance Possession.instReprAffixPosition : Repr AffixPosition

Equations

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

def Possession.instReprAffixPosition.repr : AffixPosition → Nat → Std.Format

Equations

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

inductive Possession.Notion : Type

[Hei97]: semantic targets of possession (vs 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").

@[implicit_reducible]

instance Possession.instDecidableEqNotion : DecidableEq Notion

Equations

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

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✝

@[implicit_reducible]

instance Possession.instReprNotion : Repr Notion

Equations

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

inductive Possession.InalienabilityRank : Type

Coarse inalienability cline (body-part/kinship rank highest). toNat is an operationalization for comparison, not a claimed universal — [Nic86] and [Aik12] treat kinship and body-parts as co-central.

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

@[implicit_reducible]

instance Possession.instDecidableEqInalienabilityRank : DecidableEq InalienabilityRank

Equations

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

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

[Hei97] / [Hei09a]: 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).

@[implicit_reducible]

instance Possession.instDecidableEqSource : DecidableEq Source

Equations

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

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

@[implicit_reducible]

instance Possession.instDecidableEqAlienability : DecidableEq Alienability

Equations

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

@[implicit_reducible]

instance Possession.instReprAlienability : Repr Alienability

Equations

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

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

Equations

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

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

Coarsen the cline at a language's cut: ranks at or above cut are inalienable.

Equations

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