Cross-Linguistic Causative Typology

@cite{song-1996}

Song's typology of causative constructions, orthogonal to the force-dynamic builder classification. This module classifies how causative meaning is expressed (morphosyntactic packaging), while CausativeBuilder classifies what causative meaning is (force-dynamic mechanism).

Key Typology (§5.1-5.3)

Type	Structure	Implicative?	Example
COMPACT	Vcause ⊕ Veffect fused	Yes	English kill, Turkish -dür
AND	Two clauses, sequential	Yes	Vata le
PURP	Two clauses, purposive	No	Korean -ke ha-

The COMPACT type subsumes both lexical causatives (English kill) and morphological causatives (Turkish -dür, Japanese -ase, French faire).

Cognitive Structure (§5.3)

All causative events involve: GOAL → EVENT → RESULT

• AND type highlights: EVENT + RESULT (factual sequencing)
• PURP type highlights: GOAL + EVENT (purposive, non-implicative)
• COMPACT type: entire sequence collapsed into single predicate

inductive Phenomena.Causatives.Typology.CausativeConstructionType : Type

Morphosyntactic type of causative construction.

This is orthogonal to the force-dynamic builder: a .make builder can be realized as COMPACT (English make), AND, or PURP depending on the language.

• compact: Cause and effect fused into a single predicate. Includes lexical (kill) and morphological (-dür, -ase) causatives.
• and_: Two clauses joined sequentially. Effect clause is factual.
• purp: Two clauses, with purposive semantics. Effect clause is non-implicative (not entailed to have occurred).

• compact : CausativeConstructionType

  Cause + effect fused (lexical: kill; morphological: Turkish -dür)

• and_ : CausativeConstructionType

  Two clauses, sequential (Vata le; effect is factual)

• purp : CausativeConstructionType

  Two clauses, purposive (Korean -ke ha-; effect not entailed)

instance Phenomena.Causatives.Typology.instDecidableEqCausativeConstructionType : DecidableEq CausativeConstructionType

Equations

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

def Phenomena.Causatives.Typology.instReprCausativeConstructionType.repr : CausativeConstructionType → Nat → Std.Format

Equations

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

instance Phenomena.Causatives.Typology.instReprCausativeConstructionType : Repr CausativeConstructionType

Equations

• Phenomena.Causatives.Typology.instReprCausativeConstructionType = { reprPrec := Phenomena.Causatives.Typology.instReprCausativeConstructionType.repr }

instance Phenomena.Causatives.Typology.instBEqCausativeConstructionType : BEq CausativeConstructionType

Equations

• Phenomena.Causatives.Typology.instBEqCausativeConstructionType = { beq := Phenomena.Causatives.Typology.instBEqCausativeConstructionType.beq }

def Phenomena.Causatives.Typology.instBEqCausativeConstructionType.beq : CausativeConstructionType → CausativeConstructionType → Bool

Equations

• Phenomena.Causatives.Typology.instBEqCausativeConstructionType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Causatives.Typology.CausativeConstructionType.isImplicative : CausativeConstructionType → Bool

Whether a causative construction type is implicative.

Implicative = the cause clause entails the effect clause.

• COMPACT: Yes — kill entails death occurred
• AND: Yes — sequential structure implies effect is factual
• PURP: No — purposive structure leaves effect open

Equations

• Phenomena.Causatives.Typology.CausativeConstructionType.compact.isImplicative = true
• Phenomena.Causatives.Typology.CausativeConstructionType.and_.isImplicative = true
• Phenomena.Causatives.Typology.CausativeConstructionType.purp.isImplicative = false

inductive Phenomena.Causatives.Typology.CausativeMorphology : Type

Morphosyntactic realization of the causative morpheme.

Within COMPACT causatives, the causal element can be realized as:

• A bound morpheme (Turkish -dür, Japanese -ase)
• A free morpheme forming a tight unit (French faire)
• A lexical fusion with no separable morpheme (English kill)

• suffix : CausativeMorphology

  Bound morpheme (affix): Turkish -dür, Japanese -(s)ase

• freeMorpheme : CausativeMorphology

  Free morpheme forming tight unit: French faire

• lexical : CausativeMorphology

  No separable morpheme: English kill (lexical causative)

instance Phenomena.Causatives.Typology.instDecidableEqCausativeMorphology : DecidableEq CausativeMorphology

Equations

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

instance Phenomena.Causatives.Typology.instReprCausativeMorphology : Repr CausativeMorphology

Equations

• Phenomena.Causatives.Typology.instReprCausativeMorphology = { reprPrec := Phenomena.Causatives.Typology.instReprCausativeMorphology.repr }

def Phenomena.Causatives.Typology.instReprCausativeMorphology.repr : CausativeMorphology → Nat → Std.Format

Equations

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

def Phenomena.Causatives.Typology.instBEqCausativeMorphology.beq : CausativeMorphology → CausativeMorphology → Bool

Equations

• Phenomena.Causatives.Typology.instBEqCausativeMorphology.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Causatives.Typology.instBEqCausativeMorphology : BEq CausativeMorphology

Equations

• Phenomena.Causatives.Typology.instBEqCausativeMorphology = { beq := Phenomena.Causatives.Typology.instBEqCausativeMorphology.beq }

structure Phenomena.Causatives.Typology.CausativeConstructionDatum : Type

A cross-linguistic causative construction datum.

• language : String

  Language name

• form : String

  Surface form or morpheme

• constructionType : CausativeConstructionType

  Construction type in Song's typology

• morphology : Option CausativeMorphology

  Morphological realization (for compact types)

• gloss : String

  Gloss / translation

instance Phenomena.Causatives.Typology.instReprCausativeConstructionDatum : Repr CausativeConstructionDatum

Equations

• Phenomena.Causatives.Typology.instReprCausativeConstructionDatum = { reprPrec := Phenomena.Causatives.Typology.instReprCausativeConstructionDatum.repr }

def Phenomena.Causatives.Typology.instReprCausativeConstructionDatum.repr : CausativeConstructionDatum → Nat → Std.Format

Equations

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

instance Phenomena.Causatives.Typology.instBEqCausativeConstructionDatum : BEq CausativeConstructionDatum

Equations

• Phenomena.Causatives.Typology.instBEqCausativeConstructionDatum = { beq := Phenomena.Causatives.Typology.instBEqCausativeConstructionDatum.beq }

def Phenomena.Causatives.Typology.instBEqCausativeConstructionDatum.beq : CausativeConstructionDatum → CausativeConstructionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Causatives.Typology.instBEqCausativeConstructionDatum.beq x✝¹ x✝ = false

Cross-linguistic data

def Phenomena.Causatives.Typology.englishKill : CausativeConstructionDatum

English kill — lexical COMPACT causative (kill = cause-to-die)

Equations

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

def Phenomena.Causatives.Typology.turkishDur : CausativeConstructionDatum

Turkish -dür — morphological COMPACT causative suffix

Equations

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

def Phenomena.Causatives.Typology.japaneseAse : CausativeConstructionDatum

Japanese -(s)ase — morphological COMPACT causative suffix

Equations

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

def Phenomena.Causatives.Typology.frenchFaire : CausativeConstructionDatum

French faire — COMPACT causative with free morpheme

Equations

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

def Phenomena.Causatives.Typology.koreanKeHa : CausativeConstructionDatum

Korean -ke ha- — PURP-type causative (non-implicative)

Equations

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

def Phenomena.Causatives.Typology.vataLe : CausativeConstructionDatum

Vata le — AND-type causative (sequential, implicative)

Equations

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

def Phenomena.Causatives.Typology.allData : List CausativeConstructionDatum

Equations

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

Implicativity theorems

theorem Phenomena.Causatives.Typology.compact_is_implicative : CausativeConstructionType.compact.isImplicative = true

COMPACT causatives are implicative.

theorem Phenomena.Causatives.Typology.and_is_implicative : CausativeConstructionType.and_.isImplicative = true

AND-type causatives are implicative.

theorem Phenomena.Causatives.Typology.purp_not_implicative : CausativeConstructionType.purp.isImplicative = false

PURP-type causatives are NOT implicative.

theorem Phenomena.Causatives.Typology.englishKill_implicative : englishKill.constructionType.isImplicative = true

Per-datum verification: each datum's implicativity matches its type.

theorem Phenomena.Causatives.Typology.turkishDur_implicative : turkishDur.constructionType.isImplicative = true

theorem Phenomena.Causatives.Typology.japaneseAse_implicative : japaneseAse.constructionType.isImplicative = true

theorem Phenomena.Causatives.Typology.frenchFaire_implicative : frenchFaire.constructionType.isImplicative = true

theorem Phenomena.Causatives.Typology.koreanKeHa_not_implicative : koreanKeHa.constructionType.isImplicative = false

theorem Phenomena.Causatives.Typology.vataLe_implicative : vataLe.constructionType.isImplicative = true

theorem Phenomena.Causatives.Typology.english_ch110 : Option.map (fun (dp : Core.WALS.F110A.Datapoint) => Phenomena.Causatives.Typology.fromWALS110A✝ dp.value) (Core.WALS.F110A.lookup "eng") = some (some CausativeConstructionType.and_)

English periphrastic causatives are sequential (AND-type) per WALS 110A.

theorem Phenomena.Causatives.Typology.turkish_ch110 : Option.map (fun (dp : Core.WALS.F110A.Datapoint) => Phenomena.Causatives.Typology.fromWALS110A✝ dp.value) (Core.WALS.F110A.lookup "tur") = some (some CausativeConstructionType.purp)

Turkish periphrastic causatives are purposive (PURP-type) per WALS 110A.

theorem Phenomena.Causatives.Typology.korean_ch110 : Option.map (fun (dp : Core.WALS.F110A.Datapoint) => Phenomena.Causatives.Typology.fromWALS110A✝ dp.value) (Core.WALS.F110A.lookup "kor") = some (some CausativeConstructionType.purp)

Korean periphrastic causatives are purposive (PURP-type) per WALS 110A, consistent with the -ke ha- construction being PURP in Song's typology.

theorem Phenomena.Causatives.Typology.korean_ch110_matches_datum : Option.map (fun (dp : Core.WALS.F110A.Datapoint) => Phenomena.Causatives.Typology.fromWALS110A✝ dp.value) (Core.WALS.F110A.lookup "kor") = some (some koreanKeHa.constructionType)

Korean's WALS 110A classification matches our datum's construction type.

theorem Phenomena.Causatives.Typology.english_ch111 : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_hasCompact✝ dp.value) (Core.WALS.F111A.lookup "eng") = some true

English has nonperiphrastic (compact) causatives per WALS 111A.

theorem Phenomena.Causatives.Typology.english_ch111_morphology : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_morphology✝ dp.value) (Core.WALS.F111A.lookup "eng") = some (some CausativeMorphology.suffix)

English nonperiphrastic causatives are morphological per WALS 111A (corresponding to lexical causatives like kill).

theorem Phenomena.Causatives.Typology.turkish_ch111 : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_hasCompact✝ dp.value) (Core.WALS.F111A.lookup "tur") = some true

Turkish has nonperiphrastic (compact) causatives per WALS 111A.

theorem Phenomena.Causatives.Typology.turkish_ch111_morphology : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_morphology✝ dp.value) (Core.WALS.F111A.lookup "tur") = some turkishDur.morphology

Turkish nonperiphrastic causatives are morphological (suffix -dür) per WALS 111A, matching our datum.

theorem Phenomena.Causatives.Typology.japanese_ch111 : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_hasCompact✝ dp.value) (Core.WALS.F111A.lookup "jpn") = some true

Japanese has nonperiphrastic (compact) causatives per WALS 111A.

theorem Phenomena.Causatives.Typology.japanese_ch111_morphology : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_morphology✝ dp.value) (Core.WALS.F111A.lookup "jpn") = some japaneseAse.morphology

Japanese nonperiphrastic causatives are morphological (suffix -(s)ase) per WALS 111A, matching our datum.

theorem Phenomena.Causatives.Typology.french_ch111 : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_hasCompact✝ dp.value) (Core.WALS.F111A.lookup "fre") = some true

French has nonperiphrastic (compact) causatives per WALS 111A. WALS classifies French as both (morphological and compound).

theorem Phenomena.Causatives.Typology.korean_ch111 : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_hasCompact✝ dp.value) (Core.WALS.F111A.lookup "kor") = some true

Korean has nonperiphrastic (compact) causatives per WALS 111A, in addition to the periphrastic -ke ha- construction.

theorem Phenomena.Causatives.Typology.korean_ch111_morphology : Option.map (fun (dp : Core.WALS.F111A.Datapoint) => Phenomena.Causatives.Typology.fromWALS111A_morphology✝ dp.value) (Core.WALS.F111A.lookup "kor") = some (some CausativeMorphology.suffix)

Korean nonperiphrastic causatives are morphological per WALS 111A.

theorem Phenomena.Causatives.Typology.ch110_total : Phenomena.Causatives.Typology.ch110✝.length = 118

WALS 110A total: 118 languages with periphrastic causative data.

theorem Phenomena.Causatives.Typology.ch111_total : Phenomena.Causatives.Typology.ch111✝.length = 310

WALS 111A total: 310 languages with nonperiphrastic causative data.

theorem Phenomena.Causatives.Typology.ch110_sequentialOnly : (List.filter (fun (x : Core.WALS.F110A.Datapoint) => x.value == Core.WALS.F110A.PeriphrasticCausativeType.sequentialOnly) Phenomena.Causatives.Typology.ch110✝).length = 35

WALS 110A: 35 languages have sequential-only periphrastic causatives.

theorem Phenomena.Causatives.Typology.ch110_purposiveOnly : (List.filter (fun (x : Core.WALS.F110A.Datapoint) => x.value == Core.WALS.F110A.PeriphrasticCausativeType.purposiveOnly) Phenomena.Causatives.Typology.ch110✝).length = 68

WALS 110A: 68 languages have purposive-only periphrastic causatives.

theorem Phenomena.Causatives.Typology.ch110_both : (List.filter (fun (x : Core.WALS.F110A.Datapoint) => x.value == Core.WALS.F110A.PeriphrasticCausativeType.both) Phenomena.Causatives.Typology.ch110✝).length = 15

WALS 110A: 15 languages have both sequential and purposive.

theorem Phenomena.Causatives.Typology.ch111_morphologicalOnly : (List.filter (fun (x : Core.WALS.F111A.Datapoint) => x.value == Core.WALS.F111A.NonperiphrCausativeType.morphologicalOnly) Phenomena.Causatives.Typology.ch111✝).length = 254

WALS 111A: 254 languages have morphological-only nonperiphrastic causatives.

theorem Phenomena.Causatives.Typology.ch111_compoundOnly : (List.filter (fun (x : Core.WALS.F111A.Datapoint) => x.value == Core.WALS.F111A.NonperiphrCausativeType.compoundOnly) Phenomena.Causatives.Typology.ch111✝).length = 9

WALS 111A: 9 languages have compound-only nonperiphrastic causatives.

theorem Phenomena.Causatives.Typology.ch111_both : (List.filter (fun (x : Core.WALS.F111A.Datapoint) => x.value == Core.WALS.F111A.NonperiphrCausativeType.both) Phenomena.Causatives.Typology.ch111✝).length = 24

WALS 111A: 24 languages have both morphological and compound.

theorem Phenomena.Causatives.Typology.ch111_neither : (List.filter (fun (x : Core.WALS.F111A.Datapoint) => x.value == Core.WALS.F111A.NonperiphrCausativeType.neither) Phenomena.Causatives.Typology.ch111✝).length = 23

WALS 111A: 23 languages have neither morphological nor compound.

theorem Phenomena.Causatives.Typology.purp_dominates_and : (List.filter (fun (x : Core.WALS.F110A.Datapoint) => x.value == Core.WALS.F110A.PeriphrasticCausativeType.purposiveOnly) Phenomena.Causatives.Typology.ch110✝).length > (List.filter (fun (x : Core.WALS.F110A.Datapoint) => x.value == Core.WALS.F110A.PeriphrasticCausativeType.sequentialOnly) Phenomena.Causatives.Typology.ch110✝¹).length

Purposive periphrastic causatives (PURP-type) are the dominant pattern cross-linguistically, outnumbering sequential (AND-type) roughly 2:1.

theorem Phenomena.Causatives.Typology.morphological_dominates : (List.filter (fun (x : Core.WALS.F111A.Datapoint) => x.value == Core.WALS.F111A.NonperiphrCausativeType.morphologicalOnly) Phenomena.Causatives.Typology.ch111✝).length * 100 / Phenomena.Causatives.Typology.ch111✝¹.length ≥ 81

Morphological causatives overwhelmingly dominate nonperiphrastic strategies: 254 out of 310 languages (82%) have morphological-only.