Imanishi (2020): Parameterizing Split Ergativity in Mayan

This file formalizes [Ima20], the journal account of the alignment puzzle of [Ima14]: the non-perfective clause of Kaqchikel, Chol and Q'anjob'al is an aspectual predicate embedding a nominalized clause, yet Kaqchikel cross-references the subject with the set B marker and the transitive object with set A, (4), where Chol and Q'anjob'al do the reverse, (5). The Restriction on Nominalization (63), that nominalized verbs lack a syntactically projected external argument, is the dissertation's requirement (Imanishi2014.URN) restated as a selectional property of the nominalizing head. Under it a transitive base must be independently intransitivized, by passivization, antipassivization or (pseudo) noun incorporation (Strategy), and the subject is base-generated as the argument of the matrix predicate (Matrix): absolutive from Infl under the intransitive ajin, inherent ergative from transitive v under chäp 'begin'. A Clause records these choices, and Clause.subject and Clause.object say what licenses each argument (Licensing): genitive from the D of the nominalized clause goes to its highest Case-less DP, absolutive to the object from Voice or from the Q'anjob'al suffix -on. Clause.WellFormed collects the conditions the derivations rely on, among them the semantic control of the matrix subject into an external θ-role of the base, which excludes unaccusative and passive bases under ajin, (92) and (94). The summary (117) is subjectMarker_setB_iff and objectMarker_setA_iff, and case_eq_caseOf shows that the progressive derivations assign the dissertation's Cases.

Implementation notes

• That nominalized verbs of Kaqchikel must be intransitivized is not derived from the restriction, as the paper conjectures it may be; it is a clause of WellFormed.
• The closing generalization, that the restriction fails exactly when the verbal domain of the nominalized clause has a structural Case assigner, is not stated: in the dissertation's survey Tojolabal is low absolutive yet subject to the requirement, so the criterion cannot be read off Mayan.ABSPosition.
• The Case-licensing of the relational noun by the preposition chi, (87) and (88), and the third person set B marker for the nominalized clause on the aspectual predicate are outside the model.

References

• [Ima20]
• [Ima14]
• [CMPP14]
• [Ale01]

inductive Imanishi2020.Base : Type

The base verb of a nominalization, by the arguments it projects.

• transitive : Base
• unergative : Base
• unaccusative : Base
• passive : Base

@[instance_reducible]

instance Imanishi2020.instDecidableEqBase : DecidableEq Base

Equations

• Imanishi2020.instDecidableEqBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Imanishi2020.Base.HasExternal (b : Base) : Prop

The base has an external θ-role for the matrix subject to control into (Section 3.2.2); a passive base has it suppressed.

Equations

• b.HasExternal = (b = Imanishi2020.Base.transitive ∨ b = Imanishi2020.Base.unergative)

inductive Imanishi2020.Strategy : Type

How a transitive base is intransitivized under the restriction (Sections 3.2.1 and 3.3): passivization leaves the object as the only DP of the nominalized clause, antipassivization demotes it to an oblique under a relational noun, and (pseudo) noun incorporation Case-licenses it under adjacency.

• passive : Strategy
• antipassive : Strategy
• incorporation : Strategy

@[instance_reducible]

instance Imanishi2020.instDecidableEqStrategy : DecidableEq Strategy

Equations

• Imanishi2020.instDecidableEqStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Imanishi2020.Matrix : Type

The predicate embedding the nominalized clause: the intransitive aspectual predicate ajin of the Kaqchikel progressive, whose subject sits in its specifier, the transitive verb chäp 'begin', or an aspectual predicate such as Chol choñkol and Q'anjob'al lanan that takes the nominalized clause as its sole argument.

• ajin : Matrix
• chap : Matrix
• aspectual : Matrix

@[instance_reducible]

instance Imanishi2020.instDecidableEqMatrix : DecidableEq Matrix

Equations

• Imanishi2020.instDecidableEqMatrix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Imanishi2020.Licensing : Type

What licenses an argument of the nominalized verb: genitive from the D of the nominalized clause, absolutive from Voice or the suffix inside it, absolutive from the matrix Infl, inherent ergative from the transitive matrix v, genitive from a relational noun, or (pseudo) noun incorporation.

• gen : Licensing
• absVoice : Licensing
• absInfl : Licensing
• ergV : Licensing
• oblique : Licensing
• incorporated : Licensing

@[instance_reducible]

instance Imanishi2020.instDecidableEqLicensing : DecidableEq Licensing

Equations

• Imanishi2020.instDecidableEqLicensing x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Imanishi2020.Licensing.case : Licensing → Option Case

The Case an argument receives, if any.

Equations

• Imanishi2020.Licensing.gen.case = some Case.gen
• Imanishi2020.Licensing.oblique.case = some Case.gen
• Imanishi2020.Licensing.absVoice.case = some Case.abs
• Imanishi2020.Licensing.absInfl.case = some Case.abs
• Imanishi2020.Licensing.ergV.case = some Case.erg
• Imanishi2020.Licensing.incorporated.case = none

def Imanishi2020.Licensing.marker : Licensing → Option Mayan.MarkerSet

The agreement set cross-referencing the argument on the verbal complex, ergative and genitive both spelled out as set A. An oblique is cross-referenced on its relational noun and an incorporated object not at all.

Equations

• Imanishi2020.Licensing.gen.marker = some Mayan.MarkerSet.setA
• Imanishi2020.Licensing.ergV.marker = some Mayan.MarkerSet.setA
• Imanishi2020.Licensing.absVoice.marker = some Mayan.MarkerSet.setB
• Imanishi2020.Licensing.absInfl.marker = some Mayan.MarkerSet.setB
• Imanishi2020.Licensing.oblique.marker = none
• Imanishi2020.Licensing.incorporated.marker = none

structure Imanishi2020.Clause : Type

A nominalized clause: the language's nominalization parameters, the base verb, the intransitivizing strategy if any, and the embedding predicate, none for a nominalized clause in argument position, (64)–(71).

• lang : Imanishi2014.Nominalization
• base : Base
• strategy : Option Strategy
• matrix : Option Matrix

def Imanishi2020.Clause.Restricted (c : Clause) : Prop

The restriction bans the base's external argument from the nominalized clause.

Equations

• c.Restricted = (c.lang.urn = Imanishi2014.URN.required ∧ c.base.HasExternal)

@[instance_reducible]

instance Imanishi2020.Clause.instDecidableRestricted (c : Clause) : Decidable c.Restricted

Equations

• c.instDecidableRestricted = id (id inferInstance)

def Imanishi2020.Clause.subject (c : Clause) : Option Licensing

Licensing of the subject, the external argument or the internal argument of an unaccusative or passive base. Under the restriction it is base-generated as the argument of the matrix predicate and licensed there; otherwise it is the highest DP of the nominalized clause and receives genitive from D.

Equations

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

def Imanishi2020.Clause.object (c : Clause) : Option Licensing

Licensing of the object of a transitive base: by the intransitivizing strategy under the restriction, and otherwise by the Case assigner in the verbal domain of the nominalized clause, Voice of a low absolutive language or the suffix, if there is one.

Equations

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

def Imanishi2020.Clause.subjectMarker (c : Clause) : Option Mayan.MarkerSet

The agreement set cross-referencing the subject.

Equations

• c.subjectMarker = c.subject.bind Imanishi2020.Licensing.marker

def Imanishi2020.Clause.objectMarker (c : Clause) : Option Mayan.MarkerSet

The agreement set cross-referencing the object.

Equations

• c.objectMarker = c.object.bind Imanishi2020.Licensing.marker

def Imanishi2020.Clause.WellFormed (c : Clause) : Prop

The conditions the derivations rely on: a transitive base is intransitivized exactly under the restriction (Section 3.1), the subject of ajin and chäp semantically controls an external θ-role of the base (Section 3.2.2), an embedded clause licenses its subject, and a transitive object is licensed.

Equations

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

@[instance_reducible]

instance Imanishi2020.Clause.instDecidableWellFormed (c : Clause) : Decidable c.WellFormed

Equations

• c.instDecidableWellFormed = id (id inferInstance)

def Imanishi2020.Clause.kaqchikelProgressive : Clause

The Kaqchikel progressive of a transitive, (85): a passive nominalization under ajin.

Equations

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

def Imanishi2020.Clause.kaqchikelUnergative : Clause

The Kaqchikel progressive of an unergative, (91).

Equations

• Imanishi2020.Clause.kaqchikelUnergative = { lang := Imanishi2014.Nominalization.kaqchikel, base := Imanishi2020.Base.unergative, strategy := none, matrix := some Imanishi2020.Matrix.ajin }

def Imanishi2020.Clause.kaqchikelUnaccusative : Clause

The Kaqchikel progressive of an unaccusative, (92).

Equations

• Imanishi2020.Clause.kaqchikelUnaccusative = { lang := Imanishi2014.Nominalization.kaqchikel, base := Imanishi2020.Base.unaccusative, strategy := none, matrix := some Imanishi2020.Matrix.ajin }

def Imanishi2020.Clause.kaqchikelPassive : Clause

The Kaqchikel progressive of a passive verb, (94).

Equations

• Imanishi2020.Clause.kaqchikelPassive = { lang := Imanishi2014.Nominalization.kaqchikel, base := Imanishi2020.Base.passive, strategy := none, matrix := some Imanishi2020.Matrix.ajin }

def Imanishi2020.Clause.kaqchikelSubjectNominal : Clause

A nominalized unaccusative in subject position, (69).

Equations

• Imanishi2020.Clause.kaqchikelSubjectNominal = { lang := Imanishi2014.Nominalization.kaqchikel, base := Imanishi2020.Base.unaccusative, strategy := none, matrix := none }

def Imanishi2020.Clause.kaqchikelBegin : Clause

A passive nominalization under chäp 'begin', (98).

Equations

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

def Imanishi2020.Clause.kaqchikelAntipassive : Clause

An antipassive nominalization under chäp, (100).

Equations

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

def Imanishi2020.Clause.kaqchikelIncorporation : Clause

The incorporating -oj nominalization under ajin, (102).

Equations

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

def Imanishi2020.Clause.cholProgressive : Clause

The Chol progressive of a transitive, (60a).

Equations

• Imanishi2020.Clause.cholProgressive = { lang := Imanishi2014.Nominalization.chol, base := Imanishi2020.Base.transitive, strategy := none, matrix := some Imanishi2020.Matrix.aspectual }

def Imanishi2020.Clause.cholIntransitive : Clause

The Chol progressive of an intransitive, (60b).

Equations

• Imanishi2020.Clause.cholIntransitive = { lang := Imanishi2014.Nominalization.chol, base := Imanishi2020.Base.unaccusative, strategy := none, matrix := some Imanishi2020.Matrix.aspectual }

def Imanishi2020.Clause.qanjobalProgressive : Clause

The Q'anjob'al progressive of a transitive, (73a), the object licensed by -on.

Equations

• Imanishi2020.Clause.qanjobalProgressive = { lang := Imanishi2014.Nominalization.qanjobal, base := Imanishi2020.Base.transitive, strategy := none, matrix := some Imanishi2020.Matrix.aspectual }

theorem Imanishi2020.Clause.kaqchikelProgressive_markers : kaqchikelProgressive.WellFormed ∧ kaqchikelProgressive.subjectMarker = some Mayan.MarkerSet.setB ∧ kaqchikelProgressive.objectMarker = some Mayan.MarkerSet.setA

The Kaqchikel-type alignment (4): set B on the subject, set A on the object, from a passive nominalization whose subject is the argument of ajin.

theorem Imanishi2020.Clause.kaqchikelUnergative_markers : kaqchikelUnergative.WellFormed ∧ kaqchikelUnergative.subjectMarker = some Mayan.MarkerSet.setB ∧ kaqchikelUnergative.objectMarker = none

The unergative progressive, (91): set B on the subject, no genitive assigned inside.

theorem Imanishi2020.Clause.not_wellFormed_unaccusative_passive : ¬kaqchikelUnaccusative.WellFormed ∧ ¬kaqchikelPassive.WellFormed

Unaccusative and passive bases cannot be embedded under ajin, (92) and (94): there is no external θ-role for its subject to control.

theorem Imanishi2020.Clause.kaqchikelSubjectNominal_subject : kaqchikelSubjectNominal.WellFormed ∧ kaqchikelSubjectNominal.subject = some Licensing.gen

In argument position the same unaccusative nominalizes, (69), its internal argument taking genitive from D.

theorem Imanishi2020.Clause.kaqchikelBegin_markers : kaqchikelBegin.WellFormed ∧ kaqchikelBegin.subjectMarker = some Mayan.MarkerSet.setA ∧ kaqchikelBegin.objectMarker = some Mayan.MarkerSet.setA

Under chäp, (98), the subject takes inherent ergative from the transitive matrix v, so subject and object alike are cross-referenced by set A.

theorem Imanishi2020.Clause.no_gen_antipassive_incorporation : kaqchikelAntipassive.WellFormed ∧ kaqchikelAntipassive.objectMarker = none ∧ kaqchikelIncorporation.WellFormed ∧ kaqchikelIncorporation.objectMarker = none

Antipassive and incorporating nominalizations, (100) and (102), leave no DP for D to license, so no set A marker appears on the nominalized verb, (104).

theorem Imanishi2020.Clause.chol_qanjobal_markers : cholProgressive.WellFormed ∧ cholProgressive.subjectMarker = some Mayan.MarkerSet.setA ∧ cholProgressive.objectMarker = some Mayan.MarkerSet.setB ∧ cholIntransitive.WellFormed ∧ cholIntransitive.subjectMarker = some Mayan.MarkerSet.setA ∧ qanjobalProgressive.WellFormed ∧ qanjobalProgressive.subjectMarker = some Mayan.MarkerSet.setA ∧ qanjobalProgressive.objectMarker = some Mayan.MarkerSet.setB

The Chol/Q'anjob'al-type alignment (5): the subject, the highest DP of the nominalized clause, takes genitive from D, and the object absolutive from Voice or the suffix.

theorem Imanishi2020.Clause.subject_ne_gen (c : Clause) (h : c.Restricted) : c.subject ≠ some Licensing.gen

The external argument never takes genitive from D under the restriction, (66) and (68).

theorem Imanishi2020.Clause.absPos_low_or_suffix_of_object (c : Clause) (h : c.object = some Licensing.absVoice) : c.lang.absPos = Mayan.ABSPosition.low ∨ c.lang.suffix

The non-finiteness diagnostic of (59) and (60): a set B marker inside the nominalized clause needs a Case assigner in its verbal domain, so it survives only in a low absolutive language or with the suffix.

theorem Imanishi2020.Clause.subjectMarker_setB_iff (c : Clause) (h : c.WellFormed) (hb : c.base.HasExternal) (hm : c.matrix = some Matrix.ajin ∨ c.matrix = some Matrix.aspectual) : c.subjectMarker = some Mayan.MarkerSet.setB ↔ c.lang.urn = Imanishi2014.URN.required

(117): under a progressive predicate the subject is cross-referenced by set B exactly when the restriction holds.

theorem Imanishi2020.Clause.objectMarker_setA_iff (c : Clause) (h : c.WellFormed) (ht : c.base = Base.transitive) (ha : c.strategy ≠ some Strategy.antipassive) (hi : c.strategy ≠ some Strategy.incorporation) : c.objectMarker = some Mayan.MarkerSet.setA ↔ c.lang.urn = Imanishi2014.URN.required

(117): the object of a passive nominalization or of an unrestricted transitive is cross-referenced by set A exactly when the restriction holds.

theorem Imanishi2020.Clause.case_eq_caseOf (c : Clause) (h : c.WellFormed) (ht : c.base = Base.transitive) (hm : c.matrix = some Matrix.ajin ∨ c.matrix = some Matrix.aspectual) (ha : c.strategy ≠ some Strategy.antipassive) (hi : c.strategy ≠ some Strategy.incorporation) : c.subject.bind Licensing.case = c.lang.caseOf ArgumentRole.A ∧ c.object.bind Licensing.case = c.lang.caseOf ArgumentRole.P

The progressive derivations assign the dissertation's Cases: absolutive to the subject and genitive to the object under the restriction, and the reverse without it.