Imanishi (2014): Default Ergative

This file formalizes Chapter 3 of [Ima14], the explanation of the alignment puzzle in the nominative-accusative side of Mayan ergative splits: the non-perfective sentence of Kaqchikel and of Chol and Q'anjob'al is a non-verbal predicate embedding a nominalized clause, yet Kaqchikel aligns the transitive object with the ergative morpheme, (87), where Chol and Q'anjob'al align every subject with it, (88). The Unaccusative Requirement on Nominalization (90), that nominalized verbs lack an external argument, is parameterized (URN); phase head ergative Case goes to the highest Case-less DP of the nominalized clause when it is spelled out, absolutive to the matrix-generated subject from Infl and to the object from a nominalized verb able to assign it (Nominalization, caseOf). Where the requirement holds the subject is base-generated in the matrix and the object, left Case-less by the intransitivized verb, is the highest Case-less DP; where it need not apply the subject stays inside and is that DP, (141). The two alignments of the summary (178) are the outputs (caseOf_kaqchikel, caseOf_chol, caseOf_qanjobal), they are the library's Alignment.invertedErgative and Alignment.extendedErgative, and the typological gaps (179) and (180), an all-absolutive and an all-ergative alignment, are underivable (not_all_abs, not_all_erg).

Implementation notes

• S is treated with A, as in the paper's tables; the internal argument of an unaccusative is not modelled separately. Ergative from the phase head D is Case.gen, as in the library's alignments, ERG and GEN being homophonous in Mayan.
• A nominalized verb assigns absolutive to its object when the requirement does not apply and either Voice of a low absolutive language or the special suffix of Q'anjob'al, Chuj and Jakaltek supplies the Case (Section 3.4.3); a high absolutive language without the suffix leaves the object Case-less. Mam's double ergative (181)–(183) and the transitive embedding verb chäp 'begin' of (94) are outside the model.

References

• [Ima14]
• [CMPP14]

inductive Imanishi2014.URN : Type

The Unaccusative Requirement on Nominalization, (90): whether nominalized verbs must lack an external argument, as in Kaqchikel, or need not, as in Chol and Q'anjob'al, (141).

• required : URN
• optional : URN

@[instance_reducible]

instance Imanishi2014.instDecidableEqURN : DecidableEq URN

Equations

• Imanishi2014.instDecidableEqURN x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Imanishi2014.Nominalization : Type

A language's nominalization on the accusative side of its split: the requirement, the locus of absolutive Case (Mayan.ABSPosition, the Mayan Absolutive Parameter of [CMPP14]), and whether the nominalized verb carries the suffix that lets a high absolutive language assign absolutive to its object (Section 3.4.3).

• urn : URN
• absPos : Mayan.ABSPosition
• suffix : Prop
• decSuffix : Decidable self.suffix

def Imanishi2014.Nominalization.VerbAssignsAbs (L : Nominalization) : Prop

The nominalized verb assigns absolutive Case to its object: the requirement does not intransitivize it, and either Voice of a low absolutive language or the suffix provides the Case.

Equations

• L.VerbAssignsAbs = (L.urn = Imanishi2014.URN.optional ∧ (L.absPos = Mayan.ABSPosition.low ∨ L.suffix))

@[instance_reducible]

instance Imanishi2014.Nominalization.instDecidableVerbAssignsAbs (L : Nominalization) : Decidable L.VerbAssignsAbs

Equations

• L.instDecidableVerbAssignsAbs = id inferInstance

def Imanishi2014.Nominalization.caseless (L : Nominalization) : List ArgumentRole

The Case-less DPs of the transitive nominalized clause, highest first: the external argument when the requirement lets it stay inside, and the object unless the verb assigns it Case.

Equations

• L.caseless = (if L.urn = Imanishi2014.URN.optional then [ArgumentRole.A] else []) ++ if L.VerbAssignsAbs then [] else [ArgumentRole.P]

def Imanishi2014.Nominalization.phaseHead (L : Nominalization) (r : ArgumentRole) : Option Case

Phase head ergative Case: the highest Case-less DP receives ergative from D when the nominalized clause is spelled out (Section 3.3).

Equations

• L.phaseHead r = if L.caseless.head? = some r then some Case.gen else none

def Imanishi2014.Nominalization.caseOf (L : Nominalization) : ArgumentRole → Option Case

The Case of each core argument on the accusative side: a subject base-generated in the matrix under the requirement receives absolutive from Infl, an object from a nominalized verb able to assign it, and otherwise phase head ergative Case or nothing.

Equations

• L.caseOf ArgumentRole.A = if L.urn = Imanishi2014.URN.required then some Case.abs else L.phaseHead ArgumentRole.A
• L.caseOf ArgumentRole.S = if L.urn = Imanishi2014.URN.required then some Case.abs else L.phaseHead ArgumentRole.A
• L.caseOf ArgumentRole.P = if L.VerbAssignsAbs then some Case.abs else L.phaseHead ArgumentRole.P
• L.caseOf ArgumentRole.R = none
• L.caseOf ArgumentRole.T = none

def Imanishi2014.Nominalization.kaqchikel : Nominalization

Kaqchikel: the requirement holds, high absolutive as its verbal complex has it, no suffix.

Equations

• Imanishi2014.Nominalization.kaqchikel = { urn := Imanishi2014.URN.required, absPos := Mayan.absPosition Kaqchikel.template, suffix := False, decSuffix := instDecidableFalse }

def Imanishi2014.Nominalization.chol : Nominalization

Chol: the requirement need not apply, low absolutive.

Equations

• Imanishi2014.Nominalization.chol = { urn := Imanishi2014.URN.optional, absPos := Mayan.absPosition Chol.template, suffix := False, decSuffix := instDecidableFalse }

def Imanishi2014.Nominalization.qanjobal : Nominalization

Q'anjob'al: the requirement need not apply, high absolutive, the suffix -on supplying object Case.

Equations

• Imanishi2014.Nominalization.qanjobal = { urn := Imanishi2014.URN.optional, absPos := Mayan.absPosition Qanjobal.template, suffix := True, decSuffix := instDecidableTrue }

def Imanishi2014.Nominalization.tojolabal : Nominalization

Tojolabal, (178): low absolutive but subject to the requirement, so Kaqchikel-type.

Equations

• Imanishi2014.Nominalization.tojolabal = { urn := Imanishi2014.URN.required, absPos := Mayan.ABSPosition.low, suffix := False, decSuffix := instDecidableFalse }

theorem Imanishi2014.Nominalization.caseOf_kaqchikel (r : ArgumentRole) : r ∈ [ArgumentRole.A, ArgumentRole.S, ArgumentRole.P] → kaqchikel.caseOf r = some (Alignment.invertedErgative r)

Kaqchikel's accusative side is the library's inverted ergative alignment, (87): subjects absolutive, the object ergative.

theorem Imanishi2014.Nominalization.caseOf_chol (r : ArgumentRole) : r ∈ [ArgumentRole.A, ArgumentRole.S, ArgumentRole.P] → chol.caseOf r = some (Alignment.extendedErgative r)

Chol's accusative side is the extended ergative alignment, (88).

theorem Imanishi2014.Nominalization.caseOf_qanjobal (r : ArgumentRole) : r ∈ [ArgumentRole.A, ArgumentRole.S, ArgumentRole.P] → qanjobal.caseOf r = some (Alignment.extendedErgative r)

Q'anjob'al's accusative side is the extended ergative alignment, its object Case coming from the suffix rather than from Voice.

theorem Imanishi2014.Nominalization.caseOf_tojolabal (r : ArgumentRole) : r ∈ [ArgumentRole.A, ArgumentRole.S, ArgumentRole.P] → tojolabal.caseOf r = some (Alignment.invertedErgative r)

Tojolabal patterns with Kaqchikel: the requirement, not the absolutive parameter, decides the type, (178).

theorem Imanishi2014.Nominalization.caseKaqchikel_prog (r : ArgumentRole) (h : r ∈ [ArgumentRole.A, ArgumentRole.S, ArgumentRole.P]) : kaqchikel.caseOf r = some (Kaqchikel.assignCase UD.Aspect.Prog r)

The fragment's progressive entries are the mechanism's outputs.

theorem Imanishi2014.Nominalization.caseOf_A_eq_abs_iff (L : Nominalization) : L.caseOf ArgumentRole.A = some Case.abs ↔ L.urn = URN.required

(178): the subject is absolutive exactly when the requirement holds.

theorem Imanishi2014.Nominalization.caseOf_P_eq_gen_iff (L : Nominalization) : L.caseOf ArgumentRole.P = some Case.gen ↔ L.urn = URN.required

(178): the object is ergative exactly when the requirement holds.

theorem Imanishi2014.Nominalization.caseOf_P_eq_none_iff (L : Nominalization) : L.caseOf ArgumentRole.P = none ↔ L.urn = URN.optional ∧ L.absPos = Mayan.ABSPosition.high ∧ ¬L.suffix

Without the requirement the object needs a Case assigner: a high absolutive language lacking the suffix leaves it Case-less.

theorem Imanishi2014.Nominalization.not_all_abs (L : Nominalization) : ¬(L.caseOf ArgumentRole.A = some Case.abs ∧ L.caseOf ArgumentRole.P = some Case.abs)

(179): no language aligns both the subject and the object with the absolutive. An absolutive subject means the requirement holds, so the nominalized verb is intransitivized and cannot assign the object Case.

theorem Imanishi2014.Nominalization.not_all_erg (L : Nominalization) : ¬(L.caseOf ArgumentRole.A = some Case.gen ∧ L.caseOf ArgumentRole.P = some Case.gen)

(180): no language aligns both with the ergative. An ergative subject sits inside the nominalized clause as its highest Case-less DP, so the object is not the highest.