Song 1996: Causative Construction Typology

[Son96]

[Son96]'s typology of causative constructions, classifying how causative meaning is expressed (morphosyntactic packaging). Three types: COMPACT (English kill, Turkish -dür), AND (Vata le), PURP (Korean -ke ha-).

This file owns Song's typology + 6 per-language datums + WALS Ch 110A/111A grounding theorems + the Comrie-Song complexity bridge. The orthogonal Pylkkänen 2008 Voice-bundling × selection typology lives at Studies/Pylkkanen2008.lean §13 (Pylkkänen's substrate; not subsumed by Song's). Comrie 1989's compact/morphological/ periphrastic complexity scale lives at Semantics/Causation/Morphological.CausativeComplexity (the substrate Song's toComplexity projects into).

This file replaces a previous 41-LOC Studies/Song1996.lean that was an editorial-bridge anti-pattern (HahnDegenFutrell ↔ Causation Typology). The Causation/Typology.lean file (542 LOC) was simultaneously dissolved and renamed here.

Cross-paper context (deferred)

Song's COMPACT/AND/PURP three-way is defensible but coarse, and the file-level typology should be read against:

• [dixon-2000-causatives]: nine semantic parameters × three formal types (lexical/morphological/periphrastic). Dixon's parameters cut across Song's COMPACT (e.g., directness, naturalness, volition) and arguably reduce Song's three-way to a special case of his finer parameter space.
• [shibatani-pardeshi-2002]: a causative continuum (direct → sociative → indirect) where the SOCIATIVE middle category (joint-action causation: Japanese -(s)ase in its assistive reading; Marathi sociative; dedicated Bantu/Korean/Tamil sociative morphology) is missing from Song's tripartite partition. Song collapses sociative into PURP or COMPACT depending on language, losing a robust typological generalization.
• [WM17], [cuervo-2014]: generative-side updates of Pylkkänen 2008's Voice-bundling × selection typology — see Pylkkanen2008.lean §13.

The internal CausativeMorphology enum (suffix / freeMorpheme / lexical) within COMPACT is closer to current field consensus than Song's COMPACT/AND/ PURP partition itself — the file documents the typology Song proposed, not the typology the field has converged on.

Key Typology (Song §5.1-5.3 — UNVERIFIED location refs)

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

inductive Song1996.CausativeConstructionType : Type

Morphosyntactic type of causative construction (Song 1996).

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

@[implicit_reducible]

instance Song1996.instDecidableEqCausativeConstructionType : DecidableEq CausativeConstructionType

Equations

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

def Song1996.instReprCausativeConstructionType.repr : CausativeConstructionType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Song1996.instReprCausativeConstructionType : Repr CausativeConstructionType

Equations

• Song1996.instReprCausativeConstructionType = { reprPrec := Song1996.instReprCausativeConstructionType.repr }

def Song1996.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

• Song1996.CausativeConstructionType.compact.isImplicative = true
• Song1996.CausativeConstructionType.and_.isImplicative = true
• Song1996.CausativeConstructionType.purp.isImplicative = false

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

Note: CausativeMorphology.lexical (no separable morpheme) and Semantics/Causation/Morphological.CausativeComplexity.lexical (most-compact end of Comrie's complexity scale) share the constructor name lexical but are NOT semantically equivalent. The first is a morpheme-shape claim; the second is a construction-complexity claim. English kill satisfies both, but the inferential content differs: one says "no separable causal morpheme", the other says "construction is at the most-compact end of Comrie's continuum".

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

@[implicit_reducible]

instance Song1996.instDecidableEqCausativeMorphology : DecidableEq CausativeMorphology

Equations

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

def Song1996.instReprCausativeMorphology.repr : CausativeMorphology → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Song1996.instReprCausativeMorphology : Repr CausativeMorphology

Equations

• Song1996.instReprCausativeMorphology = { reprPrec := Song1996.instReprCausativeMorphology.repr }

structure Song1996.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

@[implicit_reducible]

instance Song1996.instReprCausativeConstructionDatum : Repr CausativeConstructionDatum

Equations

• Song1996.instReprCausativeConstructionDatum = { reprPrec := Song1996.instReprCausativeConstructionDatum.repr }

def Song1996.instReprCausativeConstructionDatum.repr : CausativeConstructionDatum → ℕ → Std.Format

Equations

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

def Song1996.instBEqCausativeConstructionDatum.beq : CausativeConstructionDatum → CausativeConstructionDatum → Bool

Equations

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

@[implicit_reducible]

instance Song1996.instBEqCausativeConstructionDatum : BEq CausativeConstructionDatum

Equations

• Song1996.instBEqCausativeConstructionDatum = { beq := Song1996.instBEqCausativeConstructionDatum.beq }

Cross-linguistic data

def Song1996.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 Song1996.turkishDur : CausativeConstructionDatum

Turkish -dür — morphological COMPACT causative suffix

Equations

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

def Song1996.japaneseAse : CausativeConstructionDatum

Japanese -(s)ase — morphological COMPACT causative suffix

Equations

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

def Song1996.frenchFaire : CausativeConstructionDatum

French faire — COMPACT causative with free morpheme. NB: this is the empirically disputed boundary case — Song calls French faire a free-morpheme COMPACT, while Comrie 1989 / Folli & Harley 2005 analyse French faire-V as periphrastic (two words, analytic). The toComplexity bridge below maps it to morphological, lossily collapsing the disagreement.

Equations

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

def Song1996.koreanKeHa : CausativeConstructionDatum

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

Equations

• Song1996.koreanKeHa = { language := "Korean", form := "-ke ha-", constructionType := Song1996.CausativeConstructionType.purp, gloss := "wus-ke ha- 'smile-PURP do = cause to smile'" }

def Song1996.vataLe : CausativeConstructionDatum

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

Equations

• Song1996.vataLe = { language := "Vata", form := "le", constructionType := Song1996.CausativeConstructionType.and_, gloss := "le ... 'and' (overt coordinator)" }

def Song1996.allData : List CausativeConstructionDatum

Equations

• Song1996.allData = [Song1996.englishKill, Song1996.turkishDur, Song1996.japaneseAse, Song1996.frenchFaire, Song1996.koreanKeHa, Song1996.vataLe]

Implicativity theorems

theorem Song1996.compact_is_implicative : CausativeConstructionType.compact.isImplicative = true

COMPACT causatives are implicative.

theorem Song1996.and_is_implicative : CausativeConstructionType.and_.isImplicative = true

AND-type causatives are implicative.

theorem Song1996.purp_not_implicative : CausativeConstructionType.purp.isImplicative = false

PURP-type causatives are NOT implicative.

theorem Song1996.english_ch110 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => Song1996.fromWALS110A✝ dp.value) (Data.WALS.F110A.lookup "eng") = some (some CausativeConstructionType.and_)

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

theorem Song1996.turkish_ch110 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => Song1996.fromWALS110A✝ dp.value) (Data.WALS.F110A.lookup "tur") = some (some CausativeConstructionType.purp)

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

theorem Song1996.korean_ch110 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => Song1996.fromWALS110A✝ dp.value) (Data.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 Song1996.korean_ch110_matches_datum : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => Song1996.fromWALS110A✝ dp.value) (Data.WALS.F110A.lookup "kor") = some (some koreanKeHa.constructionType)

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

theorem Song1996.english_ch111 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_hasCompact✝ dp.value) (Data.WALS.F111A.lookup "eng") = some true

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

theorem Song1996.english_ch111_morphology : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_morphology✝ dp.value) (Data.WALS.F111A.lookup "eng") = some (some CausativeMorphology.suffix)

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

theorem Song1996.turkish_ch111 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_hasCompact✝ dp.value) (Data.WALS.F111A.lookup "tur") = some true

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

theorem Song1996.turkish_ch111_morphology : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_morphology✝ dp.value) (Data.WALS.F111A.lookup "tur") = some turkishDur.morphology

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

theorem Song1996.japanese_ch111 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_hasCompact✝ dp.value) (Data.WALS.F111A.lookup "jpn") = some true

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

theorem Song1996.japanese_ch111_morphology : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_morphology✝ dp.value) (Data.WALS.F111A.lookup "jpn") = some japaneseAse.morphology

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

theorem Song1996.french_ch111 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_hasCompact✝ dp.value) (Data.WALS.F111A.lookup "fre") = some true

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

theorem Song1996.korean_ch111 : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_hasCompact✝ dp.value) (Data.WALS.F111A.lookup "kor") = some true

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

theorem Song1996.korean_ch111_morphology : Option.map (fun (dp : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => Song1996.fromWALS111A_morphology✝ dp.value) (Data.WALS.F111A.lookup "kor") = some (some CausativeMorphology.suffix)

Korean nonperiphrastic causatives are morphological per WALS 111A.

theorem Song1996.ch110_total : Song1996.ch110✝.length = 118

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

theorem Song1996.ch111_total : Song1996.ch111✝.length = 310

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

theorem Song1996.ch110_sequentialOnly : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => x.value == Data.WALS.F110A.PeriphrasticCausativeType.sequentialOnly) Song1996.ch110✝).length = 35

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

theorem Song1996.ch110_purposiveOnly : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => x.value == Data.WALS.F110A.PeriphrasticCausativeType.purposiveOnly) Song1996.ch110✝).length = 68

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

theorem Song1996.ch110_both : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => x.value == Data.WALS.F110A.PeriphrasticCausativeType.both) Song1996.ch110✝).length = 15

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

theorem Song1996.ch111_morphologicalOnly : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => x.value == Data.WALS.F111A.NonperiphrCausativeType.morphologicalOnly) Song1996.ch111✝).length = 254

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

theorem Song1996.ch111_compoundOnly : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => x.value == Data.WALS.F111A.NonperiphrCausativeType.compoundOnly) Song1996.ch111✝).length = 9

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

theorem Song1996.ch111_both : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => x.value == Data.WALS.F111A.NonperiphrCausativeType.both) Song1996.ch111✝).length = 24

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

theorem Song1996.ch111_neither : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => x.value == Data.WALS.F111A.NonperiphrCausativeType.neither) Song1996.ch111✝).length = 23

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

theorem Song1996.purp_dominates_and : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => x.value == Data.WALS.F110A.PeriphrasticCausativeType.purposiveOnly) Song1996.ch110✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F110A.PeriphrasticCausativeType) => x.value == Data.WALS.F110A.PeriphrasticCausativeType.sequentialOnly) Song1996.ch110✝).length

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

theorem Song1996.morphological_dominates : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F111A.NonperiphrCausativeType) => x.value == Data.WALS.F111A.NonperiphrCausativeType.morphologicalOnly) Song1996.ch111✝).length * 100 / Song1996.ch111✝.length ≥ 81

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

def Song1996.CausativeConstructionType.toComplexity : CausativeConstructionType → Causation.Morphological.CausativeComplexity

Song's construction types map to [Com89]'s complexity scale.

The mapping is many-to-one and lossy at the COMPACT/freeMorpheme boundary: French faire-V is compact + freeMorpheme in Song's typology but periphrastic (analytic, two-word) in Comrie's. We collapse this disagreement by mapping COMPACT → morphological uniformly; the cost is invisibility for the faire case.

See [folli-harley-2005] for the syntactic-structure dispute over French faire-infinitive vs faire-par that this collapse obscures.

Equations

• Song1996.CausativeConstructionType.compact.toComplexity = Causation.Morphological.CausativeComplexity.morphological
• Song1996.CausativeConstructionType.and_.toComplexity = Causation.Morphological.CausativeComplexity.periphrastic
• Song1996.CausativeConstructionType.purp.toComplexity = Causation.Morphological.CausativeComplexity.periphrastic

theorem Song1996.multiclause_is_periphrastic (t : CausativeConstructionType) : t ≠ CausativeConstructionType.compact → t.toComplexity = Causation.Morphological.CausativeComplexity.periphrastic

All non-compact (multi-clause) types are periphrastic.

theorem Song1996.compact_not_periphrastic : CausativeConstructionType.compact.toComplexity ≠ Causation.Morphological.CausativeComplexity.periphrastic

Compact causatives are at most morphological — never periphrastic.

theorem Song1996.song_multiclause_both_periphrastic : CausativeConstructionType.and_.toComplexity = Causation.Morphological.CausativeComplexity.periphrastic ∧ CausativeConstructionType.purp.toComplexity = Causation.Morphological.CausativeComplexity.periphrastic

Both multi-clause Song types map to Comrie's periphrastic. Relocated here from Studies/Comrie1989.lean per the chronology-discipline rule (Comrie 1989 cannot cite Song 1996; the cross-paper bridge belongs in the later paper's study file).