Yukatek Maya Verb Classes and Status System

Yukatek Maya has a typologically rare split-intransitive pattern of argument marking controlled by overt aspect-mood marking ([Boh04]; [Luc94]). The system comprises five verb stem classes distinguished by status inflection patterns (allomorphy of aspect-mood suffixes) and four status categories encoding viewpoint aspect and modal assertiveness. The split in argument marking tracks the aspectual value: perfective status marks S like U (ergative), imperfective status marks S like A (accusative).

Main declarations

• Yukatek.VerbStemClass: the five stem classes, with eventType, isIntransitive, toTemplate (R&H templates), and toSalienceClass ([Luc94]'s 4-way cut).
• Yukatek.StatusCategory: the four status categories, with viewpointAspect and isAssertive.
• Yukatek.sArgumentMarker: which marker set cross-references the intransitive subject, given the status category.
• Yukatek.yukatekSplit: the aspect-conditioned split as an Alignment.SplitErgativity, shared with Hindi and Georgian.

Implementation notes

Verb stem classes ([Boh04] Table 3; [Luc94]):

Class	Event type	Examples
active	process	walk, sing, dance, sneeze
inactive	state change	die, burst, enter, exit
inchoative	state change (stative root + -tal)	blacken, shrink, sink
positional	state change (spatial config.)	sit, stand, hang, be round
transitive active	transitive	hit, chip, eat

Status marking encodes both viewpoint aspect and modal assertiveness ([Boh04] Table 2):

• completive: +perfective, +assertive → ergative (S = U)
• subjunctive: +perfective, −assertive → ergative (S = U)
• incompletive: −perfective, +assertive → accusative (S = A)
• imperative: directive mood

Verb stem classes

inductive Yukatek.VerbStemClass : Type

The five verb stem classes of Yukatek Maya, distinguished by status inflection patterns ([Boh04] Table 3; [Luc94]).

• active : VerbStemClass
• inactive : VerbStemClass
• inchoative : VerbStemClass
• positional : VerbStemClass
• transitiveActive : VerbStemClass

@[implicit_reducible]

instance Yukatek.instDecidableEqVerbStemClass : DecidableEq VerbStemClass

Equations

• Yukatek.instDecidableEqVerbStemClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Yukatek.instReprVerbStemClass : Repr VerbStemClass

Equations

• Yukatek.instReprVerbStemClass = { reprPrec := Yukatek.instReprVerbStemClass.repr }

def Yukatek.instReprVerbStemClass.repr : VerbStemClass → ℕ → Std.Format

Equations

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

def Yukatek.VerbStemClass.eventType : VerbStemClass → ArgumentStructure.EventStructure.EventType

Event type per verb stem class: active stems encode processes, all others state changes. Per [Boh04] §5, atelic degree achievements still fall in the inactive and inchoative classes — class membership tracks the process vs state-change distinction, not telicity.

Equations

• Yukatek.VerbStemClass.active.eventType = ArgumentStructure.EventStructure.EventType.process
• Yukatek.VerbStemClass.inactive.eventType = ArgumentStructure.EventStructure.EventType.stateChange
• Yukatek.VerbStemClass.inchoative.eventType = ArgumentStructure.EventStructure.EventType.stateChange
• Yukatek.VerbStemClass.positional.eventType = ArgumentStructure.EventStructure.EventType.stateChange
• Yukatek.VerbStemClass.transitiveActive.eventType = ArgumentStructure.EventStructure.EventType.stateChange

def Yukatek.VerbStemClass.isIntransitive : VerbStemClass → Bool

Whether a verb stem class is intransitive.

Equations

• Yukatek.VerbStemClass.transitiveActive.isIntransitive = false
• x✝.isIntransitive = true

Status categories

inductive Yukatek.StatusCategory : Type

The four status categories of Yukatek Maya, encoding viewpoint aspect and modal assertiveness ([Boh04] Table 2).

• completive : StatusCategory
• subjunctive : StatusCategory
• incompletive : StatusCategory
• imperative : StatusCategory

@[implicit_reducible]

instance Yukatek.instDecidableEqStatusCategory : DecidableEq StatusCategory

Equations

• Yukatek.instDecidableEqStatusCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yukatek.instReprStatusCategory.repr : StatusCategory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Yukatek.instReprStatusCategory : Repr StatusCategory

Equations

• Yukatek.instReprStatusCategory = { reprPrec := Yukatek.instReprStatusCategory.repr }

def Yukatek.StatusCategory.viewpointAspect : StatusCategory → Option Semantics.Aspect.ViewpointAspectB

Aspectual value of a status category (the imperative has none).

Equations

• Yukatek.StatusCategory.completive.viewpointAspect = some Semantics.Aspect.ViewpointAspectB.perfective
• Yukatek.StatusCategory.subjunctive.viewpointAspect = some Semantics.Aspect.ViewpointAspectB.perfective
• Yukatek.StatusCategory.incompletive.viewpointAspect = some Semantics.Aspect.ViewpointAspectB.imperfective
• Yukatek.StatusCategory.imperative.viewpointAspect = none

def Yukatek.StatusCategory.isAssertive : StatusCategory → Bool

Whether the status category is assertive (modal component).

Equations

• Yukatek.StatusCategory.completive.isAssertive = true
• Yukatek.StatusCategory.incompletive.isAssertive = true
• x✝.isAssertive = false

Argument marking pattern

def Yukatek.sArgumentMarker : StatusCategory → Option Mayan.MarkerSet

Which marker set cross-references the sole argument (S) of an intransitive verb, given the status category ([Boh04] Table 2). Perfective status gives set-B (ergative, S = U), imperfective set-A (accusative, S = A); the imperative is omitted from Table 2's split analysis.

Equations

• Yukatek.sArgumentMarker Yukatek.StatusCategory.completive = some Mayan.MarkerSet.setB
• Yukatek.sArgumentMarker Yukatek.StatusCategory.subjunctive = some Mayan.MarkerSet.setB
• Yukatek.sArgumentMarker Yukatek.StatusCategory.incompletive = some Mayan.MarkerSet.setA
• Yukatek.sArgumentMarker Yukatek.StatusCategory.imperative = none

theorem Yukatek.perfective_ergative : sArgumentMarker StatusCategory.completive = some Mayan.MarkerSet.setB ∧ sArgumentMarker StatusCategory.subjunctive = some Mayan.MarkerSet.setB

The split: perfective → set-B (ergative), imperfective → set-A (accusative).

theorem Yukatek.imperfective_accusative : sArgumentMarker StatusCategory.incompletive = some Mayan.MarkerSet.setA

Representative verb entries

structure Yukatek.YukatekVerb : Type

A Yukatek verb entry for the split-intransitivity analysis: stem class and causation type of the intransitive base.

• gloss : String
• stemClass : VerbStemClass
• causationType : ArgumentStructure.EventStructure.InternalExternalCause

@[implicit_reducible]

instance Yukatek.instBEqYukatekVerb : BEq YukatekVerb

Equations

• Yukatek.instBEqYukatekVerb = { beq := Yukatek.instBEqYukatekVerb.beq }

def Yukatek.instBEqYukatekVerb.beq : YukatekVerb → YukatekVerb → Bool

Equations

• Yukatek.instBEqYukatekVerb.beq { gloss := a, stemClass := a_1, causationType := a_2 } { gloss := b, stemClass := b_1, causationType := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Yukatek.instBEqYukatekVerb.beq x✝¹ x✝ = false

def Yukatek.instReprYukatekVerb.repr : YukatekVerb → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Yukatek.instReprYukatekVerb : Repr YukatekVerb

Equations

• Yukatek.instReprYukatekVerb = { reprPrec := Yukatek.instReprYukatekVerb.repr }

def Yukatek.meyah : YukatekVerb

Equations

• Yukatek.meyah = { gloss := "work", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.internal }

def Yukatek.baaxal : YukatekVerb

Equations

• Yukatek.baaxal = { gloss := "play", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.internal }

def Yukatek.balak : YukatekVerb

Equations

• Yukatek.balak = { gloss := "roll", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.peek : YukatekVerb

Equations

• Yukatek.peek = { gloss := "move/wiggle", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.tsiirin : YukatekVerb

Equations

• Yukatek.tsiirin = { gloss := "buzz", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.kim : YukatekVerb

Equations

• Yukatek.kim = { gloss := "die", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.luub : YukatekVerb

Equations

• Yukatek.luub = { gloss := "fall", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.booxTal : YukatekVerb

Equations

• Yukatek.booxTal = { gloss := "blacken", stemClass := Yukatek.VerbStemClass.inchoative, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.chichanTal : YukatekVerb

Equations

• Yukatek.chichanTal = { gloss := "shrink", stemClass := Yukatek.VerbStemClass.inchoative, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.kaan : YukatekVerb

Equations

• Yukatek.kaan = { gloss := "get tired", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.naak : YukatekVerb

Equations

• Yukatek.naak = { gloss := "ascend", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.kulTal : YukatekVerb

Equations

• Yukatek.kulTal = { gloss := "sit down", stemClass := Yukatek.VerbStemClass.positional, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.waalTal : YukatekVerb

Equations

• Yukatek.waalTal = { gloss := "stand up", stemClass := Yukatek.VerbStemClass.positional, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.haanEat : YukatekVerb

Equations

• Yukatek.haanEat = { gloss := "eat", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.internal }

def Yukatek.chiik : YukatekVerb

Equations

• Yukatek.chiik = { gloss := "shake", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.haarax : YukatekVerb

Equations

• Yukatek.haarax = { gloss := "slide", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.huuy : YukatekVerb

Equations

• Yukatek.huuy = { gloss := "stir", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.mosoon : YukatekVerb

Equations

• Yukatek.mosoon = { gloss := "whirl", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.pirik : YukatekVerb

Equations

• Yukatek.pirik = { gloss := "flick", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.walak : YukatekVerb

Equations

• Yukatek.walak = { gloss := "turn/revolve", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.nikich : YukatekVerb

Equations

• Yukatek.nikich = { gloss := "squeak", stemClass := Yukatek.VerbStemClass.active, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.chilTal : YukatekVerb

Equations

• Yukatek.chilTal = { gloss := "lie down", stemClass := Yukatek.VerbStemClass.positional, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.xolTal : YukatekVerb

Equations

• Yukatek.xolTal = { gloss := "kneel", stemClass := Yukatek.VerbStemClass.positional, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.lab : YukatekVerb

Equations

• Yukatek.lab = { gloss := "deteriorate", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.tiil : YukatekVerb

Equations

• Yukatek.tiil = { gloss := "last/drag on", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.tsuuk : YukatekVerb

Equations

• Yukatek.tsuuk = { gloss := "rot", stemClass := Yukatek.VerbStemClass.inactive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.external }

def Yukatek.haats : YukatekVerb

Equations

• Yukatek.haats = { gloss := "hit", stemClass := Yukatek.VerbStemClass.transitiveActive, causationType := ArgumentStructure.EventStructure.InternalExternalCause.internal }

Event-structure templates

def Yukatek.VerbStemClass.toTemplate : VerbStemClass → ArgumentStructure.EventStructure.Template

Yukatek verb stem classes to R&H event-structure templates (EventStructure.lean): active → activity [x ACT], inactive and inchoative → achievement [BECOME [x ⟨STATE⟩]], positional → achievement (externally-caused spatial config.), transitive active → accomplishment [[x ACT] CAUSE [BECOME [y ⟨STATE⟩]]].

Equations

• Yukatek.VerbStemClass.active.toTemplate = ArgumentStructure.EventStructure.Template.activity
• Yukatek.VerbStemClass.inactive.toTemplate = ArgumentStructure.EventStructure.Template.achievement
• Yukatek.VerbStemClass.inchoative.toTemplate = ArgumentStructure.EventStructure.Template.achievement
• Yukatek.VerbStemClass.positional.toTemplate = ArgumentStructure.EventStructure.Template.achievement
• Yukatek.VerbStemClass.transitiveActive.toTemplate = ArgumentStructure.EventStructure.Template.accomplishment

theorem Yukatek.eventType_consistent (c : VerbStemClass) : c.eventType = c.toTemplate.eventType

The stem class → template mapping preserves event type: VerbStemClass.eventType agrees with Template.eventType ∘ toTemplate.

Salience classes ([Luc94])

def Yukatek.VerbStemClass.toSalienceClass : VerbStemClass → Verb.SalienceClass

Map [Boh04]'s 5-way Yukatek stem classification to [Luc94]'s 4-way salience cut. The 5-way is a refinement: inchoative and positional both pattern as Lucy's positional (both derive via -tal from a stative root); active/inactive/ transitiveActive map straightforwardly to agent/patient/ agentPatient.

Equations

• Yukatek.VerbStemClass.active.toSalienceClass = Verb.SalienceClass.agent
• Yukatek.VerbStemClass.inactive.toSalienceClass = Verb.SalienceClass.patient
• Yukatek.VerbStemClass.inchoative.toSalienceClass = Verb.SalienceClass.positional
• Yukatek.VerbStemClass.positional.toSalienceClass = Verb.SalienceClass.positional
• Yukatek.VerbStemClass.transitiveActive.toSalienceClass = Verb.SalienceClass.agentPatient

theorem Yukatek.inchoative_positional_collapse_under_lucy : VerbStemClass.inchoative.toSalienceClass = VerbStemClass.positional.toSalienceClass

Bohnemeyer's 5-way stem classes refining Lucy's positional class: inchoative and positional both reduce to the same Lucy class.

theorem Yukatek.active_inactive_transitive_distinct : VerbStemClass.active.toSalienceClass ≠ VerbStemClass.inactive.toSalienceClass ∧ VerbStemClass.active.toSalienceClass ≠ VerbStemClass.transitiveActive.toSalienceClass ∧ VerbStemClass.inactive.toSalienceClass ≠ VerbStemClass.transitiveActive.toSalienceClass

The other three Bohnemeyer classes are mutually distinct under Lucy's salience cut (they map to three different SalienceClass values).

theorem Yukatek.toSalienceClass_surjective (c : Verb.SalienceClass) : ∃ (s : VerbStemClass), s.toSalienceClass = c

toSalienceClass is surjective: every Lucy class is in the image of Bohnemeyer's 5-way refinement.

theorem Yukatek.toSalienceClass_fiber_positional (s : VerbStemClass) : s.toSalienceClass = Verb.SalienceClass.positional ↔ s = VerbStemClass.inchoative ∨ s = VerbStemClass.positional

The fibre of toSalienceClass over .positional is exactly {.inchoative, .positional} — these are the two Bohnemeyer classes that collapse under [Luc94]'s 4-way cut. The other three fibres are singletons (active ↦ agent, inactive ↦ patient, transitiveActive ↦ agentPatient).

theorem Yukatek.toSalienceClass_fiber_agent (s : VerbStemClass) : s.toSalienceClass = Verb.SalienceClass.agent ↔ s = VerbStemClass.active

The other three fibres are singletons.

theorem Yukatek.toSalienceClass_fiber_patient (s : VerbStemClass) : s.toSalienceClass = Verb.SalienceClass.patient ↔ s = VerbStemClass.inactive

theorem Yukatek.toSalienceClass_fiber_agentPatient (s : VerbStemClass) : s.toSalienceClass = Verb.SalienceClass.agentPatient ↔ s = VerbStemClass.transitiveActive

Split-ergative system

def Yukatek.yukatekSplit : Alignment.SplitErgativity StatusCategory

Yukatek split-ergative system, parameterized by status category: perfective status (completive/subjunctive) triggers ergative alignment, imperfective (incompletive) accusative; the imperative defaults to ergative. Instantiates the same Alignment.SplitErgativity used by Hindi and Georgian.

Equations

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

theorem Yukatek.yukatek_completive_erg : yukatekSplit.alignment StatusCategory.completive = Features.AlignmentFamily.ergative

theorem Yukatek.yukatek_subjunctive_erg : yukatekSplit.alignment StatusCategory.subjunctive = Features.AlignmentFamily.ergative

theorem Yukatek.yukatek_incompletive_acc : yukatekSplit.alignment StatusCategory.incompletive = Features.AlignmentFamily.accusative

theorem Yukatek.yukatek_hindi_same_split : yukatekSplit.alignment StatusCategory.completive = Alignment.hindiSplit.alignment Alignment.Aspect.perfective ∧ yukatekSplit.alignment StatusCategory.incompletive = Alignment.hindiSplit.alignment Alignment.Aspect.imperfective

Yukatek and Hindi share the same split conditioning: perfective → ergative, imperfective → accusative. This is [Boh04]'s core insight that a single linking-by-viewpoint mechanism underlies both systems.