Beavers and Zubair (2013): Anticausatives in Sinhala

Beavers and Zubair analyze the anticausatives of Colloquial Sinhala. A causative root has two involitive detransitives, one with a nominative subject and no entailed external causer, and one with an accusative subject and an entailed external causer. Causer suppression derives both: it removes the causer from the verb's arguments, keeps the causation, and leaves the causer to be identified with the patient, as in Chierchia's and Koontz-Garboden's reflexivization, or bound existentially, as in Levin and Rappaport Hovav's analysis. A verb selects the sort of its causer, and suppression applies only when that sort includes the individuals, so minimarannə 'murder' and kapannə 'cut', which select events, have no inchoative.

Main definitions

• CauserSort: the typology of causer sorts, ordered by inclusion of basic sorts.
• causerSuppress: causer suppression.
• Reading.resolve: the two resolutions of the suppressed causer.
• caseOfReading: the accusative marks existential resolution.
• Anticausativizes: the condition of causer suppression on a root.

Main results

• CauserSort.not_event_le_individual: anticausatives are never volitive.
• reflexive_resolve_eq_reflexivize: reflexive resolution is Koontz-Garboden's reflexivization.
• causative_entails_existential: the inchoative is true whenever the causative is.
• ibeem_incompatible_with_external: ibeemə 'by itself' excludes the accusative variant.
• anticausativizes_iff_alternates: the roots that meet the condition are those with an inchoative.
• exists_hasInvolitive_not_anticausativizes: the involitive does not mark anticausatives.

Implementation notes

Sorts are checked rather than denoted. causerSuppress takes a proof that the root's causer sort includes the individuals in place of the conjunct x ∈ U_I of (77), and the volitive's sort condition is CauserSort.event ≤ s. kada- 'break' selects the whole domain as in (76), which revises the eventualities of (65a).

References

• J. Beavers and C. Zubair, Anticausatives in Sinhala: Involitivity and causer suppression (2013)
• J. Beavers and C. Zubair, The Interaction of Transitivity Features in the Sinhala Involitive (2010)
• A. Koontz-Garboden, Anticausativization (2009)
• G. Chierchia, A Semantics for Unaccusatives and its Syntactic Consequences (2004)
• B. Levin and M. Rappaport Hovav, Unaccusativity: At the Syntax-Lexical Semantics Interface (1995)

Sorts

The domain is sorted into individuals and eventualities, and the eventualities into events and states (§4.3). A verb's causer ranges over one of the sorts of the typology (81).

inductive BeaversZubair2013.BasicSort : Type

The basic sorts of the domain are the individuals and the eventualities of each dynamicity, the events being the dynamic eventualities.

• individual : BasicSort
• eventuality (k : Aspect.Dynamicity) : BasicSort

def BeaversZubair2013.instDecidableEqBasicSort.decEq (x✝ x✝¹ : BasicSort) : Decidable (x✝ = x✝¹)

Equations

• BeaversZubair2013.instDecidableEqBasicSort.decEq BeaversZubair2013.BasicSort.individual BeaversZubair2013.BasicSort.individual = isTrue ⋯
• BeaversZubair2013.instDecidableEqBasicSort.decEq BeaversZubair2013.BasicSort.individual (BeaversZubair2013.BasicSort.eventuality k) = isFalse ⋯
• BeaversZubair2013.instDecidableEqBasicSort.decEq (BeaversZubair2013.BasicSort.eventuality k) BeaversZubair2013.BasicSort.individual = isFalse ⋯
• BeaversZubair2013.instDecidableEqBasicSort.decEq (BeaversZubair2013.BasicSort.eventuality a) (BeaversZubair2013.BasicSort.eventuality b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversZubair2013.instDecidableEqBasicSort : DecidableEq BasicSort

Equations

• BeaversZubair2013.instDecidableEqBasicSort = BeaversZubair2013.instDecidableEqBasicSort.decEq

inductive BeaversZubair2013.CauserSort : Type

A causer sort is a node of the typology (81).

• event : CauserSort

  U_E comprises the events, the causers that murder verbs select.

• state : CauserSort

  U_S comprises the states, which (81) assigns to bloom verbs and negligence readings.

• eventuality : CauserSort

  U_V comprises the eventualities, the causers that destroy verbs select (80).

• individual : CauserSort

  U_I comprises the individuals, the subjects of anticausatives.

• any : CauserSort

  U is the whole domain, the causers that transitive break verbs select (76).

@[instance_reducible]

instance BeaversZubair2013.instDecidableEqCauserSort : DecidableEq CauserSort

Equations

• BeaversZubair2013.instDecidableEqCauserSort x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversZubair2013.instFintypeCauserSort : Fintype CauserSort

Equations

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

def BeaversZubair2013.CauserSort.basicSorts : CauserSort → Finset BasicSort

s.basicSorts is the set of basic sorts that the causer sort s comprises.

Equations

• One or more equations did not get rendered due to their size.
• BeaversZubair2013.CauserSort.event.basicSorts = {BeaversZubair2013.BasicSort.eventuality Aspect.Dynamicity.dynamic}
• BeaversZubair2013.CauserSort.state.basicSorts = {BeaversZubair2013.BasicSort.eventuality Aspect.Dynamicity.stative}
• BeaversZubair2013.CauserSort.eventuality.basicSorts = {BeaversZubair2013.BasicSort.eventuality Aspect.Dynamicity.dynamic, BeaversZubair2013.BasicSort.eventuality Aspect.Dynamicity.stative}
• BeaversZubair2013.CauserSort.individual.basicSorts = {BeaversZubair2013.BasicSort.individual}

theorem BeaversZubair2013.CauserSort.basicSorts_injective : Function.Injective basicSorts

@[instance_reducible]

instance BeaversZubair2013.CauserSort.instPartialOrder : PartialOrder CauserSort

One causer sort lies below another when its basic sorts are among the other's.

Equations

• BeaversZubair2013.CauserSort.instPartialOrder = PartialOrder.lift BeaversZubair2013.CauserSort.basicSorts BeaversZubair2013.CauserSort.basicSorts_injective

@[instance_reducible]

instance BeaversZubair2013.CauserSort.instDecidableLE : DecidableLE CauserSort

Equations

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

@[instance_reducible]

instance BeaversZubair2013.CauserSort.instDecidableLT : DecidableLT CauserSort

Equations

• BeaversZubair2013.CauserSort.instDecidableLT = decidableLTOfDecidableLE

theorem BeaversZubair2013.CauserSort.covBy_tree : event ⋖ eventuality ∧ state ⋖ eventuality ∧ eventuality ⋖ any ∧ individual ⋖ any

The typology (81) is a tree whose leaves are the events, the states and the individuals.

theorem BeaversZubair2013.CauserSort.individual_le_iff {s : CauserSort} : individual ≤ s ↔ s = individual ∨ s = any

Causer suppression (77) applies to the roots whose causer sort includes the individuals, those that select the individuals or the whole domain.

theorem BeaversZubair2013.CauserSort.event_le_iff {s : CauserSort} : event ≤ s ↔ s = event ∨ s = eventuality ∨ s = any

The volitive (71) applies to a predicate whose subject sort includes the events. These are the sorts of murder, destroy and break verbs, the three kinds of causative of §7.3.

theorem BeaversZubair2013.CauserSort.not_event_le_individual : ¬event ≤ individual

An individual subject cannot be resolved to an event, so an anticausative, whose subject is an individual, has no volitive (§7.3).

Causer suppression

def BeaversZubair2013.causerSuppress {E α : Type} (s : CauserSort) (_h : CauserSort.individual ≤ s) (z : E) (vp : E → α) : α

Causer suppression (77) saturates the causer argument of vp with the open variable z. It is defined only for a root whose causer sort includes the individuals.

Equations

• BeaversZubair2013.causerSuppress s _h z vp = vp z

The two resolutions of the suppressed causer

inductive BeaversZubair2013.Reading : Type

An anticausativized verb has two readings (78), on which the suppressed causer is coindexed with the patient or existentially closed.

• reflexive : Reading
• existential : Reading

@[instance_reducible]

instance BeaversZubair2013.instDecidableEqReading : DecidableEq Reading

Equations

• BeaversZubair2013.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversZubair2013.instReprReading : Repr Reading

Equations

• BeaversZubair2013.instReprReading = { reprPrec := BeaversZubair2013.instReprReading.repr }

def BeaversZubair2013.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

def BeaversZubair2013.Reading.resolve {E : Type} {s : CauserSort} (r : Reading) (h : CauserSort.individual ≤ s) (vp : E → E → Prop) : E → Prop

A reading's denotation binds the open causer that causerSuppress leaves to the patient under reflexive resolution and closes it under existential resolution. The verb takes its causer first, so vp x y has causer x and patient y.

Equations

• BeaversZubair2013.Reading.reflexive.resolve h vp = fun (y : E) => BeaversZubair2013.causerSuppress s h y vp y
• BeaversZubair2013.Reading.existential.resolve h vp = fun (y : E) => ∃ (x : E), BeaversZubair2013.causerSuppress s h x vp y

theorem BeaversZubair2013.reflexive_resolve_eq_reflexivize {E : Type} {s : CauserSort} (h : CauserSort.individual ≤ s) (vp : E → E → Prop) : Reading.reflexive.resolve h vp = KoontzGarboden2009.reflexivize vp

Reflexive resolution is Koontz-Garboden's reflexivization, the null reflexive (37).

def BeaversZubair2013.caseOfReading : Reading → Case

An anticausative's subject is accusative under existential resolution and nominative, the elsewhere case, under reflexive resolution (§7.3). Accusative is optional and limited to animates (fn. 27), so the converse is not stated.

Equations

• BeaversZubair2013.caseOfReading BeaversZubair2013.Reading.reflexive = Case.nom
• BeaversZubair2013.caseOfReading BeaversZubair2013.Reading.existential = Case.acc

theorem BeaversZubair2013.causative_entails_existential {E : Type} {s : CauserSort} (h : CauserSort.individual ≤ s) (vp : E → E → Prop) (x y : E) (hxy : vp x y) : Reading.existential.resolve h vp y

Any causative claim entails the existentially resolved inchoative. Inchoatives are true in agentive contexts ((51), §5.3), so the ban on volitive inchoatives is formal rather than truth-conditional.

theorem BeaversZubair2013.reflexive_entails_existential {E : Type} {s : CauserSort} (h : CauserSort.individual ≤ s) (vp : E → E → Prop) (y : E) (hy : Reading.reflexive.resolve h vp y) : Reading.existential.resolve h vp y

The reflexive resolution entails the existential one, with the patient itself as witness.

theorem BeaversZubair2013.ibeem_incompatible_with_external {E : Type} (vp : E → E → Prop) (y : E) : ¬((∀ (x : E), vp x y → x = y) ∧ ∃ (x : E), x ≠ y ∧ vp x y)

The ibeemə 'by itself' diagnostic (58) denies external causation, which contradicts the accusative's distinct external causer, so accusative-subject anticausatives reject ibeemə.

The roots and their causer sorts

inductive BeaversZubair2013.Root : Type

A Root is one of the Sinhala roots that the paper analyzes.

• kada : Root
• gila : Root
• mara : Root
• minimara : Root
• kapa : Root
• vinaashKara : Root

@[instance_reducible]

instance BeaversZubair2013.instDecidableEqRoot : DecidableEq Root

Equations

• BeaversZubair2013.instDecidableEqRoot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversZubair2013.instFintypeRoot : Fintype Root

Equations

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

def BeaversZubair2013.instReprRoot.repr : Root → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversZubair2013.instReprRoot : Repr Root

Equations

• BeaversZubair2013.instReprRoot = { reprPrec := BeaversZubair2013.instReprRoot.repr }

def BeaversZubair2013.Root.verb : Root → Sinhala.Verb

r.verb is the fragment verb of the root r.

Equations

• BeaversZubair2013.Root.kada.verb = Sinhala.kadann
• BeaversZubair2013.Root.gila.verb = Sinhala.gilann
• BeaversZubair2013.Root.mara.verb = Sinhala.marann
• BeaversZubair2013.Root.minimara.verb = Sinhala.minimarann
• BeaversZubair2013.Root.kapa.verb = Sinhala.kapann
• BeaversZubair2013.Root.vinaashKara.verb = Sinhala.vinaashKarann

def BeaversZubair2013.Root.causerSort : Root → CauserSort

r.causerSort is the causer sort that r selects. The agent-subject roots minimara- 'murder' ((65b)) and kapa- 'cut' select events, and the effector-subject roots select the whole domain, as kada- 'break' does (76) and as 'destroy' does in Sinhala, where it alternates (p. 40).

Equations

• BeaversZubair2013.Root.minimara.causerSort = BeaversZubair2013.CauserSort.event
• BeaversZubair2013.Root.kapa.causerSort = BeaversZubair2013.CauserSort.event
• BeaversZubair2013.Root.kada.causerSort = BeaversZubair2013.CauserSort.any
• BeaversZubair2013.Root.gila.causerSort = BeaversZubair2013.CauserSort.any
• BeaversZubair2013.Root.mara.causerSort = BeaversZubair2013.CauserSort.any
• BeaversZubair2013.Root.vinaashKara.causerSort = BeaversZubair2013.CauserSort.any

def BeaversZubair2013.Anticausativizes (r : Root) : Prop

A root anticausativizes when its causer sort includes the individuals, the condition of causer suppression (77).

Equations

• BeaversZubair2013.Anticausativizes r = (BeaversZubair2013.CauserSort.individual ≤ r.causerSort)

@[instance_reducible]

instance BeaversZubair2013.instDecidablePredRootAnticausativizes : DecidablePred Anticausativizes

Equations

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

theorem BeaversZubair2013.anticausativizes_iff_alternates (r : Root) : Anticausativizes r ↔ r.verb.Alternates Voice.anticausative

The roots that meet the condition of causer suppression are exactly those whose verbs have an inchoative.

theorem BeaversZubair2013.hasInvolitive_of_anticausativizes {r : Root} (h : Anticausativizes r) : r.verb.HasInvolitive

A root that anticausativizes has an involitive stem, where its inchoative surfaces since the volitive is barred (§7.3).

theorem BeaversZubair2013.exists_hasInvolitive_not_anticausativizes : ∃ (r : Root), r.verb.HasInvolitive ∧ ¬Anticausativizes r

The involitive does not mark anticausatives, since kapa- 'cut' has an involitive stem ((7c)) and no inchoative ((26)).