Shared Mayan Fragment Infrastructure

@cite{coon-mateo-pedro-preminger-2014} @cite{imanishi-2020} @cite{tada-1993}

Types and parameters shared across Mayan language fragments (Q'anjob'al, Chol, Kaqchikel, K'iche', Mam, etc.).

The Mayan Absolutive Parameter

The position of absolutive agreement morphemes relative to the verb stem is an observable morphological parameter:

• HIGH-ABS: absolutive immediately follows the aspect marker (pre-stem). Template: ASP-ABS-ERG-ROOT-SUFFIX. Highland Guatemala languages.
• LOW-ABS: absolutive follows the verb stem (post-stem). Template: ASP-ERG-ROOT-SUFFIX-ABS. Lowland Mexico languages.

@cite{coon-mateo-pedro-preminger-2014} observe (extending @cite{tada-1993}) that this correlates with extraction asymmetries: overwhelmingly, HIGH-ABS languages exhibit syntactic ergativity while LOW-ABS languages do not.

Case Locus (theoretical interpretation)

The observable ABSPosition receives a theoretical interpretation in terms of which functional head assigns case to the transitive object:

• ABS=NOM (HIGH-ABS): Infl⁰ assigns case (= nominative) to transitive objects. "Absolutive" is a cover term for nominative.
• ABS=DEF (LOW-ABS): v⁰ assigns case (= accusative) to transitive objects. "Absolutive" is a cover term for accusative.

Both types assign ergative uniformly (via transitive v⁰) and nominative to intransitive subjects (via Infl⁰).

inductive Fragments.Mayan.ABSPosition : Type

The position of absolutive agreement morphemes relative to the verb stem. Observable from the linear order of morphemes in the verb-aspect complex — no theoretical commitment required.

• high : ABSPosition
• low : ABSPosition

instance Fragments.Mayan.instDecidableEqABSPosition : DecidableEq ABSPosition

Equations

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

def Fragments.Mayan.instBEqABSPosition.beq : ABSPosition → ABSPosition → Bool

Equations

• Fragments.Mayan.instBEqABSPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.instBEqABSPosition : BEq ABSPosition

Equations

• Fragments.Mayan.instBEqABSPosition = { beq := Fragments.Mayan.instBEqABSPosition.beq }

def Fragments.Mayan.instReprABSPosition.repr : ABSPosition → Nat → Std.Format

Equations

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

instance Fragments.Mayan.instReprABSPosition : Repr ABSPosition

Equations

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

inductive Fragments.Mayan.CaseLocus : Type

Abstract case assignment locus for transitive objects.

• absNom: Infl⁰ assigns case to transitive object (HIGH-ABS). @cite{legate-2008}'s ABS=NOM.
• absDef: v⁰ assigns case to transitive object (LOW-ABS). @cite{legate-2008}'s ABS=DEF.

• absNom : CaseLocus
• absDef : CaseLocus

instance Fragments.Mayan.instDecidableEqCaseLocus : DecidableEq CaseLocus

Equations

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

instance Fragments.Mayan.instBEqCaseLocus : BEq CaseLocus

Equations

• Fragments.Mayan.instBEqCaseLocus = { beq := Fragments.Mayan.instBEqCaseLocus.beq }

def Fragments.Mayan.instBEqCaseLocus.beq : CaseLocus → CaseLocus → Bool

Equations

• Fragments.Mayan.instBEqCaseLocus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Mayan.instReprCaseLocus.repr : CaseLocus → Nat → Std.Format

Equations

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

instance Fragments.Mayan.instReprCaseLocus : Repr CaseLocus

Equations

• Fragments.Mayan.instReprCaseLocus = { reprPrec := Fragments.Mayan.instReprCaseLocus.repr }

def Fragments.Mayan.toCaseLocus : ABSPosition → CaseLocus

Map the observable morphological parameter to the theoretical case-assignment locus.

Equations

• Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.high = Fragments.Mayan.CaseLocus.absNom
• Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.low = Fragments.Mayan.CaseLocus.absDef

inductive Fragments.Mayan.MarkerSet : Type

The two agreement marker paradigms found in Mayan languages. Set A and set B are the traditional Mayanist labels for the two cross-referencing paradigms on the verb.

These are framework-agnostic descriptive labels — they do not commit to an analysis of the markers as ergative, accusative, nominative, or absolutive.

• setA : MarkerSet

  Set A: cross-references ergative arguments (transitive agent) and genitives (possessors). Ergative and genitive are homophonous.

• setB : MarkerSet

  Set B: cross-references absolutive arguments (intransitive subject and, in ergative alignment, transitive patient).

instance Fragments.Mayan.instDecidableEqMarkerSet : DecidableEq MarkerSet

Equations

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

def Fragments.Mayan.instBEqMarkerSet.beq : MarkerSet → MarkerSet → Bool

Equations

• Fragments.Mayan.instBEqMarkerSet.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.instBEqMarkerSet : BEq MarkerSet

Equations

• Fragments.Mayan.instBEqMarkerSet = { beq := Fragments.Mayan.instBEqMarkerSet.beq }

instance Fragments.Mayan.instReprMarkerSet : Repr MarkerSet

Equations

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

def Fragments.Mayan.instReprMarkerSet.repr : MarkerSet → Nat → Std.Format

Equations

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