Bohnemeyer 2004: split intransitivity, linking, and lexical representation

Bohnemeyer accounts for split intransitivity in Yukatek Maya. Kraemer and Wunderlich derive the language's argument linking from lexical aspect alone; Bohnemeyer argues that what the linking rules see is event structure, specifically whether the intransitive base entails internal causation. Transitivizing an internally-caused base gives applicative linking, the added applied object realized as U with the original S left as A; transitivizing an externally-caused base gives causative linking, the added instigator realized as A with the original S demoted to U (rules (26)–(27)). Which overt suffix appears, -t or -s, is lexically idiosyncratic and can dissociate from the linking, as balak' 'roll' and péek 'move' show in opposite directions.

The aspect-conditioned split itself follows from the same causal chain: the participant of a causing subevent outranks that of the caused subevent (31), and an imperfective viewpoint aligns with the initial subevent while a perfective one aligns with the final subevent or the chain as a whole (32) — accusative and ergative defaults respectively.

The verbs and their stem classes are the Yukatek fragment's; the event type the paper reads into each class, the causation type of each base and the transitivizing suffixes are the paper's and are recorded here.

Main definitions

• Verb, CausationType, stemTemplate: the fragment's verbs with the paper's causation type, and the event-structure template of each stem class (§5).
• Subevent, Subevent.Causes, linkingDefault, sMarkerFromViewpoint: the thematic hierarchy of (31) as causal precedence along the CAUSE edge, the linking-by-viewpoint rule of (32), and the linking of (33).
• applicativeLinking, causativeLinking, verbLinking, addedTermRole: the two transitivizations as Voices, and the role their added participant takes.
• TransitivizerSuffix, transitivizerSuffix: the overt suffix, kept apart from the linking.
• DetransitivizationType, DetransitivizationType.retained: the antipassive, anticausative and passive of (28)–(30), and the subevent each denotes, a projection of the base's template (Subevent.of).

Main results

• linking_derives_completive, linking_derives_incompletive: the split follows from (31)–(33).
• causation_determines_linking against template_underdetermines_linking, stemClass_underdetermines_linking, suffix_underdetermines_linking: what fixes the linking and what does not.
• linking_patterns_swap_roles, linking_markers: the two alternations are mirror images, read off their records rather than stipulated.
• degree_achievements_causativize, haanEat_applicative_despite_inactive: the counterexamples to aspect- and class-based linking.
• predictLinking_roles, pivotSourceRole_toVoice: the roles of transitivization (26)–(27) and of detransitivization (28)–(30) follow from the subevent a participant occupies, by the hierarchy (31).
• passive_anticausative_distinct_by_A_fate: the fate of the initial A separates the two.
• salience_agrees_on_shared_roots, haanEat_defies_transitiviser_diagnostic: where this classification meets Lucy's.

References

• [Boh04]
• [KW99]
• [LRH95]
• [Luc94]

The verbs and their event structure

The stem classes are the fragment's. The paper reads the active stems as processes and the inactive, inchoative and positional stems as state changes, degree achievements included (§5), so the template of an intransitive stem class has BECOME exactly when the class is one of state change. Each documented intransitive base is classified by whether it entails internal causation (§6).

def Bohnemeyer2004.stemTemplate : Yukatek.VerbStemClass → ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event

The event-structure template of a stem class, the activity for actives, the achievement for the three state-change classes and the accomplishment for transitives.

Equations

• Bohnemeyer2004.stemTemplate Yukatek.VerbStemClass.active = ArgumentStructure.EventStructure.Template.act
• Bohnemeyer2004.stemTemplate Yukatek.VerbStemClass.inactive = ArgumentStructure.EventStructure.Template.achievement
• Bohnemeyer2004.stemTemplate Yukatek.VerbStemClass.inchoative = ArgumentStructure.EventStructure.Template.achievement
• Bohnemeyer2004.stemTemplate Yukatek.VerbStemClass.positional = ArgumentStructure.EventStructure.Template.achievement
• Bohnemeyer2004.stemTemplate Yukatek.VerbStemClass.transitiveActive = ArgumentStructure.EventStructure.Template.accomplishment

inductive Bohnemeyer2004.CausationType : Type

Whether an event is internally caused in the sense of [LRH95], brought about by its instigator, a participant of the first event of a causal chain (§2).

• internal : CausationType
• external : CausationType

@[instance_reducible]

instance Bohnemeyer2004.instDecidableEqCausationType : DecidableEq CausationType

Equations

• Bohnemeyer2004.instDecidableEqCausationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bohnemeyer2004.instReprCausationType.repr : CausationType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instReprCausationType : Repr CausationType

Equations

• Bohnemeyer2004.instReprCausationType = { reprPrec := Bohnemeyer2004.instReprCausationType.repr }

structure Bohnemeyer2004.Verbextends Yukatek.Verb : Type

A verb of the paper's examples with the causation type of its intransitive base.

• form : String
• gloss : String
• stemClass : VerbStemClass
• causationType : CausationType

  Whether the base entails internal causation.

def Bohnemeyer2004.instDecidableEqVerb.decEq (x✝ x✝¹ : Verb) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instDecidableEqVerb : DecidableEq Verb

Equations

• Bohnemeyer2004.instDecidableEqVerb = Bohnemeyer2004.instDecidableEqVerb.decEq

def Bohnemeyer2004.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instReprVerb : Repr Verb

Equations

• Bohnemeyer2004.instReprVerb = { reprPrec := Bohnemeyer2004.instReprVerb.repr }

def Bohnemeyer2004.meyah : Verb

meyah 'work', internally caused.

Equations

• Bohnemeyer2004.meyah = { toVerb := Yukatek.meyah, causationType := Bohnemeyer2004.CausationType.internal }

def Bohnemeyer2004.bàaxal : Verb

bàaxal 'play', internally caused.

Equations

• Bohnemeyer2004.bàaxal = { toVerb := Yukatek.bàaxal, causationType := Bohnemeyer2004.CausationType.internal }

def Bohnemeyer2004.hàan : Verb

hàan 'eat', internally caused though inactive by stem class ((9)).

Equations

• Bohnemeyer2004.hàan = { toVerb := Yukatek.hàan, causationType := Bohnemeyer2004.CausationType.internal }

def Bohnemeyer2004.hats' : Verb

hats' 'hit', internally caused.

Equations

• Bohnemeyer2004.hats' = { toVerb := Yukatek.hats', causationType := Bohnemeyer2004.CausationType.internal }

def Bohnemeyer2004.balak' : Verb

balak' 'roll', externally caused.

Equations

• Bohnemeyer2004.balak' = { toVerb := Yukatek.balak', causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.péek : Verb

péek 'move', externally caused.

Equations

• Bohnemeyer2004.péek = { toVerb := Yukatek.péek, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.tsíirin : Verb

tsíirin 'buzz', externally caused.

Equations

• Bohnemeyer2004.tsíirin = { toVerb := Yukatek.tsíirin, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.chíik : Verb

chíik 'shake', externally caused.

Equations

• Bohnemeyer2004.chíik = { toVerb := Yukatek.chíik, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.háarax : Verb

háarax 'slide', externally caused.

Equations

• Bohnemeyer2004.háarax = { toVerb := Yukatek.háarax, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.húuy : Verb

húuy 'stir', externally caused.

Equations

• Bohnemeyer2004.húuy = { toVerb := Yukatek.húuy, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.mosòon : Verb

mosòon 'whirl', externally caused.

Equations

• Bohnemeyer2004.mosòon = { toVerb := Yukatek.mosòon, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.pirix : Verb

pirix 'flick', externally caused.

Equations

• Bohnemeyer2004.pirix = { toVerb := Yukatek.pirix, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.walak' : Verb

walak' 'turn', externally caused.

Equations

• Bohnemeyer2004.walak' = { toVerb := Yukatek.walak', causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.nik'ich : Verb

nik'ich 'squeak', externally caused.

Equations

• Bohnemeyer2004.nik'ich = { toVerb := Yukatek.nik'ich, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.kim : Verb

kim 'die', externally caused.

Equations

• Bohnemeyer2004.kim = { toVerb := Yukatek.kim, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.lúub : Verb

lúub 'fall', externally caused.

Equations

• Bohnemeyer2004.lúub = { toVerb := Yukatek.lúub, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.ka'n : Verb

ka'n 'get tired', externally caused.

Equations

• Bohnemeyer2004.ka'n = { toVerb := Yukatek.ka'n, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.na'k : Verb

na'k 'ascend', externally caused.

Equations

• Bohnemeyer2004.na'k = { toVerb := Yukatek.na'k, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.la'b : Verb

la'b 'deteriorate', externally caused.

Equations

• Bohnemeyer2004.la'b = { toVerb := Yukatek.la'b, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.t'íil : Verb

t'íil 'last', externally caused.

Equations

• Bohnemeyer2004.t'íil = { toVerb := Yukatek.t'íil, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.ts'u'k : Verb

ts'u'k 'rot', externally caused.

Equations

• Bohnemeyer2004.ts'u'k = { toVerb := Yukatek.ts'u'k, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.bòoxtal : Verb

bòox-tal 'blacken', externally caused.

Equations

• Bohnemeyer2004.bòoxtal = { toVerb := Yukatek.bòoxtal, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.chichantal : Verb

chichan-tal 'shrink', externally caused.

Equations

• Bohnemeyer2004.chichantal = { toVerb := Yukatek.chichantal, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.kultal : Verb

kul-tal 'sit down', externally caused.

Equations

• Bohnemeyer2004.kultal = { toVerb := Yukatek.kultal, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.wa'ltal : Verb

wa'l-tal 'stand up', externally caused.

Equations

• Bohnemeyer2004.wa'ltal = { toVerb := Yukatek.wa'ltal, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.chiltal : Verb

chil-tal 'lie down', externally caused.

Equations

• Bohnemeyer2004.chiltal = { toVerb := Yukatek.chiltal, causationType := Bohnemeyer2004.CausationType.external }

def Bohnemeyer2004.xoltal : Verb

xol-tal 'kneel', externally caused.

Equations

• Bohnemeyer2004.xoltal = { toVerb := Yukatek.xoltal, causationType := Bohnemeyer2004.CausationType.external }

Causal chain and thematic hierarchy

inductive Bohnemeyer2004.Subevent : Type

A subevent is one of the two in the causal chain a clause expresses, the causing subevent or the subevent it causes. Yukatek clauses have at most two core arguments, so two subevents suffice for the hierarchy (31).

• causing : Subevent
• caused : Subevent

@[instance_reducible]

instance Bohnemeyer2004.instDecidableEqSubevent : DecidableEq Subevent

Equations

• Bohnemeyer2004.instDecidableEqSubevent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bohnemeyer2004.instFintypeSubevent : Fintype Subevent

Equations

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

def Bohnemeyer2004.instReprSubevent.repr : Subevent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instReprSubevent : Repr Subevent

Equations

• Bohnemeyer2004.instReprSubevent = { reprPrec := Bohnemeyer2004.instReprSubevent.repr }

def Bohnemeyer2004.Subevent.Causes (a b : Subevent) : Prop

Causes a b holds when a is the causing and b the caused subevent, the causal edge of (31).

Equations

• a.Causes b = (a = Bohnemeyer2004.Subevent.causing ∧ b = Bohnemeyer2004.Subevent.caused)

@[instance_reducible]

instance Bohnemeyer2004.instDecidableRelSubeventCauses : DecidableRel Subevent.Causes

Equations

• Bohnemeyer2004.instDecidableRelSubeventCauses x✝¹ x✝ = { decide := decide (x✝¹ = Bohnemeyer2004.Subevent.causing) && decide (x✝ = Bohnemeyer2004.Subevent.caused), reflects_decide := ⋯ }

@[instance_reducible]

instance Bohnemeyer2004.instLinearOrderSubevent : LinearOrder Subevent

Subevents in order of causal precedence, the causing subevent first. The thematic hierarchy (31) ranks the participant of a causing subevent above the participant of the subevent it causes, so a participant of a outranks a participant of b exactly when a < b.

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instBoundedOrderSubevent : BoundedOrder Subevent

Equations

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

def Bohnemeyer2004.termRole : Subevent → Voice.TermRole

termRole e is the core term role of the participant of e (33a–b). The highest-ranking role is the A of a transitive clause and the lowest-ranking role its P.

Equations

• Bohnemeyer2004.termRole Bohnemeyer2004.Subevent.causing = Voice.TermRole.A
• Bohnemeyer2004.termRole Bohnemeyer2004.Subevent.caused = Voice.TermRole.P

def Bohnemeyer2004.Subevent.other : Subevent → Subevent

The other subevent of the chain.

Equations

• Bohnemeyer2004.Subevent.causing.other = Bohnemeyer2004.Subevent.caused
• Bohnemeyer2004.Subevent.caused.other = Bohnemeyer2004.Subevent.causing

def Bohnemeyer2004.Subevent.of : Subevent → ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event → Option (ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event)

e.of t is the subevent e of the causative template t, its causing or its caused subevent, and none when t is not causative.

Equations

• Bohnemeyer2004.Subevent.causing.of = ArgumentStructure.EventStructure.Template.causing
• Bohnemeyer2004.Subevent.caused.of = ArgumentStructure.EventStructure.Template.caused

def Bohnemeyer2004.markerOf : Voice.TermRole → Option Mayan.MarkerSet

markerOf r is the marker set the core term role r takes in Yukatek (33), set A for A and set B for P. The sole argument of an intransitive takes whichever the viewpoint selects, which is the split (sMarkerFromViewpoint).

Equations

• Bohnemeyer2004.markerOf Voice.TermRole.A = some Mayan.MarkerSet.setA
• Bohnemeyer2004.markerOf Voice.TermRole.P = some Mayan.MarkerSet.setB
• Bohnemeyer2004.markerOf Voice.TermRole.S = none
• Bohnemeyer2004.markerOf Voice.TermRole.X = none

theorem Bohnemeyer2004.markerOf_termRole_of_lt {a b : Subevent} (h : a < b) : markerOf (termRole a) = some Mayan.MarkerSet.setA ∧ markerOf (termRole b) = some Mayan.MarkerSet.setB

The marker assignment respects the hierarchy: the participant of the earlier subevent is realized as A and takes set A, the participant of the later one as P and takes set B.

Linking by viewpoint

def Bohnemeyer2004.linkingDefault {α : Type u_1} [LE α] [BoundedOrder α] : Aspect.Perfectivity → α

By rule (32), viewpoint aspect aligns with an end of the causal chain, and the role there sets the default for linking. An imperfective viewpoint aligns with the initial subevent, making the highest-ranking role the default, the accusative pattern. A perfective one aligns with the final subevent or the chain as a whole, making the lowest-ranking role the default, the ergative pattern.

Equations

• Bohnemeyer2004.linkingDefault Aspect.Perfectivity.imperfective = ⊥
• Bohnemeyer2004.linkingDefault Aspect.Perfectivity.perfective = ⊤

def Bohnemeyer2004.sMarkerFromViewpoint (v : Aspect.Perfectivity) : Option Mayan.MarkerSet

The marker of the sole argument S of an intransitive. S is unranked, so by (33c) it follows the default that the viewpoint selects by (32), and takes the marker of that role.

Equations

• Bohnemeyer2004.sMarkerFromViewpoint v = Bohnemeyer2004.markerOf (Bohnemeyer2004.termRole (Bohnemeyer2004.linkingDefault v))

Linking by viewpoint derives the split

The composed mechanism reproduces the Yukatek split recorded in the Fragment's sArgumentMarker: perfective status → ergative (set-B), imperfective → accusative (set-A).

theorem Bohnemeyer2004.linking_derives_completive : sMarkerFromViewpoint Aspect.Perfectivity.perfective = Yukatek.sArgumentMarker Yukatek.StatusCategory.completive

theorem Bohnemeyer2004.linking_derives_subjunctive : sMarkerFromViewpoint Aspect.Perfectivity.perfective = Yukatek.sArgumentMarker Yukatek.StatusCategory.subjunctive

theorem Bohnemeyer2004.linking_derives_incompletive : sMarkerFromViewpoint Aspect.Perfectivity.imperfective = Yukatek.sArgumentMarker Yukatek.StatusCategory.incompletive

Linking pattern under transitivization

def Bohnemeyer2004.applicativeLinking : Voice

By rule (26), transitivizing an internally-caused base nucleativizes an applied object as P while the base's S is maintained, surfacing as the A of the derived transitive clause. This is Creissels' P-applicativization over an intransitive base.

Equations

• Bohnemeyer2004.applicativeLinking = Voice.of ArgumentFrame.intransitive ArgumentFrame.np [some ArgumentFrame.Slot.external, some (ArgumentFrame.Slot.complement 0)]

def Bohnemeyer2004.causativeLinking : Voice

By rule (27), transitivizing an externally-caused base nucleativizes an instigator as A, the base's S surfacing as P. This is the causative unchanged.

Equations

• Bohnemeyer2004.causativeLinking = Voice.causative

def Bohnemeyer2004.predictLinking : CausationType → Voice

The causation type of the intransitive base selects the alternation (rules 26–27).

Equations

• Bohnemeyer2004.predictLinking Bohnemeyer2004.CausationType.internal = Bohnemeyer2004.applicativeLinking
• Bohnemeyer2004.predictLinking Bohnemeyer2004.CausationType.external = Bohnemeyer2004.causativeLinking

def Bohnemeyer2004.verbLinking (v : Verb) : Voice

The alternation a Yukatek verb undergoes under transitivization.

Equations

• Bohnemeyer2004.verbLinking v = Bohnemeyer2004.predictLinking v.causationType

def Bohnemeyer2004.addedRole (va : Voice) : Option Voice.TermRole

The role the added participant receives, read off the alternation.

Equations

• Bohnemeyer2004.addedRole va = va.newParticipant

def Bohnemeyer2004.originalRole (va : Voice) : Option Voice.TermRole

The base's S receives the role of the derived slot its participant occupies.

Equations

• Bohnemeyer2004.originalRole va = (va.image ArgumentFrame.Slot.external).bind fun (t : ArgumentFrame.Slot) => (va.derived.status t).role

def Bohnemeyer2004.CausationType.baseSubevent : CausationType → Subevent

Under transitivization the participant of an internally-caused base occupies the causing process (26), and that of an externally-caused base the caused event (27).

Equations

• Bohnemeyer2004.CausationType.internal.baseSubevent = Bohnemeyer2004.Subevent.causing
• Bohnemeyer2004.CausationType.external.baseSubevent = Bohnemeyer2004.Subevent.caused

theorem Bohnemeyer2004.predictLinking_roles (c : CausationType) : originalRole (predictLinking c) = some (termRole c.baseSubevent) ∧ addedRole (predictLinking c) = some (termRole c.baseSubevent.other)

Under transitivization (26)–(27) and the hierarchy (31), the base's participant takes the role of the subevent it occupies and the added participant that of the other, so the instigator of an internally-caused process outranks the added argument, and the participant of an externally-caused event is outranked by it.

theorem Bohnemeyer2004.linking_patterns_swap_roles : addedRole applicativeLinking = originalRole causativeLinking ∧ originalRole applicativeLinking = addedRole causativeLinking

Applicative and causative linking are mirror images, and not by stipulation: each alternation adds a participant in the role the other leaves to the base's S, so the marker one assigns to the added argument is the marker the other assigns to the original S.

theorem Bohnemeyer2004.linking_markers : (addedRole applicativeLinking).bind markerOf = some Mayan.MarkerSet.setB ∧ (originalRole applicativeLinking).bind markerOf = some Mayan.MarkerSet.setA ∧ (addedRole causativeLinking).bind markerOf = some Mayan.MarkerSet.setA ∧ (originalRole causativeLinking).bind markerOf = some Mayan.MarkerSet.setB

The marker each participant receives follows from its role by markerOf: the applicative adds a set-B argument and keeps the base's S as set A, the causative the reverse.

theorem Bohnemeyer2004.transitivizations_increase_valency : applicativeLinking.IsValencyIncreasing ∧ causativeLinking.IsValencyIncreasing

Both transitivizations are valency-increasing, which the detransitivizations of (28)–(30) are not — the two halves of the system are one mechanism read in two directions.

def Bohnemeyer2004.addedTermRole (v : Verb) : Option Voice.TermRole

The added participant of a verb takes P under applicative linking and A under causative linking.

Equations

• Bohnemeyer2004.addedTermRole v = Bohnemeyer2004.addedRole (Bohnemeyer2004.verbLinking v)

Transitivizing suffix vs linking

The overt transitivizing suffix is lexically specified and usually tracks the linking pattern, but the two can dissociate — the paper's central argument against aspect-based linking. The suffix is paper-specific lexical data, so it is recorded here against the Fragment's entries rather than in the Fragment.

inductive Bohnemeyer2004.TransitivizerSuffix : Type

A transitivizing suffix is the applicative -t or the causative -s.

• applicativeT : TransitivizerSuffix
• causativeS : TransitivizerSuffix

@[instance_reducible]

instance Bohnemeyer2004.instDecidableEqTransitivizerSuffix : DecidableEq TransitivizerSuffix

Equations

• Bohnemeyer2004.instDecidableEqTransitivizerSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bohnemeyer2004.instReprTransitivizerSuffix.repr : TransitivizerSuffix → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instReprTransitivizerSuffix : Repr TransitivizerSuffix

Equations

• Bohnemeyer2004.instReprTransitivizerSuffix = { reprPrec := Bohnemeyer2004.instReprTransitivizerSuffix.repr }

def Bohnemeyer2004.suffixTable : List (Verb × TransitivizerSuffix)

The suffix each verb the paper documents takes under transitivization (4), (5), (6), (7), (8), (9), (10), (11). The suffix is lexically idiosyncratic, since balak' and péek are both active and externally caused yet take -t and -s respectively.

Equations

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

def Bohnemeyer2004.transitivizerSuffix (v : Verb) : Option TransitivizerSuffix

The suffix of a documented verb; none for verbs the paper does not exemplify.

Equations

• Bohnemeyer2004.transitivizerSuffix v = List.lookup v Bohnemeyer2004.suffixTable

def Bohnemeyer2004.documented : List Verb

The verbs whose transitivization the paper exemplifies.

Equations

• Bohnemeyer2004.documented = List.map (fun (x : Bohnemeyer2004.Verb × Bohnemeyer2004.TransitivizerSuffix) => x.1) Bohnemeyer2004.suffixTable

What determines the linking

Causation type determines the alternation by rules (26)–(27). The paper's argument is that the properties competing accounts appeal to do not: each of lexical aspect (which is what [KW99]'s rule (14) reads), stem class, and the overt suffix leaves the linking open, witnessed by a minimal pair of documented verbs.

theorem Bohnemeyer2004.causation_determines_linking (v w : Verb) (h : v.causationType = w.causationType) : verbLinking v = verbLinking w

Causation type settles the alternation.

theorem Bohnemeyer2004.template_underdetermines_linking : stemTemplate meyah.stemClass = stemTemplate balak'.stemClass ∧ addedTermRole meyah ≠ addedTermRole balak'

Lexical aspect does not settle the alternation. Meyah 'work' and balak' 'roll' are both processes, with the same template, and they link differently, the counterexample to rule (14), which reads only lexical aspect ((4) vs (10)).

theorem Bohnemeyer2004.stemClass_underdetermines_linking : hàan.stemClass = kim.stemClass ∧ addedTermRole hàan ≠ addedTermRole kim

Stem class does not settle it either. Hàan 'eat' and kim 'die' are both inactive, and they link differently ((9) vs (6)).

theorem Bohnemeyer2004.suffix_underdetermines_linking : transitivizerSuffix meyah = transitivizerSuffix balak' ∧ addedTermRole meyah ≠ addedTermRole balak'

Nor does the overt suffix. Meyah and balak' both take -t, and they link differently: "balak' takes the applicative suffix –t when transitivized. However, the linking properties of the transitivized stem balak'-t are those of a causativized stem" (§6).

theorem Bohnemeyer2004.suffix_not_predictable : balak'.stemClass = péek.stemClass ∧ balak'.causationType = péek.causationType ∧ transitivizerSuffix balak' ≠ transitivizerSuffix péek

Nor does the suffix follow from causation type and stem class: balak' and péek agree on both and still differ in suffix ((8), (10)) — the dissociation runs in both directions.

theorem Bohnemeyer2004.documented_linking : (documented.all fun (v : Verb) => addedTermRole v == some (if (v.causationType == CausationType.internal) = true then Voice.TermRole.P else Voice.TermRole.A)) = true

Every documented verb links by its causation type: those with internally-caused bases add a P, the rest an A.

Degree achievements: event type vs aspect

theorem Bohnemeyer2004.kaan_is_state_change : (stemTemplate ka'n.stemClass).HasResultState

Degree achievements are event-structurally state changes, not processes, even though they behave atelically. The class takes the resultative -a'n ((19), ka'n-a'n-en 'I'm very tired') and incorporates the universal quantifier láah ((20), lúub-láah 'they fell completely'), which active intransitives do not, despite behaving atelically under (15) (§5).

theorem Bohnemeyer2004.naak_is_state_change : (stemTemplate na'k.stemClass).HasResultState

theorem Bohnemeyer2004.degree_achievements_causativize : addedTermRole ka'n = some Voice.TermRole.A ∧ addedTermRole na'k = some Voice.TermRole.A

Degree achievements transitivize like state-change verbs, adding an instigator as A rather than an applied object as P. This is the first direct counterevidence against Kraemer and Wunderlich's aspect-based linking, whose rule (14) treats them with the process verbs and so predicts applicativization; they causativize like every other state-change verb ((17) lists the class, (21) derives lúub 'fall').

theorem Bohnemeyer2004.haanEat_applicative_despite_inactive : hàan.stemClass = Yukatek.VerbStemClass.inactive ∧ addedTermRole hàan = some Voice.TermRole.P

hàan 'eat' is inactive by stem class yet internally caused, and it applicativizes ((9)): if stem class determined transitivization it would causativize like kim 'die'.

Bridge to detransitivization

The three Yukatek detransitivizations are instances of the cross-linguistic valency-alternation typology (Syntax/Voice/Alternation.lean). That substrate keeps passive and anticausative distinct by the fate of the initial A — passive denucleativizes it (retained in participant structure as a possible oblique agent), anticausative suppresses it (removed entirely).

inductive Bohnemeyer2004.DetransitivizationType : Type

The detransitivizations of Yukatek are those of rules (28)–(30). The antipassive (28) removes the caused event and retains the causing process, and active intransitives inflect like antipassive stems. The anticausative (29) removes the causing event and retains the caused one, and inactive intransitives inflect like anticausative stems. The passive (30) is like the anticausative but adds PROC_C and an instigator to the caused event.

• antipassive : DetransitivizationType
• anticausative : DetransitivizationType
• passive : DetransitivizationType

@[instance_reducible]

instance Bohnemeyer2004.instDecidableEqDetransitivizationType : DecidableEq DetransitivizationType

Equations

• Bohnemeyer2004.instDecidableEqDetransitivizationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bohnemeyer2004.instReprDetransitivizationType.repr : DetransitivizationType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bohnemeyer2004.instReprDetransitivizationType : Repr DetransitivizationType

Equations

• Bohnemeyer2004.instReprDetransitivizationType = { reprPrec := Bohnemeyer2004.instReprDetransitivizationType.repr }

def Bohnemeyer2004.DetransitivizationType.toVoice : DetransitivizationType → Voice

Each Yukatek detransitivization is a cross-linguistic valency alternation. The antipassive denucleativizes P and makes A the S, the anticausative suppresses A and makes P the S, and the passive denucleativizes A but retains it and makes P the S.

Equations

• Bohnemeyer2004.DetransitivizationType.antipassive.toVoice = Voice.antipassive
• Bohnemeyer2004.DetransitivizationType.anticausative.toVoice = Voice.anticausative
• Bohnemeyer2004.DetransitivizationType.passive.toVoice = Voice.passive

theorem Bohnemeyer2004.detransitivizations_decrease_valency : DetransitivizationType.antipassive.toVoice.IsValencyDecreasing ∧ DetransitivizationType.anticausative.toVoice.IsValencyDecreasing ∧ DetransitivizationType.passive.toVoice.IsValencyDecreasing

All three detransitivizations are valency-decreasing, as in the antipassive p'èeh, the passive p'e'h-el and the anticausative p'éeh-el of p'eh 'chip' (12).

theorem Bohnemeyer2004.passive_anticausative_distinct_by_A_fate : DetransitivizationType.passive.toVoice.fateOfRole Voice.TermRole.A = Voice.ParticipantFate.denucleativized ∧ DetransitivizationType.anticausative.toVoice.fateOfRole Voice.TermRole.A = Voice.ParticipantFate.suppressed

The fate of the initial A separates the passive from the anticausative, a distinction the coarser intransitivization typology collapses. The passive denucleativizes A, which stays in participant structure, and the anticausative suppresses it.

The subevent a detransitivized stem denotes

"Antipassives denote the causing event, while anticausatives and passives denote the caused event" (§6): each detransitivization keeps one subevent of its base's causal chain, whose participant is the derived stem's sole argument. (29) and (30) leave open whether the caused event is a state change, and the contact verbs that passivize and anticausativize may not entail one.

def Bohnemeyer2004.DetransitivizationType.retained : DetransitivizationType → Subevent

A stem detransitivized by d denotes the subevent d.retained, the causing event for the antipassive (28) and the caused event for the anticausative and the passive ((29)–(30)). The passive differs from the anticausative in participant structure, not in the subevent it denotes.

Equations

• Bohnemeyer2004.DetransitivizationType.antipassive.retained = Bohnemeyer2004.Subevent.causing
• Bohnemeyer2004.DetransitivizationType.anticausative.retained = Bohnemeyer2004.Subevent.caused
• Bohnemeyer2004.DetransitivizationType.passive.retained = Bohnemeyer2004.Subevent.caused

def Bohnemeyer2004.DetransitivizationType.template (d : DetransitivizationType) : ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event → Option (ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event)

The template a detransitivized stem denotes, the retained subevent of its base's template.

Equations

• d.template = d.retained.of

theorem Bohnemeyer2004.DetransitivizationType.isSome_template_iff (d : DetransitivizationType) (t : ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event) : (d.template t).isSome = true ↔ ∃ (c : ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event) (e : ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event), t = c.cause e

Rules (28)–(30) presuppose that only verbs encoding a causal relation between two subevents detransitivize.

def Bohnemeyer2004.pivotSourceRole (va : Voice) : Option Voice.TermRole

The initial role of the participant that a voice's derived construction privileges.

Equations

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

theorem Bohnemeyer2004.pivotSourceRole_toVoice (d : DetransitivizationType) : pivotSourceRole d.toVoice = some (termRole d.retained)

The sole argument of a detransitivized stem is the participant of the subevent it denotes, in the role (33) gives that subevent: the S of an antipassive was the A, that of an anticausative or a passive the P.

The rest of the inventory

def Bohnemeyer2004.externallyCaused : List Verb

The Fragment's externally-caused verbs span three stem classes, the manner-of-motion and sound-emission actives, the positionals ((25)) and the inactive degree achievements ((17)).

Equations

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

theorem Bohnemeyer2004.externally_caused_causativize : (externallyCaused.all fun (v : Verb) => v.causationType == CausationType.external && addedTermRole v == some Voice.TermRole.A) = true

Each of them is externally caused whatever its stem class, and so adds an instigator as A: stem class varies across the list while the linking does not.

Bridge to split ergativity

theorem Bohnemeyer2004.linking_consistent_with_split : Yukatek.alignment Yukatek.StatusCategory.completive = Alignment.AlignmentType.ergative ∧ Yukatek.alignment Yukatek.StatusCategory.incompletive = Alignment.AlignmentType.accusative

The linking-by-viewpoint mechanism derives the alignment the fragment records for each status category.

theorem Bohnemeyer2004.aspect_conditioned_split_family : Yukatek.alignment Yukatek.StatusCategory.completive = HindiUrdu.alignment Aspect.Perfectivity.perfective

Yukatek's split is aspect-conditioned like that of Hindi-Urdu, the completive aligning as the Hindi-Urdu perfective does.

Stem classes vs Lucy's root classes

[Luc94] classifies underived Yukatek roots by required transitiviser; this paper's five stem classes cut the same lexicon by status inflection. The comparison lives here because the paper engages Lucy's analysis directly — §5 argues degree achievements defeat its Vendlerian construal of these classes.

def Bohnemeyer2004.salienceClassOf : Yukatek.VerbStemClass → Option ArgumentStructure.SalienceClass

salienceClassOf c is the salience class of Lucy's that the stem class c corresponds to. The map is partial. inchoative stems derive from adjectival roots (completive -chah), which Lucy holds outside the predicate-root cut, and positional roots form Lucy's separate cross-cutting class (completive -lah); the two stem classes share only the anomalous incompletive -tal.

Equations

• Bohnemeyer2004.salienceClassOf Yukatek.VerbStemClass.active = some ArgumentStructure.SalienceClass.agent
• Bohnemeyer2004.salienceClassOf Yukatek.VerbStemClass.inactive = some ArgumentStructure.SalienceClass.patient
• Bohnemeyer2004.salienceClassOf Yukatek.VerbStemClass.transitiveActive = some ArgumentStructure.SalienceClass.agentPatient
• Bohnemeyer2004.salienceClassOf Yukatek.VerbStemClass.inchoative = none
• Bohnemeyer2004.salienceClassOf Yukatek.VerbStemClass.positional = none

theorem Bohnemeyer2004.salience_agrees_on_shared_roots : salienceClassOf kim.stemClass = Lucy1994.predictedClass Lucy1994.kiim ∧ salienceClassOf lúub.stemClass = Lucy1994.predictedClass Lucy1994.luub ∧ salienceClassOf na'k.stemClass = Lucy1994.predictedClass Lucy1994.naak

Where the two samples share a lexeme, stem class and Lucy's derived root class agree, for kim kíim 'die', lúub lúub' 'fall' and na'k ~ ná'ak 'ascend'.

theorem Bohnemeyer2004.haanEat_defies_transitiviser_diagnostic : transitivizerSuffix hàan = some TransitivizerSuffix.applicativeT ∧ salienceClassOf hàan.stemClass = some ArgumentStructure.SalienceClass.patient

Hàan 'eat' defeats a purely transitiviser-based classification. Its stem class maps to patient salient, yet it transitivizes with applicative -t, the exponent Lucy's diagnostic reads as agent salient. The suffix tracks internal causation, not class (9).

theorem Bohnemeyer2004.peek_stem_vs_root_class_divergence : salienceClassOf péek.stemClass = some ArgumentStructure.SalienceClass.agent ∧ Lucy1994.predictedClass Lucy1994.peek = some ArgumentStructure.SalienceClass.patient

Péek is active in this paper's classification, a manner-of-motion process with idiosyncratic causative -s, but a #-marked state-change root in Lucy's (4), so the two sources classify the same root differently.