Mayan person marking

Mayan languages cross-reference the arguments of the verb with two sets of person markers, called Set A and Set B by Mayanists. Set A marks the transitive subject and, on a noun, the possessor; Set B marks the intransitive subject and the transitive object. Both sets occupy fixed positions in the verbal complex, the word built from an aspect marker, the person markers, the verb stem and a status suffix, and the position of Set B divides the family: in the highland languages of Guatemala (K'ichean, Mamean, Q'anjob'alan) Set B follows the aspect marker and precedes the stem, while in the lowland languages (Cholan, Tseltalan, Yucatecan) it follows the stem. Coon, Mateo Pedro and Preminger call the two settings high and low absolutive, after Tada's observation that the high-absolutive languages ban the extraction of transitive subjects. Third person singular Set B has no segmental exponent in most of the family, a pattern Kaufman and Norman reconstruct for proto-Mayan. Many Mayan languages split their alignment by aspect or clause type, Set A extending to every subject in the non-perfective aspects or in clauses without an aspect marker; Aissen, England and Zavala survey the splits, which arose independently in Cholan, Q'anjob'alan and Yucatecan.

Main declarations

• Mayan.MarkerSet: Set A and Set B.
• Mayan.ExponentTable: a person-marker paradigm over the six person–number cells, with Mayan.ExponentTable.IsThirdSgZero for a null third person singular.
• Mayan.VerbSlot: the position classes of the verbal complex, and Mayan.absPosition, the Mayan.ABSPosition a verbal template determines.

Implementation notes

A paradigm is an Agreement.Paradigm over Agreement.Bundle.personNumberCells, so a controller's Word.phi indexes it directly, as in Corbett's account of agreement; an exponent is a list of Morphology.Morph, empty for zero exponence and of length two for a discontinuous marker such as a person prefix with a separate plural word. A cell whose only marker is a process also renders as []. Tables with pre-consonantal and pre-vocalic shapes are Phonology.Segment.Class → ExponentTable functions. Each language's fragment carries its own tables, its verbal template and its case function by aspect, so the position of the absolutive is read off the template rather than recorded beside it; quantification over the family is a study's, in Studies/CoonMateoPedroPreminger2014.lean.

References

• [AEZM17]
• [CMPP14]
• [Cor98]
• [KN84]
• [Tad93]

inductive Mayan.MarkerSet : Type

The two sets of person markers. Set A cross-references the transitive subject and the possessor, Set B the intransitive subject and the transitive object.

• setA : MarkerSet
• setB : MarkerSet

@[instance_reducible]

instance Mayan.instDecidableEqMarkerSet : DecidableEq MarkerSet

Equations

• Mayan.instDecidableEqMarkerSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Mayan.instReprMarkerSet : Repr MarkerSet

Equations

• Mayan.instReprMarkerSet = { reprPrec := Mayan.instReprMarkerSet.repr }

def Mayan.instReprMarkerSet.repr : MarkerSet → ℕ → Std.Format

Equations

• Mayan.instReprMarkerSet.repr Mayan.MarkerSet.setA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.MarkerSet.setA")).group prec✝
• Mayan.instReprMarkerSet.repr Mayan.MarkerSet.setB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.MarkerSet.setB")).group prec✝

@[instance_reducible]

instance Mayan.instFintypeMarkerSet : Fintype MarkerSet

Equations

• Mayan.instFintypeMarkerSet = { elems := { val := ↑Mayan.MarkerSet.enumList, nodup := Mayan.MarkerSet.enumList_nodup }, complete := Mayan.instFintypeMarkerSet._proof_1 }

@[reducible, inline]

abbrev Mayan.ExponentTable : Type

A person-marker paradigm: the exponent of each person–number cell, as a list of morphs.

Equations

• Mayan.ExponentTable = Agreement.Paradigm (List Morphology.Morph)

def Mayan.ExponentTable.IsThirdSgZero (e : ExponentTable) : Prop

The third person singular cell has no segmental exponent.

Equations

• e.IsThirdSgZero = (Agreement.Paradigm.realize e (Agreement.Bundle.personNumber Person.third Number.singular) = some [])

@[instance_reducible]

instance Mayan.instDecidableIsThirdSgZero (e : ExponentTable) : Decidable e.IsThirdSgZero

Equations

• Mayan.instDecidableIsThirdSgZero e = Mayan.instDecidableIsThirdSgZero._aux_1 e

The verbal complex

inductive Mayan.VerbSlot : Type

A position class of the verbal complex, in the Mayanist categories, which keep Set A and Set B apart. The stem is not a slot: a slot's side of a Morphology.AffixTemplate is its position relative to the stem.

• aspect : VerbSlot
• setB : VerbSlot
• setA : VerbSlot
• status : VerbSlot

@[instance_reducible]

instance Mayan.instDecidableEqVerbSlot : DecidableEq VerbSlot

Equations

• Mayan.instDecidableEqVerbSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mayan.instReprVerbSlot.repr : VerbSlot → ℕ → Std.Format

Equations

• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.aspect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.aspect")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.setB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.setB")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.setA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.setA")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.status prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.status")).group prec✝

@[instance_reducible]

instance Mayan.instReprVerbSlot : Repr VerbSlot

Equations

• Mayan.instReprVerbSlot = { reprPrec := Mayan.instReprVerbSlot.repr }

@[instance_reducible]

instance Mayan.instFintypeVerbSlot : Fintype VerbSlot

Equations

• Mayan.instFintypeVerbSlot = { elems := { val := ↑Mayan.VerbSlot.enumList, nodup := Mayan.VerbSlot.enumList_nodup }, complete := Mayan.instFintypeVerbSlot._proof_1 }

inductive Mayan.ABSPosition : Type

Set B sits high, between the aspect marker and the stem, or low, after the stem.

• high : ABSPosition
• low : ABSPosition

@[instance_reducible]

instance Mayan.instDecidableEqABSPosition : DecidableEq ABSPosition

Equations

• Mayan.instDecidableEqABSPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Mayan.instReprABSPosition : Repr ABSPosition

Equations

• Mayan.instReprABSPosition = { reprPrec := Mayan.instReprABSPosition.repr }

def Mayan.instReprABSPosition.repr : ABSPosition → ℕ → Std.Format

Equations

• Mayan.instReprABSPosition.repr Mayan.ABSPosition.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.ABSPosition.high")).group prec✝
• Mayan.instReprABSPosition.repr Mayan.ABSPosition.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.ABSPosition.low")).group prec✝

@[instance_reducible]

instance Mayan.instFintypeABSPosition : Fintype ABSPosition

Equations

• Mayan.instFintypeABSPosition = { elems := { val := ↑Mayan.ABSPosition.enumList, nodup := Mayan.ABSPosition.enumList_nodup }, complete := Mayan.instFintypeABSPosition._proof_1 }

def Mayan.absPosition (t : Morphology.AffixTemplate VerbSlot) : ABSPosition

A verbal template sets the absolutive high when Set B is a prefix slot.

Equations

• Mayan.absPosition t = if Mayan.VerbSlot.setB ∈ t.prefixSlots then Mayan.ABSPosition.high else Mayan.ABSPosition.low

theorem Mayan.absPosition_eq_high_iff (t : Morphology.AffixTemplate VerbSlot) : absPosition t = ABSPosition.high ↔ VerbSlot.setB ∈ t.prefixSlots