Imanishi (2020): Parameterizing Split Ergativity in Mayan

@cite{imanishi-2020}

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 (@cite{coon-mateo-pedro-preminger-2014}): 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 Phenomena.Ergativity.Studies.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

instance Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqRON : DecidableEq RON

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqRON = Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqRON.decEq

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

Equations

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

instance Phenomena.Ergativity.Studies.Imanishi2020.instBEqRON : BEq RON

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instBEqRON = { beq := Phenomena.Ergativity.Studies.Imanishi2020.instBEqRON.beq }

def Phenomena.Ergativity.Studies.Imanishi2020.instBEqRON.beq : RON → RON → Bool

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instBEqRON.beq { active := a } { active := b } = (a == b)
• Phenomena.Ergativity.Studies.Imanishi2020.instBEqRON.beq x✝¹ x✝ = false

def Phenomena.Ergativity.Studies.Imanishi2020.instReprRON.repr : RON → ℕ → Std.Format

Equations

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

instance Phenomena.Ergativity.Studies.Imanishi2020.instReprRON : Repr RON

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instReprRON = { reprPrec := Phenomena.Ergativity.Studies.Imanishi2020.instReprRON.repr }

structure Phenomena.Ergativity.Studies.Imanishi2020.MayanParams : Type

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

• ron : RON
• absPos : ABSPosition

instance Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqMayanParams : DecidableEq MayanParams

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqMayanParams = Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqMayanParams.decEq

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

Equations

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

instance Phenomena.Ergativity.Studies.Imanishi2020.instBEqMayanParams : BEq MayanParams

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instBEqMayanParams = { beq := Phenomena.Ergativity.Studies.Imanishi2020.instBEqMayanParams.beq }

def Phenomena.Ergativity.Studies.Imanishi2020.instBEqMayanParams.beq : MayanParams → MayanParams → Bool

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instBEqMayanParams.beq { ron := a, absPos := a_1 } { ron := b, absPos := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Ergativity.Studies.Imanishi2020.instBEqMayanParams.beq x✝¹ x✝ = false

def Phenomena.Ergativity.Studies.Imanishi2020.instReprMayanParams.repr : MayanParams → ℕ → Std.Format

Equations

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

instance Phenomena.Ergativity.Studies.Imanishi2020.instReprMayanParams : Repr MayanParams

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instReprMayanParams = { reprPrec := Phenomena.Ergativity.Studies.Imanishi2020.instReprMayanParams.repr }

def Phenomena.Ergativity.Studies.Imanishi2020.kaqchikelParams : MayanParams

Kaqchikel: RON active, high absolutive.

Equations

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

def Phenomena.Ergativity.Studies.Imanishi2020.cholParams : MayanParams

Chol: RON inactive, low absolutive.

Equations

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

def Phenomena.Ergativity.Studies.Imanishi2020.qanjobalParams : MayanParams

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

Equations

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

structure Phenomena.Ergativity.Studies.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 Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqNomClause.decEq (x✝ x✝¹ : NomClause) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqNomClause : DecidableEq NomClause

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqNomClause = Phenomena.Ergativity.Studies.Imanishi2020.instDecidableEqNomClause.decEq

instance Phenomena.Ergativity.Studies.Imanishi2020.instBEqNomClause : BEq NomClause

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instBEqNomClause = { beq := Phenomena.Ergativity.Studies.Imanishi2020.instBEqNomClause.beq }

def Phenomena.Ergativity.Studies.Imanishi2020.instBEqNomClause.beq : NomClause → NomClause → Bool

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instBEqNomClause.beq { hasExternalArg := a, hasInternalArg := a_1 } { hasExternalArg := b, hasInternalArg := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Ergativity.Studies.Imanishi2020.instBEqNomClause.beq x✝¹ x✝ = false

instance Phenomena.Ergativity.Studies.Imanishi2020.instReprNomClause : Repr NomClause

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.instReprNomClause = { reprPrec := Phenomena.Ergativity.Studies.Imanishi2020.instReprNomClause.repr }

def Phenomena.Ergativity.Studies.Imanishi2020.instReprNomClause.repr : NomClause → ℕ → Std.Format

Equations

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

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

Build the nominalized clause from the RON and transitivity.

Equations

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

def Phenomena.Ergativity.Studies.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 Phenomena.Ergativity.Studies.Imanishi2020.kaqchikel_alignment : deriveAccPattern kaqchikelParams = kaqchikelPattern

Kaqchikel's parameters derive the Kaqchikel alignment pattern.

theorem Phenomena.Ergativity.Studies.Imanishi2020.chol_alignment : deriveAccPattern cholParams = cholPattern

Chol's parameters derive the Chol alignment pattern.

theorem Phenomena.Ergativity.Studies.Imanishi2020.qanjobal_alignment : deriveAccPattern qanjobalParams = cholPattern

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.ron_determines_alignment (abs : 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 Phenomena.Ergativity.Studies.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 Phenomena.Ergativity.Studies.Imanishi2020.passive_satisfies_ron : Minimalism.voicePassive.assignsTheta = false

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.agentive_violates_ron : Minimalism.voiceAgent.assignsTheta = true

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

def Phenomena.Ergativity.Studies.Imanishi2020.ronCompatibleVoice (v : Minimalism.VoiceHead) : Bool

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

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.ronCompatibleVoice v = !v.assignsTheta

theorem Phenomena.Ergativity.Studies.Imanishi2020.passive_ron_compatible : ronCompatibleVoice Minimalism.voicePassive = true

theorem Phenomena.Ergativity.Studies.Imanishi2020.agentive_ron_incompatible : ronCompatibleVoice Minimalism.voiceAgent = false

theorem Phenomena.Ergativity.Studies.Imanishi2020.anticausative_ron_compatible : ronCompatibleVoice Minimalism.voiceAnticausative = true

theorem Phenomena.Ergativity.Studies.Imanishi2020.kaqchikel_perfective_bridge : Fragments.Mayan.Kaqchikel.KaqArgPosition.agent.case = Minimalism.CaseVal.erg ∧ Fragments.Mayan.Kaqchikel.KaqArgPosition.patient.case = Minimalism.CaseVal.abs ∧ Fragments.Mayan.Kaqchikel.KaqArgPosition.intranS.case = Minimalism.CaseVal.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 Phenomena.Ergativity.Studies.Imanishi2020.chol_perfective_bridge : Fragments.Mayan.Chol.ArgPosition.agent.ergCase = Minimalism.CaseVal.erg ∧ Fragments.Mayan.Chol.ArgPosition.patient.ergCase = Minimalism.CaseVal.abs ∧ Fragments.Mayan.Chol.ArgPosition.intranS.ergCase = Minimalism.CaseVal.abs

Chol's perfective alignment matches the same ergative pattern.

theorem Phenomena.Ergativity.Studies.Imanishi2020.qanjobal_perfective_bridge : Fragments.Mayan.Qanjobal.ArgPosition.agent.ergCase = Minimalism.CaseVal.erg ∧ Fragments.Mayan.Qanjobal.ArgPosition.patient.ergCase = Minimalism.CaseVal.abs ∧ Fragments.Mayan.Qanjobal.ArgPosition.intranS.ergCase = Minimalism.CaseVal.abs

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.shared_ergative : Fragments.Mayan.Kaqchikel.KaqArgPosition.agent.case = Fragments.Mayan.Chol.ArgPosition.agent.ergCase ∧ Fragments.Mayan.Chol.ArgPosition.agent.ergCase = Fragments.Mayan.Qanjobal.ArgPosition.agent.ergCase

All three languages share ergative alignment in the perfective.

def Phenomena.Ergativity.Studies.Imanishi2020.caseToMarker : Minimalism.CaseVal → 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

• Phenomena.Ergativity.Studies.Imanishi2020.caseToMarker Minimalism.CaseVal.erg = Fragments.Mayan.MarkerSet.setA
• Phenomena.Ergativity.Studies.Imanishi2020.caseToMarker Minimalism.CaseVal.gen = Fragments.Mayan.MarkerSet.setA
• Phenomena.Ergativity.Studies.Imanishi2020.caseToMarker Minimalism.CaseVal.abs = Fragments.Mayan.MarkerSet.setB
• Phenomena.Ergativity.Studies.Imanishi2020.caseToMarker x✝ = Fragments.Mayan.MarkerSet.setA

theorem Phenomena.Ergativity.Studies.Imanishi2020.erg_gen_homophonous : caseToMarker Minimalism.CaseVal.erg = caseToMarker Minimalism.CaseVal.gen

ERG/GEN homophony: both map to set A.

theorem Phenomena.Ergativity.Studies.Imanishi2020.chol_case_to_marker_bridge : caseToMarker Fragments.Mayan.Chol.ArgPosition.agent.accCase = cholPattern.sMarker ∧ caseToMarker Fragments.Mayan.Chol.ArgPosition.patient.accCase = cholPattern.oMarker

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.qanjobal_case_to_marker_bridge : caseToMarker Fragments.Mayan.Qanjobal.ArgPosition.agent.accCase = cholPattern.sMarker ∧ caseToMarker Fragments.Mayan.Qanjobal.ArgPosition.patient.accCase = cholPattern.oMarker

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.kaqchikel_case_to_marker_bridge : caseToMarker Fragments.Mayan.Kaqchikel.KaqArgPosition.agent.accCase = kaqchikelPattern.sMarker ∧ caseToMarker Fragments.Mayan.Kaqchikel.KaqArgPosition.patient.accCase = kaqchikelPattern.oMarker

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.acc_case_mirror : Fragments.Mayan.Kaqchikel.KaqArgPosition.agent.accCase = Fragments.Mayan.Chol.ArgPosition.patient.accCase ∧ Fragments.Mayan.Kaqchikel.KaqArgPosition.patient.accCase = Fragments.Mayan.Chol.ArgPosition.agent.accCase

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.end_to_end_all_languages : (caseToMarker Fragments.Mayan.Kaqchikel.KaqArgPosition.agent.accCase = (deriveAccPattern kaqchikelParams).sMarker ∧ caseToMarker Fragments.Mayan.Kaqchikel.KaqArgPosition.patient.accCase = (deriveAccPattern kaqchikelParams).oMarker) ∧ (caseToMarker Fragments.Mayan.Chol.ArgPosition.agent.accCase = (deriveAccPattern cholParams).sMarker ∧ caseToMarker Fragments.Mayan.Chol.ArgPosition.patient.accCase = (deriveAccPattern cholParams).oMarker) ∧ caseToMarker Fragments.Mayan.Qanjobal.ArgPosition.agent.accCase = (deriveAccPattern qanjobalParams).sMarker ∧ caseToMarker Fragments.Mayan.Qanjobal.ArgPosition.patient.accCase = (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 Phenomena.Ergativity.Studies.Imanishi2020.mayanSplit : Core.SplitErgativity Core.Aspect

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

Equations

• Phenomena.Ergativity.Studies.Imanishi2020.mayanSplit = { ergCondition := fun (a : Core.Aspect) => a == Core.Aspect.perfective }

theorem Phenomena.Ergativity.Studies.Imanishi2020.mayan_perfective_erg : mayanSplit.alignment Core.Aspect.perfective = Core.AlignmentFamily.ergative

theorem Phenomena.Ergativity.Studies.Imanishi2020.mayan_imperfective_acc : mayanSplit.alignment Core.Aspect.imperfective = Core.AlignmentFamily.accusative

theorem Phenomena.Ergativity.Studies.Imanishi2020.mayan_hindi_same_split : mayanSplit = Core.hindiSplit

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.cmp2014_ergativity_from_params (p : MayanParams) : CoonMateoPedroPreminger2014.hasSyntacticErgativity (Fragments.Mayan.toCaseLocus p.absPos) = (p.absPos == Fragments.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 Phenomena.Ergativity.Studies.Imanishi2020.kaqchikel_full_profile : deriveAccPattern kaqchikelParams = kaqchikelPattern ∧ CoonMateoPedroPreminger2014.hasSyntacticErgativity (Fragments.Mayan.toCaseLocus kaqchikelParams.absPos) = true

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

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

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

theorem Phenomena.Ergativity.Studies.Imanishi2020.qanjobal_cross_cutting : CoonMateoPedroPreminger2014.hasSyntacticErgativity (Fragments.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.