Imanishi (2020): Parameterizing Split Ergativity in Mayan

[Ima20]

Explains the alignment puzzle in the accusative (non-perfective) side of Mayan split-ergative systems.

The Alignment Puzzle

Kaqchikel, Chol, and Q'anjob'al all have (nearly) identical biclausal structures for non-perfective clauses — an aspectual predicate embedding a nominalized clause [Asp ... [vP_NMLZ]]. Yet:

• Kaqchikel: S/A = ABS (set B), O = ERG/GEN (set A)
• Chol/Q'anjob'al: S/A = ERG/GEN (set A), O = ABS (set B)

The Analysis

Two parameters explain the contrast:

1. Restriction on Nominalization (RON): The nominalizing head n in Kaqchikel obligatorily selects a vP lacking an external argument. In Chol and Q'anjob'al, n does not impose this restriction.

2. Mayan Absolutive Parameter ([CMPP14]): High absolutive languages (Kaqchikel, Q'anjob'al) have Infl as the locus of absolutive Case; low absolutive languages (Chol) have Voice.

The RON alone determines the alignment type: it controls which argument is the highest DP inside the nominalized clause and thus which receives genitive Case from D.

Intransitivization Strategies

The RON forces nominalized verbs in Kaqchikel to be intransitive. Three strategies satisfy this:

• Passivization: Voice[PASSIVE] suppresses the external argument
• Antipassivization: internal argument demoted to oblique
• Pseudo noun incorporation: object Case-licensed by adjacency

structure Imanishi2020.AccSidePattern : Type

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

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

• sMarker : Mayan.MarkerSet

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

• oMarker : Mayan.MarkerSet

  Marker set cross-referencing O (transitive object).

@[implicit_reducible]

instance Imanishi2020.instDecidableEqAccSidePattern : DecidableEq AccSidePattern

Equations

• Imanishi2020.instDecidableEqAccSidePattern = Imanishi2020.instDecidableEqAccSidePattern.decEq

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

Equations

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

def Imanishi2020.instReprAccSidePattern.repr : AccSidePattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Imanishi2020.instReprAccSidePattern : Repr AccSidePattern

Equations

• Imanishi2020.instReprAccSidePattern = { reprPrec := Imanishi2020.instReprAccSidePattern.repr }

def Imanishi2020.kaqchikelPattern : AccSidePattern

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

Equations

• Imanishi2020.kaqchikelPattern = { sMarker := Mayan.MarkerSet.setB, oMarker := Mayan.MarkerSet.setA }

def Imanishi2020.cholPattern : AccSidePattern

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

Equations

• Imanishi2020.cholPattern = { sMarker := Mayan.MarkerSet.setA, oMarker := Mayan.MarkerSet.setB }

theorem Imanishi2020.patterns_distinct : kaqchikelPattern ≠ cholPattern

The two accusative-side patterns are distinct.

theorem Imanishi2020.patterns_mirror : kaqchikelPattern.sMarker = cholPattern.oMarker ∧ kaqchikelPattern.oMarker = cholPattern.sMarker

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

structure Imanishi2020.RON : Type

The Restriction on Nominalization (RON): "Nominalized verbs must lack a syntactically projected external argument."

A property of the nominalizing head n in a given language. When active, n obligatorily selects for a vP without an external argument (i.e., no specifier of VoiceP projected inside the nominalized clause).

• active : Bool

def Imanishi2020.instDecidableEqRON.decEq (x✝ x✝¹ : RON) : Decidable (x✝ = x✝¹)

Equations

• Imanishi2020.instDecidableEqRON.decEq { active := a } { active := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Imanishi2020.instDecidableEqRON : DecidableEq RON

Equations

• Imanishi2020.instDecidableEqRON = Imanishi2020.instDecidableEqRON.decEq

def Imanishi2020.instReprRON.repr : RON → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Imanishi2020.instReprRON : Repr RON

Equations

• Imanishi2020.instReprRON = { reprPrec := Imanishi2020.instReprRON.repr }

structure Imanishi2020.MayanParams : Type

Parameters for a Mayan language's split-ergative system.

• ron : RON
• absPos : Mayan.ABSPosition

@[implicit_reducible]

instance Imanishi2020.instDecidableEqMayanParams : DecidableEq MayanParams

Equations

• Imanishi2020.instDecidableEqMayanParams = Imanishi2020.instDecidableEqMayanParams.decEq

def Imanishi2020.instDecidableEqMayanParams.decEq (x✝ x✝¹ : MayanParams) : Decidable (x✝ = x✝¹)

Equations

• Imanishi2020.instDecidableEqMayanParams.decEq { ron := a, absPos := a_1 } { ron := b, absPos := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Imanishi2020.instReprMayanParams.repr : MayanParams → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Imanishi2020.instReprMayanParams : Repr MayanParams

Equations

• Imanishi2020.instReprMayanParams = { reprPrec := Imanishi2020.instReprMayanParams.repr }

def Imanishi2020.kaqchikelParams : MayanParams

Kaqchikel: RON active, high absolutive.

Equations

• Imanishi2020.kaqchikelParams = { ron := { active := true }, absPos := Mayan.ABSPosition.high }

def Imanishi2020.cholParams : MayanParams

Chol: RON inactive, low absolutive.

Equations

• Imanishi2020.cholParams = { ron := { active := false }, absPos := Mayan.ABSPosition.low }

def Imanishi2020.qanjobalParams : MayanParams

Q'anjob'al: RON inactive, high absolutive.

Equations

• Imanishi2020.qanjobalParams = { ron := { active := false }, absPos := Mayan.ABSPosition.high }

structure Imanishi2020.NomClause : Type

Structure of the nominalized clause embedded under the aspectual predicate on the accusative side. The clause is [DP [nP [vP [VoiceP [VP]]]]] — verbal projections dominated by nominal projections.

The key structural variable: whether an external argument is syntactically projected inside the nominalized clause. Determined by the RON.

• hasExternalArg : Bool
• hasInternalArg : Bool

def Imanishi2020.instDecidableEqNomClause.decEq (x✝ x✝¹ : NomClause) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Imanishi2020.instDecidableEqNomClause : DecidableEq NomClause

Equations

• Imanishi2020.instDecidableEqNomClause = Imanishi2020.instDecidableEqNomClause.decEq

def Imanishi2020.instReprNomClause.repr : NomClause → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Imanishi2020.instReprNomClause : Repr NomClause

Equations

• Imanishi2020.instReprNomClause = { reprPrec := Imanishi2020.instReprNomClause.repr }

def Imanishi2020.nomClauseFromRON (ron : RON) (transitive : Bool) : NomClause

Build the nominalized clause from the RON and transitivity.

Equations

• Imanishi2020.nomClauseFromRON ron transitive = { hasExternalArg := !ron.active && transitive, hasInternalArg := transitive }

def Imanishi2020.deriveAccPattern (params : MayanParams) : AccSidePattern

Derive the accusative-side alignment pattern from language parameters.

The D head of the nominalized clause assigns genitive Case to the structurally closest (highest) DP. Since ERG and GEN are homophonous in Mayan (both realized as set A markers), the DP receiving GEN is cross-referenced by set A.

• RON active → no external arg → internal arg is highest DP → set A on O
• RON inactive → external arg present → external arg is highest → set A on S

Equations

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

theorem Imanishi2020.kaqchikel_alignment : deriveAccPattern kaqchikelParams = kaqchikelPattern

Kaqchikel's parameters derive the Kaqchikel alignment pattern.

theorem Imanishi2020.chol_alignment : deriveAccPattern cholParams = cholPattern

Chol's parameters derive the Chol alignment pattern.

theorem Imanishi2020.qanjobal_alignment : deriveAccPattern qanjobalParams = cholPattern

Q'anjob'al's parameters derive the Chol pattern (same as Chol).

theorem Imanishi2020.ron_determines_alignment (abs : Mayan.ABSPosition) : deriveAccPattern { ron := { active := true }, absPos := abs } = kaqchikelPattern ∧ deriveAccPattern { ron := { active := false }, absPos := abs } = cholPattern

The RON alone determines the alignment type, regardless of ABSPosition. This is the paper's central result: the alignment puzzle reduces to a single binary parameter on the nominalizing head.

theorem Imanishi2020.absPos_insufficient : kaqchikelParams.absPos = qanjobalParams.absPos ∧ deriveAccPattern kaqchikelParams ≠ deriveAccPattern qanjobalParams

Q'anjob'al and Kaqchikel share ABSPosition but differ in alignment — confirming that ABSPosition alone does not determine the accusative-side alignment.

theorem Imanishi2020.passive_satisfies_ron : ¬Minimalist.voicePassive.AssignsTheta

Passive Voice satisfies the RON: no θ-role assignment means no external argument is projected.

theorem Imanishi2020.agentive_violates_ron : Minimalist.voiceAgent.AssignsTheta

Agentive Voice violates the RON: it projects an external argument.

def Imanishi2020.RonCompatibleVoice (v : Minimalist.VoiceHead) : Prop

A Voice head is compatible with the RON iff it does not assign a θ-role (and hence does not project an external argument).

Equations

• Imanishi2020.RonCompatibleVoice v = ¬v.AssignsTheta

@[implicit_reducible]

instance Imanishi2020.instDecidableRonCompatibleVoice (v : Minimalist.VoiceHead) : Decidable (RonCompatibleVoice v)

Equations

• Imanishi2020.instDecidableRonCompatibleVoice v = id inferInstance

theorem Imanishi2020.passive_ron_compatible : RonCompatibleVoice Minimalist.voicePassive

theorem Imanishi2020.agentive_ron_incompatible : ¬RonCompatibleVoice Minimalist.voiceAgent

theorem Imanishi2020.anticausative_ron_compatible : RonCompatibleVoice Minimalist.voiceAnticausative

theorem Imanishi2020.kaqchikel_perfective_bridge : Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.A = Case.erg ∧ Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.P = Case.abs ∧ Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.S = Case.abs

Kaqchikel's perfective (ergative) case assignment from the existing fragment: A = ERG, S = P = ABS. Confirms the ergative side is shared across all three languages.

theorem Imanishi2020.chol_perfective_bridge : Chol.ArgPosition.case Features.Prominence.ArgumentRole.A = Case.erg ∧ Chol.ArgPosition.case Features.Prominence.ArgumentRole.P = Case.abs ∧ Chol.ArgPosition.case Features.Prominence.ArgumentRole.S = Case.abs

Chol's perfective alignment matches the same ergative pattern.

theorem Imanishi2020.qanjobal_perfective_bridge : Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.A = Case.erg ∧ Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.P = Case.abs ∧ Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.S = Case.abs

Q'anjob'al's perfective alignment matches the same ergative pattern.

theorem Imanishi2020.shared_ergative : Kaqchikel.ArgPosition.case Features.Prominence.ArgumentRole.A = Chol.ArgPosition.case Features.Prominence.ArgumentRole.A ∧ Chol.ArgPosition.case Features.Prominence.ArgumentRole.A = Qanjobal.ArgPosition.case Features.Prominence.ArgumentRole.A

All three languages share ergative alignment in the perfective.

def Imanishi2020.caseToMarker : Case → Mayan.MarkerSet

Map Minimalist case values to the Mayan marker set that realizes them. ERG and GEN are both realized by set A (they are homophonous in Mayan). ABS is realized by set B. The wildcard maps non-Mayan cases (NOM, ACC, DAT, etc.) to set A — these should never appear in Mayan fragments.

Equations

• Imanishi2020.caseToMarker Case.erg = Mayan.MarkerSet.setA
• Imanishi2020.caseToMarker Case.gen = Mayan.MarkerSet.setA
• Imanishi2020.caseToMarker Case.abs = Mayan.MarkerSet.setB
• Imanishi2020.caseToMarker x✝ = Mayan.MarkerSet.setA

theorem Imanishi2020.erg_gen_homophonous : caseToMarker Case.erg = caseToMarker Case.gen

ERG/GEN homophony: both map to set A.

theorem Imanishi2020.chol_case_to_marker_bridge : caseToMarker (Chol.ArgPosition.accCase Features.Prominence.ArgumentRole.A) = cholPattern.sMarker ∧ caseToMarker (Chol.ArgPosition.accCase Features.Prominence.ArgumentRole.P) = cholPattern.oMarker

Chol's fragment case values, mapped through the Mayan marker bridge, yield the predicted accusative-side pattern.

theorem Imanishi2020.qanjobal_case_to_marker_bridge : caseToMarker (Qanjobal.ArgPosition.accCase Features.Prominence.ArgumentRole.A) = cholPattern.sMarker ∧ caseToMarker (Qanjobal.ArgPosition.accCase Features.Prominence.ArgumentRole.P) = cholPattern.oMarker

Q'anjob'al's fragment case values yield the same pattern as Chol.

theorem Imanishi2020.kaqchikel_case_to_marker_bridge : caseToMarker (Kaqchikel.ArgPosition.accCase Features.Prominence.ArgumentRole.A) = kaqchikelPattern.sMarker ∧ caseToMarker (Kaqchikel.ArgPosition.accCase Features.Prominence.ArgumentRole.P) = kaqchikelPattern.oMarker

Kaqchikel's fragment accusative-side case values, mapped through the Mayan marker bridge, yield the predicted Kaqchikel alignment pattern.

theorem Imanishi2020.acc_case_mirror : Kaqchikel.ArgPosition.accCase Features.Prominence.ArgumentRole.A = Chol.ArgPosition.accCase Features.Prominence.ArgumentRole.P ∧ Kaqchikel.ArgPosition.accCase Features.Prominence.ArgumentRole.P = Chol.ArgPosition.accCase Features.Prominence.ArgumentRole.A

The accusative-side case contrast between Kaqchikel and Chol is a true mirror image: agent and patient cases are swapped.

theorem Imanishi2020.end_to_end_all_languages : (caseToMarker (Kaqchikel.ArgPosition.accCase Features.Prominence.ArgumentRole.A) = (deriveAccPattern kaqchikelParams).sMarker ∧ caseToMarker (Kaqchikel.ArgPosition.accCase Features.Prominence.ArgumentRole.P) = (deriveAccPattern kaqchikelParams).oMarker) ∧ (caseToMarker (Chol.ArgPosition.accCase Features.Prominence.ArgumentRole.A) = (deriveAccPattern cholParams).sMarker ∧ caseToMarker (Chol.ArgPosition.accCase Features.Prominence.ArgumentRole.P) = (deriveAccPattern cholParams).oMarker) ∧ caseToMarker (Qanjobal.ArgPosition.accCase Features.Prominence.ArgumentRole.A) = (deriveAccPattern qanjobalParams).sMarker ∧ caseToMarker (Qanjobal.ArgPosition.accCase Features.Prominence.ArgumentRole.P) = (deriveAccPattern qanjobalParams).oMarker

End-to-end: for all three languages, the fragment case data (mapped through the marker bridge) matches the parametrically derived pattern. This closes the argumentation chain from parameters → alignment → case → markers.

def Imanishi2020.mayanSplit : Alignment.SplitErgativity Alignment.Aspect

The Mayan split is aspect-conditioned: perfective → ergative, non-perfective → accusative. Instantiates the same SplitErgativity infrastructure as the Hindi example in Alignment.SplitErgativity.

Equations

• Imanishi2020.mayanSplit = { ergCondition := fun (a : Alignment.Aspect) => a == Alignment.Aspect.perfective }

theorem Imanishi2020.mayan_perfective_erg : mayanSplit.alignment Alignment.Aspect.perfective = Features.AlignmentFamily.ergative

theorem Imanishi2020.mayan_imperfective_acc : mayanSplit.alignment Alignment.Aspect.imperfective = Features.AlignmentFamily.accusative

theorem Imanishi2020.mayan_hindi_same_split : mayanSplit = Alignment.hindiSplit

Mayan and Hindi have the same aspect-conditioned split direction: perfective triggers ergativity in both language families.

theorem Imanishi2020.cmp2014_ergativity_from_params (p : MayanParams) : CoonMateoPedroPreminger2014.hasSyntacticErgativity (Mayan.toCaseLocus p.absPos) = (p.absPos == Mayan.ABSPosition.high)

Imanishi's RON determines the accusative-side alignment (this study), while CMP2014's CaseLocus determines syntactic ergativity (ergative side). Together they form the full Mayan parameterization: RON for the accusative side, ABSPosition→CaseLocus for the ergative side.

theorem Imanishi2020.kaqchikel_full_profile : deriveAccPattern kaqchikelParams = kaqchikelPattern ∧ CoonMateoPedroPreminger2014.hasSyntacticErgativity (Mayan.toCaseLocus kaqchikelParams.absPos) = true

The two studies agree on Kaqchikel: RON active + HIGH-ABS = syntactic ergativity + Kaqchikel-type accusative alignment.

theorem Imanishi2020.chol_full_profile : deriveAccPattern cholParams = cholPattern ∧ CoonMateoPedroPreminger2014.hasSyntacticErgativity (Mayan.toCaseLocus cholParams.absPos) = false

The two studies agree on Chol: RON inactive + LOW-ABS = no syntactic ergativity + Chol-type accusative alignment.

theorem Imanishi2020.qanjobal_cross_cutting : CoonMateoPedroPreminger2014.hasSyntacticErgativity (Mayan.toCaseLocus qanjobalParams.absPos) = true ∧ deriveAccPattern qanjobalParams = cholPattern

Q'anjob'al shows that the two dimensions are independent: HIGH-ABS (like Kaqchikel) but RON inactive (like Chol). Syntactic ergativity yes, but Chol-type accusative alignment.