Morphological causation: compactness and directness

Causative constructions vary along two scales: morphological complexity, from compact (lexical) to analytic (periphrastic), and directness of mediation, from a causer that brings about the result itself to one that acts through a causee. [Com89]'s generalization is that within a language the more compact construction expresses the more direct causation (CausativeConstruction.ComrieMonotone). The causee of a causativized verb takes the highest grammatical relation its base verb leaves free (causeeDemotion), so the causee sinks as the base valency rises (causeeDemotion_antitoneOn).

References

• [Com89]

Mediation

inductive Causation.Morphological.Mediation : Type

Directness of causal mediation between causer and result.

[Com89]: direct causation involves no intermediary, the causer bringing 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

  The causer brings about the result itself.

• indirect : Mediation

  The causer acts through an intermediary causee.

@[instance_reducible]

instance Causation.Morphological.instDecidableEqMediation : DecidableEq Mediation

Equations

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

def Causation.Morphological.instReprMediation.repr : Mediation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Causation.Morphological.instReprMediation : Repr Mediation

Equations

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

@[instance_reducible]

instance Causation.Morphological.instFintypeMediation : Fintype Mediation

Equations

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

def Causation.Morphological.Mediation.rank : Mediation → ℕ

Numeric rank: direct (0) < indirect (1).

Equations

• Causation.Morphological.Mediation.direct.rank = 0
• Causation.Morphological.Mediation.indirect.rank = 1

@[instance_reducible]

instance Causation.Morphological.instLinearOrderMediation : LinearOrder Mediation

Direct < indirect: the directness scale.

Equations

• Causation.Morphological.instLinearOrderMediation = LinearOrder.lift' Causation.Morphological.Mediation.rank ⋯

Causative complexity

inductive Causation.Morphological.CausativeComplexity : Type

Morphological complexity of a causative construction, [Com89]'s compact-to-analytic continuum:

• lexical: suppletive or idiosyncratic (kill die, fell fall)
• morphological: a productive affix (Japanese -(s)ase)
• periphrastic: an analytic multi-word construction (English make X do Y)

• lexical : CausativeComplexity
• morphological : CausativeComplexity
• periphrastic : CausativeComplexity

@[instance_reducible]

instance Causation.Morphological.instDecidableEqCausativeComplexity : DecidableEq CausativeComplexity

Equations

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

def Causation.Morphological.instReprCausativeComplexity.repr : CausativeComplexity → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Causation.Morphological.instReprCausativeComplexity : Repr CausativeComplexity

Equations

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

def Causation.Morphological.CausativeComplexity.toNat : CausativeComplexity → ℕ

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

Equations

• Causation.Morphological.CausativeComplexity.lexical.toNat = 0
• Causation.Morphological.CausativeComplexity.morphological.toNat = 1
• Causation.Morphological.CausativeComplexity.periphrastic.toNat = 2

@[instance_reducible]

instance Causation.Morphological.instLinearOrderCausativeComplexity : LinearOrder CausativeComplexity

Equations

• Causation.Morphological.instLinearOrderCausativeComplexity = LinearOrder.lift' Causation.Morphological.CausativeComplexity.toNat ⋯

Causative constructions and Comrie's generalization

structure Causation.Morphological.CausativeConstruction : Type

A causative construction, located on the two scales.

• complexity : CausativeComplexity

  Morphological complexity (compact → analytic).

• mediation : Mediation

  Direct vs. indirect mediation.

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

Equations

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

@[instance_reducible]

instance Causation.Morphological.instDecidableEqCausativeConstruction : DecidableEq CausativeConstruction

Equations

• Causation.Morphological.instDecidableEqCausativeConstruction = Causation.Morphological.instDecidableEqCausativeConstruction.decEq

def Causation.Morphological.instReprCausativeConstruction.repr : CausativeConstruction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Causation.Morphological.instReprCausativeConstruction : Repr CausativeConstruction

Equations

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

def Causation.Morphological.CausativeConstruction.ComrieMonotone (c₁ c₂ : CausativeConstruction) : Prop

Comrie's monotonicity ([Com89]): if construction c₁ is morphologically more compact than c₂, then c₁ encodes at least as direct causation as c₂.

Equations

• c₁.ComrieMonotone c₂ = (c₁.complexity < c₂.complexity → c₁.mediation ≤ c₂.mediation)

@[instance_reducible]

instance Causation.Morphological.instDecidableComrieMonotone (c₁ c₂ : CausativeConstruction) : Decidable (c₁.ComrieMonotone c₂)

Equations

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

The causee-marking hierarchy

inductive Causation.Morphological.CauseeSlot : Type

Grammatical relations available to the causee, ordered from highest to lowest.

[Com89]: when a verb is causativized, its original subject is demoted to the highest relation on the hierarchy that the base verb's arguments leave free, so an intransitive base yields a direct-object causee, a transitive one an indirect-object causee, and a ditransitive one an oblique causee.

• directObject : CauseeSlot
• indirectObject : CauseeSlot
• oblique : CauseeSlot

@[instance_reducible]

instance Causation.Morphological.instDecidableEqCauseeSlot : DecidableEq CauseeSlot

Equations

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

def Causation.Morphological.instReprCauseeSlot.repr : CauseeSlot → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Causation.Morphological.instReprCauseeSlot : Repr CauseeSlot

Equations

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

def Causation.Morphological.CauseeSlot.rank : CauseeSlot → ℕ

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

Equations

• Causation.Morphological.CauseeSlot.directObject.rank = 2
• Causation.Morphological.CauseeSlot.indirectObject.rank = 1
• Causation.Morphological.CauseeSlot.oblique.rank = 0

@[instance_reducible]

instance Causation.Morphological.instLinearOrderCauseeSlot : LinearOrder CauseeSlot

Oblique < indirect object < direct object: the grammatical-relations hierarchy.

Equations

• Causation.Morphological.instLinearOrderCauseeSlot = LinearOrder.lift' Causation.Morphological.CauseeSlot.rank ⋯

def Causation.Morphological.causeeDemotion : ℕ → CauseeSlot

The causee's slot given the base verb's valency: the highest slot the base verb's own arguments leave free.

Equations

• Causation.Morphological.causeeDemotion 1 = Causation.Morphological.CauseeSlot.directObject
• Causation.Morphological.causeeDemotion 2 = Causation.Morphological.CauseeSlot.indirectObject
• Causation.Morphological.causeeDemotion x✝ = Causation.Morphological.CauseeSlot.oblique

theorem Causation.Morphological.causeeDemotion_antitoneOn : AntitoneOn causeeDemotion (Set.Ici 1)

The higher the base valency, the lower the causee lands.