The Mayan Alignment Puzzle

@cite{imanishi-2020} @cite{coon-2013a} @cite{dixon-1994}

Theory-neutral observations about the accusative side of Mayan split ergativity. In perfective aspect, Mayan languages uniformly show ergative alignment. In non-perfective aspect, they switch to accusative alignment — but the specific alignment patterns differ across languages.

The Puzzle

Kaqchikel, Chol, and Q'anjob'al have (nearly) identical biclausal structures for non-perfective clauses, yet display contrastive alignment patterns.

Kaqchikel type (S = ABS, O = ERG/GEN): Both S and A are cross-referenced by absolutive (set B) markers. The transitive object is cross-referenced by ergative/genitive (set A).

Chol/Q'anjob'al type (S = ERG/GEN, O = ABS): Both S and A are cross-referenced by ergative/genitive (set A) markers. The transitive object is cross-referenced by absolutive (set B).

structure Phenomena.Ergativity.AccSidePattern : Type

Alignment pattern in the accusative (non-perfective) side of the split. Records which marker set cross-references S (= A on accusative side) and which cross-references O.

• sMarker : MarkerSet

  Marker set cross-referencing S (intransitive subject) and A (transitive subject) — these pattern together on the accusative side.

• oMarker : MarkerSet

  Marker set cross-referencing O (transitive object).

instance Phenomena.Ergativity.instDecidableEqAccSidePattern : DecidableEq AccSidePattern

Equations

• Phenomena.Ergativity.instDecidableEqAccSidePattern = Phenomena.Ergativity.instDecidableEqAccSidePattern.decEq

def Phenomena.Ergativity.instDecidableEqAccSidePattern.decEq (x✝ x✝¹ : AccSidePattern) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Ergativity.instBEqAccSidePattern : BEq AccSidePattern

Equations

• Phenomena.Ergativity.instBEqAccSidePattern = { beq := Phenomena.Ergativity.instBEqAccSidePattern.beq }

def Phenomena.Ergativity.instBEqAccSidePattern.beq : AccSidePattern → AccSidePattern → Bool

Equations

• Phenomena.Ergativity.instBEqAccSidePattern.beq { sMarker := a, oMarker := a_1 } { sMarker := b, oMarker := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Ergativity.instBEqAccSidePattern.beq x✝¹ x✝ = false

def Phenomena.Ergativity.instReprAccSidePattern.repr : AccSidePattern → Nat → Std.Format

Equations

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

instance Phenomena.Ergativity.instReprAccSidePattern : Repr AccSidePattern

Equations

• Phenomena.Ergativity.instReprAccSidePattern = { reprPrec := Phenomena.Ergativity.instReprAccSidePattern.repr }

def Phenomena.Ergativity.kaqchikelPattern : AccSidePattern

Kaqchikel-type accusative alignment: S/A = set B (ABS), O = set A (ERG/GEN).

Equations

• Phenomena.Ergativity.kaqchikelPattern = { sMarker := Fragments.Mayan.MarkerSet.setB, oMarker := Fragments.Mayan.MarkerSet.setA }

def Phenomena.Ergativity.cholPattern : AccSidePattern

Chol/Q'anjob'al-type accusative alignment: S/A = set A (ERG/GEN), O = set B (ABS).

Equations

• Phenomena.Ergativity.cholPattern = { sMarker := Fragments.Mayan.MarkerSet.setA, oMarker := Fragments.Mayan.MarkerSet.setB }

theorem Phenomena.Ergativity.patterns_distinct : kaqchikelPattern ≠ cholPattern

The two accusative-side patterns are distinct.

theorem Phenomena.Ergativity.patterns_mirror : kaqchikelPattern.sMarker = cholPattern.oMarker ∧ kaqchikelPattern.oMarker = cholPattern.sMarker

The two patterns are mirror images: the marker sets are swapped.

structure Phenomena.Ergativity.MayanExtractionDatum : Type

A Mayan language's observable extraction behavior.

• name : String
• absPosition : ABSPosition
• hasExtractionAsymmetry : Bool

  Does the language ban A-bar extraction of transitive subjects?

instance Phenomena.Ergativity.instDecidableEqMayanExtractionDatum : DecidableEq MayanExtractionDatum

Equations

• Phenomena.Ergativity.instDecidableEqMayanExtractionDatum = Phenomena.Ergativity.instDecidableEqMayanExtractionDatum.decEq

def Phenomena.Ergativity.instDecidableEqMayanExtractionDatum.decEq (x✝ x✝¹ : MayanExtractionDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Ergativity.instBEqMayanExtractionDatum : BEq MayanExtractionDatum

Equations

• Phenomena.Ergativity.instBEqMayanExtractionDatum = { beq := Phenomena.Ergativity.instBEqMayanExtractionDatum.beq }

def Phenomena.Ergativity.instBEqMayanExtractionDatum.beq : MayanExtractionDatum → MayanExtractionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Ergativity.instBEqMayanExtractionDatum.beq x✝¹ x✝ = false

instance Phenomena.Ergativity.instReprMayanExtractionDatum : Repr MayanExtractionDatum

Equations

• Phenomena.Ergativity.instReprMayanExtractionDatum = { reprPrec := Phenomena.Ergativity.instReprMayanExtractionDatum.repr }

def Phenomena.Ergativity.instReprMayanExtractionDatum.repr : MayanExtractionDatum → Nat → Std.Format

Equations

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

def Phenomena.Ergativity.tadasTable : List MayanExtractionDatum

Tada's Generalization data (table (19) of @cite{coon-mateo-pedro-preminger-2014}, extending @cite{tada-1993}).

The two noted outliers are Yucatec and Ixil (LOW-ABS with extraction asymmetries). Yucatec's AF differs significantly from other Mayan AF; Ixil's absolutive morphemes behave like full pronominal forms.

Equations

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

theorem Phenomena.Ergativity.high_abs_all_have_asymmetries : ((List.filter (fun (l : MayanExtractionDatum) => l.absPosition == Fragments.Mayan.ABSPosition.high) tadasTable).all fun (l : MayanExtractionDatum) => l.hasExtractionAsymmetry) = true

All HIGH-ABS languages in the sample exhibit extraction asymmetries.

theorem Phenomena.Ergativity.low_abs_mostly_lack_asymmetries : ((List.filter (fun (l : MayanExtractionDatum) => l.absPosition == Fragments.Mayan.ABSPosition.low && l.name != "Yucatec" && l.name != "Ixil") tadasTable).all fun (l : MayanExtractionDatum) => !l.hasExtractionAsymmetry) = true

All LOW-ABS languages except the two noted outliers lack extraction asymmetries.

theorem Phenomena.Ergativity.high_abs_none_lack_asymmetries : (List.filter (fun (l : MayanExtractionDatum) => l.absPosition == Fragments.Mayan.ABSPosition.high && !l.hasExtractionAsymmetry) tadasTable).length = 0

No HIGH-ABS language lacks extraction asymmetries (unattested cell).