Heine (1997): Possession

This file formalizes the second chapter of [Hei97], on the sources of predicative possession. Possessive constructions derive by grammaticalization from eight event schemas, propositional templates for everyday situations: X takes Y, Y is located at X, X is with Y, X's Y exists, Y exists for X, Y exists from X, as for X, Y exists, and Y is X's. Each schema is a Formula giving its predicate nucleus, which participant it makes the subject, and how the other participant enters, and the contrastive properties the chapter tabulates follow from the formulas: only the Action Schema has a lexical nucleus, only Action and Location are basic rather than extended by an adjunct or modifier, and only Action and Companion encode the possessor as the subject, the others marking it by an oblique case (Schema.possessorCase). Grammaticalization follows the Overlap Model: a construction carries the source meaning alone, then both meanings, then the target meaning alone, and overlap_of_gradual derives the middle stage for any development that changes one meaning at a time and is never meaningless. The rows carry the chapter's examples, the Russian locative construction at each of the three stages (russian_stages), the Telugu division of labour between the Location Schema for physical possession and the Goal Schema for the permanent and inalienable notions of Possession.Notion (telugu_notions), and the Ewe and English cases.

The chapter's survey of source schemas in a hundred languages, the correlations between schemas and have or belong constructions, and the probabilistic generalizations about which notions each schema tends to express stay in prose: Location and Goal are the most frequent sources and Action a minority one, Location gives have constructions and Equation belong constructions, and the Existence schemas are seldom recruited for physical possession.

Implementation notes

• The formulas are the chapter's; the classification of nuclei as lexical or schematic and of the second participant's entry as core or grafted on are the chapter's criteria, applied once to each formula.
• The Source Schema, absent from the chapter's tables, is treated as an Existence schema with an ablative possessor.

References

• [Hei97]
• [Hei93]

The event schemas

inductive Heine1997.Schema : Type

The eight event schemas from which predicative possession derives.

• action : Schema
• location : Schema
• companion : Schema
• genitive : Schema
• goal : Schema
• source : Schema
• topic : Schema
• equation : Schema

@[instance_reducible]

instance Heine1997.instDecidableEqSchema : DecidableEq Schema

Equations

• Heine1997.instDecidableEqSchema x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Heine1997.instReprSchema : Repr Schema

Equations

• Heine1997.instReprSchema = { reprPrec := Heine1997.instReprSchema.repr }

def Heine1997.instReprSchema.repr : Schema → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Heine1997.instFintypeSchema : Fintype Schema

Equations

• Heine1997.instFintypeSchema = { elems := { val := ↑Heine1997.Schema.enumList, nodup := Heine1997.Schema.enumList_nodup }, complete := Heine1997.instFintypeSchema._proof_1 }

inductive Heine1997.Nucleus : Type

The predicate nucleus of a schema's formula: the lexical verb take, the locative copula be at, the existential exist, or the equative copula be.

• take : Nucleus
• beAt : Nucleus
• exist : Nucleus
• be : Nucleus

@[instance_reducible]

instance Heine1997.instDecidableEqNucleus : DecidableEq Nucleus

Equations

• Heine1997.instDecidableEqNucleus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Heine1997.instReprNucleus : Repr Nucleus

Equations

• Heine1997.instReprNucleus = { reprPrec := Heine1997.instReprNucleus.repr }

def Heine1997.instReprNucleus.repr : Nucleus → ℕ → Std.Format

Equations

• Heine1997.instReprNucleus.repr Heine1997.Nucleus.take prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Nucleus.take")).group prec✝
• Heine1997.instReprNucleus.repr Heine1997.Nucleus.beAt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Nucleus.beAt")).group prec✝
• Heine1997.instReprNucleus.repr Heine1997.Nucleus.exist prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Nucleus.exist")).group prec✝
• Heine1997.instReprNucleus.repr Heine1997.Nucleus.be prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Nucleus.be")).group prec✝

def Heine1997.Nucleus.IsLexical : Nucleus → Prop

Whether a nucleus retains lexical content: take does, the schematic predicates of location, existence, and equation do not.

Equations

• Heine1997.Nucleus.take.IsLexical = True
• Heine1997.Nucleus.beAt.IsLexical = False
• Heine1997.Nucleus.exist.IsLexical = False
• Heine1997.Nucleus.be.IsLexical = False

@[instance_reducible]

instance Heine1997.instDecidablePredNucleusIsLexical : DecidablePred Nucleus.IsLexical

Equations

• Heine1997.instDecidablePredNucleusIsLexical Heine1997.Nucleus.take = isTrue trivial
• Heine1997.instDecidablePredNucleusIsLexical Heine1997.Nucleus.beAt = isFalse Heine1997.instDecidablePredNucleusIsLexical._proof_1
• Heine1997.instDecidablePredNucleusIsLexical Heine1997.Nucleus.exist = isFalse Heine1997.instDecidablePredNucleusIsLexical._proof_2
• Heine1997.instDecidablePredNucleusIsLexical Heine1997.Nucleus.be = isFalse Heine1997.instDecidablePredNucleusIsLexical._proof_3

inductive Heine1997.Participant : Type

The two participants of a possessive situation.

• possessor : Participant
• possessee : Participant

@[instance_reducible]

instance Heine1997.instDecidableEqParticipant : DecidableEq Participant

Equations

• Heine1997.instDecidableEqParticipant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Heine1997.instReprParticipant.repr : Participant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Heine1997.instReprParticipant : Repr Participant

Equations

• Heine1997.instReprParticipant = { reprPrec := Heine1997.instReprParticipant.repr }

inductive Heine1997.Entry : Type

How the participant that is not the subject enters the formula: as the object or the locative argument of the nucleus, or grafted on as a comitative, dative, or ablative adjunct, a genitival modifier, or a topic.

• object : Entry
• locative : Entry
• comitative : Entry
• genitive : Entry
• dative : Entry
• ablative : Entry
• topic : Entry

@[instance_reducible]

instance Heine1997.instDecidableEqEntry : DecidableEq Entry

Equations

• Heine1997.instDecidableEqEntry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Heine1997.instReprEntry.repr : Entry → ℕ → Std.Format

Equations

• Heine1997.instReprEntry.repr Heine1997.Entry.object prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.object")).group prec✝
• Heine1997.instReprEntry.repr Heine1997.Entry.locative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.locative")).group prec✝
• Heine1997.instReprEntry.repr Heine1997.Entry.comitative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.comitative")).group prec✝
• Heine1997.instReprEntry.repr Heine1997.Entry.genitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.genitive")).group prec✝
• Heine1997.instReprEntry.repr Heine1997.Entry.dative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.dative")).group prec✝
• Heine1997.instReprEntry.repr Heine1997.Entry.ablative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.ablative")).group prec✝
• Heine1997.instReprEntry.repr Heine1997.Entry.topic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Entry.topic")).group prec✝

@[instance_reducible]

instance Heine1997.instReprEntry : Repr Entry

Equations

• Heine1997.instReprEntry = { reprPrec := Heine1997.instReprEntry.repr }

def Heine1997.Entry.IsCore : Entry → Prop

Whether the entry is an argument of the nucleus rather than an addition to a simpler structure.

Equations

• Heine1997.Entry.object.IsCore = True
• Heine1997.Entry.locative.IsCore = True
• Heine1997.Entry.comitative.IsCore = False
• Heine1997.Entry.genitive.IsCore = False
• Heine1997.Entry.dative.IsCore = False
• Heine1997.Entry.ablative.IsCore = False
• Heine1997.Entry.topic.IsCore = False

@[instance_reducible]

instance Heine1997.instDecidablePredEntryIsCore : DecidablePred Entry.IsCore

Equations

• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.object = isTrue trivial
• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.locative = isTrue trivial
• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.comitative = isFalse Heine1997.instDecidablePredEntryIsCore._proof_1
• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.genitive = isFalse Heine1997.instDecidablePredEntryIsCore._proof_2
• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.dative = isFalse Heine1997.instDecidablePredEntryIsCore._proof_3
• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.ablative = isFalse Heine1997.instDecidablePredEntryIsCore._proof_4
• Heine1997.instDecidablePredEntryIsCore Heine1997.Entry.topic = isFalse Heine1997.instDecidablePredEntryIsCore._proof_5

def Heine1997.Entry.case : Entry → Option Case

The case that marks an entry, when it is a case-marked oblique.

Equations

• Heine1997.Entry.locative.case = some Case.loc
• Heine1997.Entry.comitative.case = some Case.com
• Heine1997.Entry.genitive.case = some Case.gen
• Heine1997.Entry.dative.case = some Case.dat
• Heine1997.Entry.ablative.case = some Case.abl
• Heine1997.Entry.object.case = none
• Heine1997.Entry.topic.case = none

structure Heine1997.Formula : Type

A formulaic description of a schema: its nucleus, the participant it encodes as the subject, and how the other participant enters.

• nucleus : Nucleus
• subject : Participant
• entry : Entry

@[instance_reducible]

instance Heine1997.instDecidableEqFormula : DecidableEq Formula

Equations

• Heine1997.instDecidableEqFormula = Heine1997.instDecidableEqFormula.decEq

def Heine1997.instDecidableEqFormula.decEq (x✝ x✝¹ : Formula) : Decidable (x✝ = x✝¹)

Equations

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

def Heine1997.instReprFormula.repr : Formula → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Heine1997.instReprFormula : Repr Formula

Equations

• Heine1997.instReprFormula = { reprPrec := Heine1997.instReprFormula.repr }

def Heine1997.Schema.formula : Schema → Formula

The formulas of the eight schemas.

Equations

• Heine1997.Schema.action.formula = { nucleus := Heine1997.Nucleus.take, subject := Heine1997.Participant.possessor, entry := Heine1997.Entry.object }
• Heine1997.Schema.location.formula = { nucleus := Heine1997.Nucleus.beAt, subject := Heine1997.Participant.possessee, entry := Heine1997.Entry.locative }
• Heine1997.Schema.companion.formula = { nucleus := Heine1997.Nucleus.be, subject := Heine1997.Participant.possessor, entry := Heine1997.Entry.comitative }
• Heine1997.Schema.genitive.formula = { nucleus := Heine1997.Nucleus.exist, subject := Heine1997.Participant.possessee, entry := Heine1997.Entry.genitive }
• Heine1997.Schema.goal.formula = { nucleus := Heine1997.Nucleus.exist, subject := Heine1997.Participant.possessee, entry := Heine1997.Entry.dative }
• Heine1997.Schema.source.formula = { nucleus := Heine1997.Nucleus.exist, subject := Heine1997.Participant.possessee, entry := Heine1997.Entry.ablative }
• Heine1997.Schema.topic.formula = { nucleus := Heine1997.Nucleus.exist, subject := Heine1997.Participant.possessee, entry := Heine1997.Entry.topic }
• Heine1997.Schema.equation.formula = { nucleus := Heine1997.Nucleus.be, subject := Heine1997.Participant.possessee, entry := Heine1997.Entry.genitive }

def Heine1997.Schema.IsBasic (s : Schema) : Prop

A schema is basic when its second participant is an argument of the nucleus, extended when it is grafted onto a simpler structure.

Equations

• s.IsBasic = s.formula.entry.IsCore

@[instance_reducible]

instance Heine1997.instDecidablePredSchemaIsBasic : DecidablePred Schema.IsBasic

Equations

• Heine1997.instDecidablePredSchemaIsBasic s = Heine1997.instDecidablePredSchemaIsBasic._aux_1 s

def Heine1997.Schema.possessorCase (s : Schema) : Option Case

The case marking the possessor when it is not the subject.

Equations

• s.possessorCase = if s.formula.subject = Heine1997.Participant.possessee then s.formula.entry.case else none

The contrastive properties of the schemas follow from their formulas.

theorem Heine1997.isLexical_iff (s : Schema) : s.formula.nucleus.IsLexical ↔ s = Schema.action

Only the Action Schema has a lexical predicate nucleus.

theorem Heine1997.isBasic_iff (s : Schema) : s.IsBasic ↔ s = Schema.action ∨ s = Schema.location

Action and Location are the basic schemas.

theorem Heine1997.subject_possessor_iff (s : Schema) : s.formula.subject = Participant.possessor ↔ s = Schema.action ∨ s = Schema.companion

Action and Companion encode the possessor as the subject.

theorem Heine1997.possessorCase_isSome_iff (s : Schema) : s.possessorCase.isSome = true ↔ s.formula.subject = Participant.possessee ∧ s ≠ Schema.topic

A schema marks its possessor by a case exactly when the possessor is not the subject and is not merely topicalized.

The Overlap Model

A construction grammaticalizing from a source schema to a possessive target carries the source meaning alone at Stage I, both meanings at Stage II, where it is ambiguous, and the target meaning alone at Stage III.

inductive Heine1997.Meaning : Type

The meanings a construction can carry: that of its source schema and the possessive target.

• source : Meaning
• target : Meaning

@[instance_reducible]

instance Heine1997.instDecidableEqMeaning : DecidableEq Meaning

Equations

• Heine1997.instDecidableEqMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Heine1997.instReprMeaning : Repr Meaning

Equations

• Heine1997.instReprMeaning = { reprPrec := Heine1997.instReprMeaning.repr }

def Heine1997.instReprMeaning.repr : Meaning → ℕ → Std.Format

Equations

• Heine1997.instReprMeaning.repr Heine1997.Meaning.source prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Meaning.source")).group prec✝
• Heine1997.instReprMeaning.repr Heine1997.Meaning.target prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heine1997.Meaning.target")).group prec✝

@[instance_reducible]

instance Heine1997.instFintypeMeaning : Fintype Meaning

Equations

• Heine1997.instFintypeMeaning = { elems := { val := ↑Heine1997.Meaning.enumList, nodup := Heine1997.Meaning.enumList_nodup }, complete := Heine1997.instFintypeMeaning._proof_1 }

def Heine1997.stage : Fin 3 → Finset Meaning

The three stages of the Overlap Model.

Equations

• Heine1997.stage 0 = {Heine1997.Meaning.source}
• Heine1997.stage 1 = {Heine1997.Meaning.source, Heine1997.Meaning.target}
• Heine1997.stage 2 = {Heine1997.Meaning.target}

def Heine1997.Gradual (f : ℕ → Finset Meaning) : Prop

A development is gradual when consecutive stages differ in at most one meaning and no stage is meaningless.

Equations

• Heine1997.Gradual f = ∀ (i : ℕ), (f i).Nonempty ∧ (symmDiff (f i) (f (i + 1))).card ≤ 1

theorem Heine1997.overlap_of_gradual (f : ℕ → Finset Meaning) (hf : Gradual f) (h0 : f 0 = stage 0) {n : ℕ} (hn : f n = stage 2) : ∃ i ≤ n, f i = stage 1

A gradual development from the source meaning alone to the target meaning alone passes through the overlap stage.

The rows

def Heine1997.schema (r : Datum) : Option Schema

The schema a row instantiates.

Equations

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

def Heine1997.meanings (r : Datum) : Finset Meaning

The meanings a row's construction carries, read from whether the source and the target readings are available.

Equations

• Heine1997.meanings r = (if r.feature? "source" = some "true" then {Heine1997.Meaning.source} else ∅) ∪ if r.feature? "target" = some "true" then {Heine1997.Meaning.target} else ∅

def Heine1997.russianData : List (Finset Meaning)

The meaning sets of the Russian rows (73), stages I, II, and III of the Location Schema's grammaticalization.

Equations

• Heine1997.russianData = List.map Heine1997.meanings (List.filter (fun (r : Datum) => decide (r.language = "russ1263")) Heine1997.Examples.all)

theorem Heine1997.russian_stages (i : Fin 3) : stage i ∈ russianData

The Russian locative construction is attested at each stage of the Overlap Model, with the ambiguous (73c) at the overlap stage.

def Heine1997.notion (r : Datum) : Option Possession.Notion

The possessive notion a row expresses.

Equations

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

def Heine1997.teluguData : List (Schema × Possession.Notion)

The schema and notion of each Telugu row (85).

Equations

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

theorem Heine1997.telugu_notions (d : Schema × Possession.Notion) : d ∈ teluguData → (d.1 = Schema.location ↔ d.2 = Possession.Notion.physical)

Telugu divides the notions between two schemas as the chapter's generalizations expect: the Location Schema expresses physical possession and the Goal Schema, an Existence schema, the permanent and inalienable notions, never the physical one.