Documentation

Linglib.Theories.Semantics.Causation.Morphological

Morphological Causation: Causative Construction Typology #

@cite{comrie-1989} @cite{song-1996} @cite{krejci-2012}

Causative constructions cross-linguistically vary along two orthogonal axes: morphological complexity (compact → analytic) and semantic directness (direct → indirect mediation). @cite{comrie-1989}'s central generalization: more complex morphology correlates with more indirect causation.

Causer Type #

Causative constructions are sensitive to the causer's intentionality and ontological category. Following @cite{hafeez-2025}, we distinguish:

intentional human (IHCr): volitional, controlled action → full agentivity
accidental human (AHCr): unintentional, no control → marginal agentivity
natural force (NFCr): non-human, non-volitional → non-agentive

The key dimension is intentionality, not ontological type: IHCr and AHCr are both human but differ in agentivity. This three-way distinction drives construction selection in Urdu and other languages.

Causee/Affectee Type #

The second participant in a causal chain (causee or affectee) varies in four levels of control and animacy, following @cite{hafeez-2025}:

controlling human (ContrHCEAF): exercises control over the induced action
physically impacted human (PhysImpHCEAF): involuntarily coerced
psychologically impacted human (PsychImpHCEAF): mentally affected
inanimate (InanCEAF): no volition or sentience

Agentivity #

Agentivity decomposes into intentionality × control (following @cite{van-valin-wilkins-1996}). Three degrees:

full: intentional causer (IHCr)
marginal: accidental human (AHCr) or natural force (NFCr)
partial/induced: causee exercises control under causer's influence

Bridges #

CauserType.toCausalSource → CausalSource (psych causation)
CauserType.toAgentivityNode → AgentivityNode (agentivity lattice)
CauserType.volitionality → Volitionality (root dimensions)
CauserType.agentivityDegree → AgentivityDegree
CausativeConstruction bundles complexity + mediation + causer/causee restrictions for cross-linguistic comparison
comrie_monotone formalizes the compact-diffuse correlation

Intransitivization (@cite{krejci-2012}) #

The causative/inchoative alternation has two directions: causativization (adding an external cause) and intransitivization (removing or coidentifying it). @cite{krejci-2012}'s central insight: intransitive variants are NOT structurally uniform. Reflexive intransitives (German sich, Hindi apne-aap) coidentify causer and causee, retaining bieventive structure. Anticausative intransitives remove the external cause entirely, yielding monoeventive structure.

IntransitivizationType distinguishes reflexive, anticausative, and unmarked intransitivization
Three diagnostics (again/re- ambiguity, negation over CAUSE, "by itself") all detect the causer position retained by reflexive intransitives but absent from anticausatives

inductive Semantics.Causation.Morphological.CauserType :

Causer type distinguished by intentionality and ontological category.

The key dimension is intentionality: IHCr and AHCr are both human but have fundamentally different agentivity profiles. NFCr is non-human and non-intentional.

This three-way distinction drives construction selection in Urdu (@cite{hafeez-2025}) and other languages.

intentionalHuman : CauserType
accidentalHuman : CauserType
naturalForce : CauserType

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqCauserType :

DecidableEq CauserType

Equations

Semantics.Causation.Morphological.instDecidableEqCauserType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprCauserType :

Repr CauserType

Equations

Semantics.Causation.Morphological.instReprCauserType = { reprPrec := Semantics.Causation.Morphological.instReprCauserType.repr }

def Semantics.Causation.Morphological.instReprCauserType.repr :

CauserType → ℕ → Std.Format

Equations

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

Instances For

inductive Semantics.Causation.Morphological.CauseeAffecteeType :

Causee/affectee type: four levels of control and animacy.

@cite{hafeez-2025}'s four-way distinction captures the gradient of the second participant's autonomy in a causal chain. A controlling causee reduces the causer's responsibility; an inanimate affectee increases it.

controllingHuman : CauseeAffecteeType
physImpactHuman : CauseeAffecteeType
psychImpactHuman : CauseeAffecteeType
inanimate : CauseeAffecteeType

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqCauseeAffecteeType :

DecidableEq CauseeAffecteeType

Equations

Semantics.Causation.Morphological.instDecidableEqCauseeAffecteeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.Morphological.instReprCauseeAffecteeType.repr :

CauseeAffecteeType → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprCauseeAffecteeType :

Repr CauseeAffecteeType

Equations

Semantics.Causation.Morphological.instReprCauseeAffecteeType = { reprPrec := Semantics.Causation.Morphological.instReprCauseeAffecteeType.repr }

inductive Semantics.Causation.Morphological.AgentivityDegree :

Degree of agentivity, decomposed from intentionality × control.

@cite{hafeez-2025}: "an intentional causer displays full agentivity, an accidental causer shows reduced or marginal agentivity, and a causee/affectee who exerts control displays induced or partial agentivity."

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqAgentivityDegree :

DecidableEq AgentivityDegree

Equations

Semantics.Causation.Morphological.instDecidableEqAgentivityDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprAgentivityDegree :

Repr AgentivityDegree

Equations

Semantics.Causation.Morphological.instReprAgentivityDegree = { reprPrec := Semantics.Causation.Morphological.instReprAgentivityDegree.repr }

def Semantics.Causation.Morphological.instReprAgentivityDegree.repr :

AgentivityDegree → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Causation.Morphological.CauserType.agentivityDegree :

CauserType → AgentivityDegree

Causer type determines causer's agentivity degree.

Equations

Instances For

def Semantics.Causation.Morphological.CauseeAffecteeType.hasInducedAgentivity :

CauseeAffecteeType → Bool

A controlling causee has partial (induced) agentivity; all other causee types have no independent agentivity.

Equations

Semantics.Causation.Morphological.CauseeAffecteeType.controllingHuman.hasInducedAgentivity = true
x✝.hasInducedAgentivity = false

Instances For

inductive Semantics.Causation.Morphological.Mediation :

Directness of causal mediation between causer and result.

@cite{comrie-1989}: direct causation involves no intermediary — the causer brings about the result without an intervening causee decision or action. Indirect causation involves a mediating causee who retains some autonomy over the caused event.

direct : Mediation
indirect : Mediation

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqMediation :

DecidableEq Mediation

Equations

Semantics.Causation.Morphological.instDecidableEqMediation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.Morphological.instReprMediation.repr :

Mediation → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprMediation :

Equations

Semantics.Causation.Morphological.instReprMediation = { reprPrec := Semantics.Causation.Morphological.instReprMediation.repr }

def Semantics.Causation.Morphological.Mediation.rank :

Mediation → ℕ

Numeric rank: direct (0) < indirect (1). Used in comrie_monotone to express the co-variation of complexity and indirectness as a proper ordering rather than a disjunction.

Equations

Instances For

inductive Semantics.Causation.Morphological.CausativeComplexity :

Morphological complexity of a causative construction.

@cite{comrie-1989}'s compact-to-analytic continuum:

lexical: suppletive or idiosyncratic (kill/die, fell/fall)
morphological: productive affix (Urdu -aa, Japanese -(s)ase)
periphrastic: analytic multi-word (English "make X do Y")

Ordered from compact to analytic.

Naming-collision note: CausativeComplexity.lexical (this constructor) and Phenomena/Causation/Studies/Song1996.CausativeMorphology.lexical share the constructor name lexical but encode different claims. CausativeComplexity.lexical is a construction-level claim — "this causative construction sits at the most-compact end of Comrie's continuum"; Song's CausativeMorphology.lexical is a morpheme-shape claim — "no separable causal morpheme exists". English kill satisfies both, but the inferential content differs. The two enums are NOT interconvertible; the lossy CausativeConstructionType.toComplexity bridge in Studies/Song1996.lean collapses Song's compact / freeMorpheme (e.g. French faire-V) into CausativeComplexity.morphological, even though @cite{folli-harley-2005} analyse French faire as periphrastic.

lexical : CausativeComplexity
morphological : CausativeComplexity
periphrastic : CausativeComplexity

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqCausativeComplexity :

DecidableEq CausativeComplexity

Equations

Semantics.Causation.Morphological.instDecidableEqCausativeComplexity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.Morphological.instReprCausativeComplexity.repr :

CausativeComplexity → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprCausativeComplexity :

Repr CausativeComplexity

Equations

Semantics.Causation.Morphological.instReprCausativeComplexity = { reprPrec := Semantics.Causation.Morphological.instReprCausativeComplexity.repr }

def Semantics.Causation.Morphological.CausativeComplexity.toNat :

CausativeComplexity → ℕ

Numeric encoding: lexical (0) < morphological (1) < periphrastic (2).

Equations

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instLinearOrderCausativeComplexity :

LinearOrder CausativeComplexity

Equations

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

structure Semantics.Causation.Morphological.CausativeConstruction :

A causative construction bundles morphological complexity with semantic parameters that govern its use.

Each language's causative system is a list of CausativeConstruction values — e.g., Urdu has 7 (acceptability study), Japanese has 3.

complexity : CausativeComplexity
Morphological complexity (compact → analytic)
mediation : Mediation
Direct vs. indirect mediation
causerRestriction : Option CauserType
Restriction on causer type (none = unrestricted)
causeeRestriction : Option CauseeAffecteeType
Required causee/affectee type (none = unrestricted)

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqCausativeConstruction :

DecidableEq CausativeConstruction

Equations

Semantics.Causation.Morphological.instDecidableEqCausativeConstruction = Semantics.Causation.Morphological.instDecidableEqCausativeConstruction.decEq

def Semantics.Causation.Morphological.instDecidableEqCausativeConstruction.decEq (x✝ x✝¹ : CausativeConstruction) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprCausativeConstruction :

Repr CausativeConstruction

Equations

Semantics.Causation.Morphological.instReprCausativeConstruction = { reprPrec := Semantics.Causation.Morphological.instReprCausativeConstruction.repr }

def Semantics.Causation.Morphological.instReprCausativeConstruction.repr :

CausativeConstruction → ℕ → Std.Format

Equations

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

Instances For

structure Semantics.Causation.Morphological.SemanticPrototype :

A semantic prototype specifies the combination of semantic variables under which a construction receives its peak acceptability rating or is preferentially produced.

-- UNVERIFIED: table number @cite{hafeez-2025}: each construction has a (possibly empty) set of features that define its prototype. A prototype is "hypothesized" when the acceptability peak exceeds 50% ceiling for a scene type.

Prototypes use both positive (e.g., [+IHCr]) and negative (e.g., [-IHCr]) feature specifications. Both are represented as lists: presentCausers/absentCausers etc.

presentCausers : List CauserType
Causer types that must be present (e.g., [+IHCr])
absentCausers : List CauserType
Causer types that must be absent (e.g., [-IHCr])
presentCausees : List CauseeAffecteeType
Causee/affectee types that must be present
absentCausees : List CauseeAffecteeType
Causee/affectee types that must be absent
requiresMediation : Option Bool
Whether mediation is part of the prototype

Instances For

def Semantics.Causation.Morphological.instDecidableEqSemanticPrototype.decEq (x✝ x✝¹ : SemanticPrototype) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqSemanticPrototype :

DecidableEq SemanticPrototype

Equations

Semantics.Causation.Morphological.instDecidableEqSemanticPrototype = Semantics.Causation.Morphological.instDecidableEqSemanticPrototype.decEq

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprSemanticPrototype :

Repr SemanticPrototype

Equations

Semantics.Causation.Morphological.instReprSemanticPrototype = { reprPrec := Semantics.Causation.Morphological.instReprSemanticPrototype.repr }

def Semantics.Causation.Morphological.instReprSemanticPrototype.repr :

SemanticPrototype → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Causation.Morphological.comrie_monotone (c1 c2 : CausativeConstruction) :

Comrie's monotonicity (@cite{comrie-1989}): within a single language, if construction A is morphologically more compact than construction B, then A encodes at least as direct causation as B.

More compact morphology correlates with more direct causation: compactness and directness co-vary monotonically. Stated as an ordering on mediation rank (direct = 0 < indirect = 1).

Equations

Semantics.Causation.Morphological.comrie_monotone c1 c2 = (c1.complexity < c2.complexity → c1.mediation.rank ≤ c2.mediation.rank)

Instances For

inductive Semantics.Causation.Morphological.CauseeSlot :

Grammatical relation slots available for causee assignment, ordered from highest to lowest on the hierarchy.

@cite{comrie-1989}: when a verb is causativized, the original subject (S or A) is demoted to the next available slot on the grammatical relations hierarchy. The slot depends on the base verb's valency — higher valency leaves fewer slots open:

Intransitive base (valency 1): causee → direct object
Transitive base (valency 2): causee → indirect object (DO occupied)
Ditransitive base (valency 3): causee → oblique (DO, IO occupied)

This hierarchy is attested across typologically diverse languages: Turkish, French, Dargwa, Japanese, among others.

directObject : CauseeSlot
indirectObject : CauseeSlot
oblique : CauseeSlot

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqCauseeSlot :

DecidableEq CauseeSlot

Equations

Semantics.Causation.Morphological.instDecidableEqCauseeSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.Morphological.instReprCauseeSlot.repr :

CauseeSlot → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprCauseeSlot :

Repr CauseeSlot

Equations

Semantics.Causation.Morphological.instReprCauseeSlot = { reprPrec := Semantics.Causation.Morphological.instReprCauseeSlot.repr }

def Semantics.Causation.Morphological.CauseeSlot.rank :

CauseeSlot → ℕ

Rank on the GR hierarchy: DO (2) > IO (1) > OBL (0).

Equations

Instances For

def Semantics.Causation.Morphological.causeeDemotion :

ℕ → CauseeSlot

Predict causee slot from base verb valency.

@cite{comrie-1989}: the causee occupies the highest available slot not already filled by the base verb's arguments.

valency 1 (intransitive): S is the sole argument → causee = DO
valency 2 (transitive): S + DO filled → causee = IO
valency ≥ 3 (ditransitive): S + DO + IO filled → causee = OBL

Equations

Instances For

theorem Semantics.Causation.Morphological.causee_demotion_monotone (v1 v2 : Fin 4) :

↑v1 ≥ 1 → v1 < v2 → (causeeDemotion ↑v2).rank ≤ (causeeDemotion ↑v1).rank

Monotonicity: higher base valency → lower causee slot. Proved for the bounded range 1 ≤ v1 < v2 ≤ 3.

def Semantics.Causation.Morphological.CauserType.toCausalSource :

CauserType → Psych.CausalSource

All causer types are "external" in @cite{kim-2024}'s sense.

The causer type taxonomy refines CausalSource.external: psych verbs' internal source (mental representation) is not a causer type in the morphological causation sense.

Equations

Instances For

def Semantics.Causation.Morphological.CauserType.volitionality :

CauserType → Lexical.Roots.Volitionality

Intentional human causers are volitional; accidental and natural force causers are not.

Equations

Instances For

def Semantics.Causation.Morphological.CauserType.toAgentivityNode :

CauserType → ArgumentStructure.AgentivityLattice.AgentivityNode

Intentional human causers map to the agentive pole of the lattice (volition + sentience + instigation); accidental humans retain sentience but lack volition; natural forces have instigation only.

Equations

Semantics.Causation.Morphological.CauserType.intentionalHuman.toAgentivityNode = { volition := true, sentience := true, instigation := true, motion := false }
Semantics.Causation.Morphological.CauserType.accidentalHuman.toAgentivityNode = { volition := false, sentience := true, instigation := true, motion := false }
Semantics.Causation.Morphological.CauserType.naturalForce.toAgentivityNode = { volition := false, sentience := false, instigation := true, motion := false }

Instances For

theorem Semantics.Causation.Morphological.intentional_max_agentivity :

CauserType.intentionalHuman.toAgentivityNode.volition = true ∧ CauserType.intentionalHuman.toAgentivityNode.sentience = true ∧ CauserType.intentionalHuman.toAgentivityNode.instigation = true

Intentional human causers have maximal agentivity among causer types.

theorem Semantics.Causation.Morphological.accidental_sentient_not_volitional :

CauserType.accidentalHuman.toAgentivityNode.sentience = true ∧ CauserType.accidentalHuman.toAgentivityNode.volition = false

Accidental human causers retain sentience but lack volition.

theorem Semantics.Causation.Morphological.naturalForce_instigation_only :

CauserType.naturalForce.toAgentivityNode = { volition := false, sentience := false, instigation := true, motion := false }

Natural force causers have only instigation (no sentience, no volition).

theorem Semantics.Causation.Morphological.all_causers_external (ct : CauserType) :

ct.toCausalSource = Psych.CausalSource.external

All causer types project to external CausalSource.

theorem Semantics.Causation.Morphological.intentional_full_agentivity :

CauserType.intentionalHuman.agentivityDegree = AgentivityDegree.full

IHCr has full agentivity; AHCr and NFCr have marginal.

theorem Semantics.Causation.Morphological.accidental_marginal_agentivity :

CauserType.accidentalHuman.agentivityDegree = AgentivityDegree.marginal

theorem Semantics.Causation.Morphological.naturalForce_marginal_agentivity :

CauserType.naturalForce.agentivityDegree = AgentivityDegree.marginal

theorem Semantics.Causation.Morphological.controlling_has_induced :

CauseeAffecteeType.controllingHuman.hasInducedAgentivity = true

Controlling causees have induced agentivity; all other causee types do not.

theorem Semantics.Causation.Morphological.inanimate_no_induced :

CauseeAffecteeType.inanimate.hasInducedAgentivity = false

theorem Semantics.Causation.Morphological.physImpact_no_induced :

CauseeAffecteeType.physImpactHuman.hasInducedAgentivity = false

inductive Semantics.Causation.Morphological.IntransitivizationType :

How an alternating verb forms its intransitive variant.

@cite{krejci-2012}'s central insight: intransitive variants of causative/inchoative alternation verbs are NOT structurally uniform. Two distinct operations produce surface intransitives:

anticausative: on the deletion analysis (@cite{krejci-2012}), the external cause is removed entirely; the result is monoeventive: [BECOME [x STATE]], with no causer position. On the competing reflexivization analysis (@cite{koontz-garboden-2009}), CAUSE is retained and the EFFECTOR is identified with the THEME — the result is bieventive. See Phenomena/Causation/Studies/KoontzGarboden2009.lean.
reflexive: the causer and causee are coidentified — a single participant fills both roles. The result is bieventive: [x ACT] CAUSE [BECOME [x STATE]] with causer = causee. Morphologically marked: German sich, Marathi -un.
unmarked: no morphological distinction (English break). Event structure must be diagnosed per-verb.

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instDecidableEqIntransitivizationType :

DecidableEq IntransitivizationType

Equations

Semantics.Causation.Morphological.instDecidableEqIntransitivizationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprIntransitivizationType :

Repr IntransitivizationType

Equations

Semantics.Causation.Morphological.instReprIntransitivizationType = { reprPrec := Semantics.Causation.Morphological.instReprIntransitivizationType.repr }

def Semantics.Causation.Morphological.instReprIntransitivizationType.repr :

IntransitivizationType → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Causation.Morphological.IntransitivizationType.isBieventive :

IntransitivizationType → Bool

Reflexive intransitives retain the causer position (coidentified with the causee), preserving bieventive structure. Anticausatives remove the causer entirely, yielding monoeventive structure.

Equations

Semantics.Causation.Morphological.IntransitivizationType.reflexive.isBieventive = true
x✝.isBieventive = false

Instances For

def Semantics.Causation.Morphological.IntransitivizationType.hasCoidentification :

IntransitivizationType → Bool

Does the intransitive variant involve coidentification of causer and causee (a single participant in both roles)?

Equations

Semantics.Causation.Morphological.IntransitivizationType.reflexive.hasCoidentification = true
x✝.hasCoidentification = false

Instances For

def Semantics.Causation.Morphological.IntransitivizationType.licensesBySelf :

IntransitivizationType → Bool

"By itself" (von selbst, apne-aap, aapo-aap) is licensed when a causer position exists, even if coidentified with the causee. Anticausatives lack a causer position entirely.

English unmarked intransitives also license "by itself" ("The door opened by itself"), because the unmarked form can be either reflexive or anticausative — only true anticausatives block the modifier.

Equations

Semantics.Causation.Morphological.IntransitivizationType.anticausative.licensesBySelf = false
x✝.licensesBySelf = true

Instances For

theorem Semantics.Causation.Morphological.coidentification_implies_bieventive (it : IntransitivizationType) :

it.hasCoidentification = true → it.isBieventive = true

Coidentification implies bieventivity (the causer position preserved by coidentification is what makes the structure bieventive).

theorem Semantics.Causation.Morphological.bieventive_implies_bySelf (it : IntransitivizationType) :

it.isBieventive = true → it.licensesBySelf = true

Bieventivity implies "by itself" licensing (both track the presence of a causer position).

theorem Semantics.Causation.Morphological.anticausative_monoeventive :

IntransitivizationType.anticausative.isBieventive = false ∧ IntransitivizationType.anticausative.hasCoidentification = false ∧ IntransitivizationType.anticausative.licensesBySelf = false

Anticausatives are monoeventive on @cite{krejci-2012}'s analysis: no coidentification, no bieventivity, no "by itself" licensing. @cite{koontz-garboden-2009} disputes this — see Phenomena/Causation/Studies/KoontzGarboden2009.lean.

theorem Semantics.Causation.Morphological.reflexive_bieventive :

IntransitivizationType.reflexive.isBieventive = true ∧ IntransitivizationType.reflexive.hasCoidentification = true ∧ IntransitivizationType.reflexive.licensesBySelf = true

Reflexive intransitives are bieventive with coidentification.

@cite{krejci-2012} proposes a cross-linguistic hierarchy of causativizability — the extent to which a morphological causative morpheme can apply to different verb classes:

    unaccusatives > middles/ingestives > unergatives > simple transitives

The hierarchy is implicational: if a morpheme causativizes a
higher verb class, it also causativizes all lower classes. This
-- UNVERIFIED: table number
is validated across 12 languages in @cite{krejci-2012}.

structure Semantics.Causation.Morphological.CausativizabilityData :

Cross-linguistic data on causativizability: which verb classes a given morphological causative morpheme can apply to.

language : String
morpheme : String
unaccusative : Bool
middlesIngestive : Bool
unergative : Bool
simpleTransitive : Bool

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instReprCausativizabilityData :

Repr CausativizabilityData

Equations

Semantics.Causation.Morphological.instReprCausativizabilityData = { reprPrec := Semantics.Causation.Morphological.instReprCausativizabilityData.repr }

def Semantics.Causation.Morphological.instReprCausativizabilityData.repr :

CausativizabilityData → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Causation.Morphological.instBEqCausativizabilityData :

BEq CausativizabilityData

Equations

Semantics.Causation.Morphological.instBEqCausativizabilityData = { beq := Semantics.Causation.Morphological.instBEqCausativizabilityData.beq }

def Semantics.Causation.Morphological.instBEqCausativizabilityData.beq :

CausativizabilityData → CausativizabilityData → Bool

Equations

One or more equations did not get rendered due to their size.
Semantics.Causation.Morphological.instBEqCausativizabilityData.beq x✝¹ x✝ = false

Instances For

def Semantics.Causation.Morphological.CausativizabilityData.respectsHierarchy (d : CausativizabilityData) :

Bool

The hierarchy is implicational: each level implies all lower levels. simpleTransitive → unergative → middlesIngestive → unaccusative.

Equations

d.respectsHierarchy = ((!d.simpleTransitive || d.unergative) && (!d.unergative || d.middlesIngestive) && (!d.middlesIngestive || d.unaccusative))

Instances For

def Semantics.Causation.Morphological.krejciLanguages :

List CausativizabilityData

Cross-linguistic causativizability data from @cite{krejci-2012}. Languages are ordered from narrowest to broadest causative scope.

Equations

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

Instances For

theorem Semantics.Causation.Morphological.krejci_hierarchy_holds :

(krejciLanguages.all fun (x : CausativizabilityData) => x.respectsHierarchy) = true

All 12 languages respect the implicational hierarchy.