Documentation

Linglib.Fragments.Mayan.Yukatek.VerbClasses

Yukatek Maya Verb Classes and Status System #

@cite{bohnemeyer-2004} @cite{lucy-1994}

Yukatek Maya has a typologically rare split-intransitive pattern of argument marking controlled by overt aspect-mood marking. The system comprises five verb stem classes distinguished by their status inflection patterns (allomorphy of aspect-mood suffixes).

Verb Stem Classes #

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 Categories #

Status marking encodes both viewpoint aspect and modal assertiveness (@cite{bohnemeyer-2004} Table 2):

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

The split in argument marking is associated with the aspectual value: perfective status → S marked like U (ergative); imperfective status → S marked like A (accusative).

inductive Fragments.Mayan.Yukatek.VerbStemClass :

The five verb stem classes of Yukatek Maya, distinguished by status inflection patterns (@cite{bohnemeyer-2004} Table 3; @cite{lucy-1994}).

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

Instances For

@[implicit_reducible]

instance Fragments.Mayan.Yukatek.instDecidableEqVerbStemClass :

DecidableEq VerbStemClass

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Yukatek.instReprVerbStemClass :

Repr VerbStemClass

Equations

Fragments.Mayan.Yukatek.instReprVerbStemClass = { reprPrec := Fragments.Mayan.Yukatek.instReprVerbStemClass.repr }

def Fragments.Mayan.Yukatek.instReprVerbStemClass.repr :

VerbStemClass → ℕ → Std.Format

Equations

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

Instances For

def Fragments.Mayan.Yukatek.VerbStemClass.eventType :

VerbStemClass → Features.EventStructure.EventType

Event type encoded by each verb stem class. Active stems encode processes; all others encode state changes.

@cite{bohnemeyer-2004} §5: degree achievement verbs regularly appear in the inactive and inchoative classes despite being atelic. Their event structure encodes state change — the process/state-change distinction, not telicity, motivates class membership.

Equations

Instances For

def Fragments.Mayan.Yukatek.VerbStemClass.isIntransitive :

VerbStemClass → Bool

Whether a verb stem class is intransitive.

Equations

Fragments.Mayan.Yukatek.VerbStemClass.transitiveActive.isIntransitive = false
x✝.isIntransitive = true

Instances For

inductive Fragments.Mayan.Yukatek.StatusCategory :

The four status categories of Yukatek Maya, encoding viewpoint aspect and modal assertiveness (@cite{bohnemeyer-2004} Table 2).

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

Instances For

@[implicit_reducible]

instance Fragments.Mayan.Yukatek.instDecidableEqStatusCategory :

DecidableEq StatusCategory

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Yukatek.instReprStatusCategory :

Repr StatusCategory

Equations

Fragments.Mayan.Yukatek.instReprStatusCategory = { reprPrec := Fragments.Mayan.Yukatek.instReprStatusCategory.repr }

def Fragments.Mayan.Yukatek.instReprStatusCategory.repr :

StatusCategory → ℕ → Std.Format

Equations

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

Instances For

def Fragments.Mayan.Yukatek.StatusCategory.viewpointAspect :

StatusCategory → Option Semantics.Aspect.Core.ViewpointAspectB

Aspectual value of a status category. Completive and subjunctive are perfective; incompletive is imperfective. Imperative has no clear aspectual value.

Equations

Instances For

def Fragments.Mayan.Yukatek.StatusCategory.isAssertive :

StatusCategory → Bool

Whether the status category is assertive (modal component).

Equations

Fragments.Mayan.Yukatek.StatusCategory.completive.isAssertive = true
Fragments.Mayan.Yukatek.StatusCategory.incompletive.isAssertive = true
x✝.isAssertive = false

Instances For

def Fragments.Mayan.Yukatek.sArgumentMarker :

StatusCategory → Option MarkerSet

Which marker set cross-references the sole argument (S) of an intransitive verb, given the status category.

@cite{bohnemeyer-2004} Table 2:

Perfective status (completive/subjunctive): S = U → set-B (ergative)
Imperfective status (incompletive): S = A → set-A (accusative)
Imperative: not discussed in the split analysis (Table 2 omits it)

Equations

Instances For

theorem Fragments.Mayan.Yukatek.perfective_ergative :

sArgumentMarker StatusCategory.completive = some MarkerSet.setB ∧ sArgumentMarker StatusCategory.subjunctive = some MarkerSet.setB

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

theorem Fragments.Mayan.Yukatek.imperfective_accusative :

sArgumentMarker StatusCategory.incompletive = some MarkerSet.setA

structure Fragments.Mayan.Yukatek.YukatekVerb :

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

gloss : String
stemClass : VerbStemClass
causationType : Features.EventStructure.CausationType

Instances For

def Fragments.Mayan.Yukatek.instBEqYukatekVerb.beq :

YukatekVerb → YukatekVerb → Bool

Equations

One or more equations did not get rendered due to their size.
Fragments.Mayan.Yukatek.instBEqYukatekVerb.beq x✝¹ x✝ = false

Instances For

@[implicit_reducible]

instance Fragments.Mayan.Yukatek.instBEqYukatekVerb :

BEq YukatekVerb

Equations

Fragments.Mayan.Yukatek.instBEqYukatekVerb = { beq := Fragments.Mayan.Yukatek.instBEqYukatekVerb.beq }

@[implicit_reducible]

instance Fragments.Mayan.Yukatek.instReprYukatekVerb :

Repr YukatekVerb

Equations

Fragments.Mayan.Yukatek.instReprYukatekVerb = { reprPrec := Fragments.Mayan.Yukatek.instReprYukatekVerb.repr }

def Fragments.Mayan.Yukatek.instReprYukatekVerb.repr :

YukatekVerb → ℕ → Std.Format

Equations

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

Instances For

def Fragments.Mayan.Yukatek.meyah :

Equations

Fragments.Mayan.Yukatek.meyah = { gloss := "work", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.internal }

Instances For

def Fragments.Mayan.Yukatek.baaxal :

Equations

Fragments.Mayan.Yukatek.baaxal = { gloss := "play", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.internal }

Instances For

def Fragments.Mayan.Yukatek.balak :

Equations

Fragments.Mayan.Yukatek.balak = { gloss := "roll", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.peek :

Equations

Fragments.Mayan.Yukatek.peek = { gloss := "move/wiggle", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.tsiirin :

Equations

Fragments.Mayan.Yukatek.tsiirin = { gloss := "buzz", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.kim :

Equations

Fragments.Mayan.Yukatek.kim = { gloss := "die", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.luub :

Equations

Fragments.Mayan.Yukatek.luub = { gloss := "fall", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.booxTal :

Equations

Fragments.Mayan.Yukatek.booxTal = { gloss := "blacken", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inchoative, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.chichanTal :

Equations

Fragments.Mayan.Yukatek.chichanTal = { gloss := "shrink", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inchoative, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.kaan :

Equations

Fragments.Mayan.Yukatek.kaan = { gloss := "get tired", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.naak :

Equations

Fragments.Mayan.Yukatek.naak = { gloss := "ascend", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.kulTal :

Equations

Fragments.Mayan.Yukatek.kulTal = { gloss := "sit down", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.positional, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.waalTal :

Equations

Fragments.Mayan.Yukatek.waalTal = { gloss := "stand up", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.positional, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.haanEat :

Equations

Fragments.Mayan.Yukatek.haanEat = { gloss := "eat", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.internal }

Instances For

def Fragments.Mayan.Yukatek.chiik :

Equations

Fragments.Mayan.Yukatek.chiik = { gloss := "shake", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.haarax :

Equations

Fragments.Mayan.Yukatek.haarax = { gloss := "slide", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.huuy :

Equations

Fragments.Mayan.Yukatek.huuy = { gloss := "stir", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.mosoon :

Equations

Fragments.Mayan.Yukatek.mosoon = { gloss := "whirl", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.pirik :

Equations

Fragments.Mayan.Yukatek.pirik = { gloss := "flick", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.walak :

Equations

Fragments.Mayan.Yukatek.walak = { gloss := "turn/revolve", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.nikich :

Equations

Fragments.Mayan.Yukatek.nikich = { gloss := "squeak", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.chilTal :

Equations

Fragments.Mayan.Yukatek.chilTal = { gloss := "lie down", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.positional, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.xolTal :

Equations

Fragments.Mayan.Yukatek.xolTal = { gloss := "kneel", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.positional, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.lab :

Equations

Fragments.Mayan.Yukatek.lab = { gloss := "deteriorate", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.tiil :

Equations

Fragments.Mayan.Yukatek.tiil = { gloss := "last/drag on", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.tsuuk :

Equations

Fragments.Mayan.Yukatek.tsuuk = { gloss := "rot", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Features.EventStructure.CausationType.external }

Instances For

def Fragments.Mayan.Yukatek.haats :

Equations

Fragments.Mayan.Yukatek.haats = { gloss := "hit", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.transitiveActive, causationType := Features.EventStructure.CausationType.internal }

Instances For

def Fragments.Mayan.Yukatek.VerbStemClass.toTemplate :

VerbStemClass → Features.EventStructure.Template

Map Yukatek verb stem classes to R&H event structure templates. This connects the language-specific classification to the theory-level decomposition in EventStructure.lean.

Active → activity [x ACT]
Inactive/inchoative → achievement [BECOME [x ⟨STATE⟩]]
Positional → achievement (externally-caused spatial config.)
Transitive active → accomplishment [[x ACT] CAUSE [BECOME [y ⟨STATE⟩]]]

Equations

Instances For

theorem Fragments.Mayan.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.

def Fragments.Mayan.Yukatek.VerbStemClass.toSalienceClass :

VerbStemClass → Semantics.Lexical.Roots.SalienceClass

Map @cite{bohnemeyer-2004}'s 5-way Yukatek stem classification to @cite{lucy-1994}'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

Instances For

theorem Fragments.Mayan.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 Fragments.Mayan.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 Fragments.Mayan.Yukatek.toSalienceClass_surjective (c : Semantics.Lexical.Roots.SalienceClass) :

∃ (s : VerbStemClass), s.toSalienceClass = c

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

theorem Fragments.Mayan.Yukatek.toSalienceClass_fiber_positional (s : VerbStemClass) :

s.toSalienceClass = Semantics.Lexical.Roots.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 @cite{lucy-1994}'s 4-way cut. The other three fibres are singletons (active ↦ agent, inactive ↦ patient, transitiveActive ↦ agentPatient).

theorem Fragments.Mayan.Yukatek.toSalienceClass_fiber_agent (s : VerbStemClass) :

s.toSalienceClass = Semantics.Lexical.Roots.SalienceClass.agent ↔ s = VerbStemClass.active

The other three fibres are singletons.

theorem Fragments.Mayan.Yukatek.toSalienceClass_fiber_patient (s : VerbStemClass) :

s.toSalienceClass = Semantics.Lexical.Roots.SalienceClass.patient ↔ s = VerbStemClass.inactive

theorem Fragments.Mayan.Yukatek.toSalienceClass_fiber_agentPatient (s : VerbStemClass) :

s.toSalienceClass = Semantics.Lexical.Roots.SalienceClass.agentPatient ↔ s = VerbStemClass.transitiveActive

def Fragments.Mayan.Yukatek.yukatekSplit :

Core.SplitErgativity StatusCategory

Yukatek split-ergative system, parameterized by status category. Perfective status (completive/subjunctive) triggers ergative alignment; imperfective status (incompletive) triggers accusative alignment. Imperative is treated as ergative (completive-like default).

This instantiates the same Core.SplitErgativity type used by Hindi and Georgian, enabling cross-linguistic comparison.

Equations

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

Instances For

theorem Fragments.Mayan.Yukatek.yukatek_completive_erg :

yukatekSplit.alignment StatusCategory.completive = Core.AlignmentFamily.ergative

theorem Fragments.Mayan.Yukatek.yukatek_subjunctive_erg :

yukatekSplit.alignment StatusCategory.subjunctive = Core.AlignmentFamily.ergative

theorem Fragments.Mayan.Yukatek.yukatek_incompletive_acc :

yukatekSplit.alignment StatusCategory.incompletive = Core.AlignmentFamily.accusative

theorem Fragments.Mayan.Yukatek.yukatek_hindi_same_split :

yukatekSplit.alignment StatusCategory.completive = Core.hindiSplit.alignment Core.Aspect.perfective ∧ yukatekSplit.alignment StatusCategory.incompletive = Core.hindiSplit.alignment Core.Aspect.imperfective

Yukatek and Hindi share the same split conditioning: perfective → ergative, imperfective → accusative. This is @cite{bohnemeyer-2004}'s core insight that a single linking-by-viewpoint mechanism underlies both systems.