Coon, Mateo Pedro and Preminger (2014): The role of Case in A-bar extraction asymmetries

Many Mayan languages cannot extract the subject of a regular transitive clause and use the Agent Focus form of the verb instead. Coon, Mateo Pedro and Preminger trace this syntactic ergativity to the Case of the object rather than to the ergative subject. Following Legate and Aldridge, every Mayan language licenses the transitive subject low, from v, but the object is licensed either by Infl, where the absolutive marker sits high on the aspect marker, or by v, where it sits low on the stem. A transitive verb phrase is a phase with a single escape hatch that contains the subject, so an object that must reach Infl takes the hatch and traps the subject, which is Tada's generalization, and in a non-finite clause, which lacks Infl, it has no Case at all. The Q'anjob'al Agent Focus suffix -on is a marked Voice that cases the object itself, so no ergative is assigned and v is intransitive, non-phasal and spelled out by the intransitive status suffix; it frees the subject, licenses non-finite transitives (the Crazy Antipassive), and as a last resort fails with reflexive and bare objects, which need no Case and let the subject of a regular transitive extract.

Main statements

• tada: a registered language marks the extraction of a core argument from a finite transitive exactly when the regular derivation fails, which for the subject is when the absolutive is high.
• converges_iff_verbForm: in Q'anjob'al the derivation that converges uses the verb form the fragment records, Agent Focus in every non-finite transitive and under extraction of a third-person subject.
• formallyTransitive_iff_hasSetA, formallyTransitive_iff_statusSuffix: Agent Focus selects intransitive v, so it has no Set A and takes the intransitive status suffix.
• analysed_rows: every analysed example is grammatical exactly when its clause converges.

Implementation notes

• The paper's v sits above the substrate's Voice head and is formally transitive when Voice would head a phase by Chomsky's criterion and leaves the object's Case to Infl or v; phasehood, Set A and the status suffix are read off that one property.
• Trapping builds in the subject's position inside the phase and the single escape hatch, as the paper assumes them.
• The last resort is the paper's later formulation, that the Case-checking Voice merges only where the regular derivation would leave the object without Case or trap the extracting subject.
• Rows carry the paper's high or low classification of their language, checked against the fragment's verbal template; Kaqchikel Agent Focus and the nominal-stem and passive strategies for non-finite transitives are recorded as rows without a configuration.

TODO

• The person restriction on Agent Focus (72), which the paper tentatively derives by base-generating first- and second-person agents high, is not modelled, so converges_iff_verbForm is stated for third-person agents.
• Agent Focus with reflexive objects in non-finite clauses, which the paper's fn. 31 records and leaves unexplained, does not converge here either.
• Trapping could be derived from SyntacticObject.phaseEdge on the tree (55) once the substrate bounds the number of specifiers at a phase edge.
• The extraction of low adverbs and the instrumental voice (§5.3) are not modelled.

References

• J. Coon, P. Mateo Pedro and O. Preminger, The role of Case in A-bar extraction asymmetries: Evidence from Mayan (2014)
• J. A. Legate, Morphological and abstract case (2008)
• E. Aldridge, Ergativity and word order in Austronesian languages (2004)
• H. Tada, A/A-bar partition in derivation (1993)
• N. Chomsky, Derivation by Phase (2001)
• H. Harley, External arguments and the Mirror Principle: On the distinctness of Voice and v (2013)
• F. Ordóñez, The antipassive in Jacaltec: A last resort strategy (1995)
• D. Massam, Pseudo noun incorporation in Niuean (2001)
• L. Hou, Agent focus in Chuj reflexive constructions (2013)

Clauses

inductive CoonMateoPedroPreminger2014.Licenser : Type

The heads that assign structural Case (5).

• infl : Licenser
• v : Licenser

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqLicenser : DecidableEq Licenser

Equations

• CoonMateoPedroPreminger2014.instDecidableEqLicenser x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instReprLicenser : Repr Licenser

Equations

• CoonMateoPedroPreminger2014.instReprLicenser = { reprPrec := CoonMateoPedroPreminger2014.instReprLicenser.repr }

def CoonMateoPedroPreminger2014.instReprLicenser.repr : Licenser → ℕ → Std.Format

Equations

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

def CoonMateoPedroPreminger2014.Licenser.ofPosition : Mayan.ABSPosition → Licenser

The head licensing transitive objects is read off the absolutive's position (24): Infl when the absolutive is high, so that it is nominative ([Leg08]'s ABS=NOM), and v when it is low, so that it is a default (ABS=DEF).

Equations

• CoonMateoPedroPreminger2014.Licenser.ofPosition Mayan.ABSPosition.high = CoonMateoPedroPreminger2014.Licenser.infl
• CoonMateoPedroPreminger2014.Licenser.ofPosition Mayan.ABSPosition.low = CoonMateoPedroPreminger2014.Licenser.v

inductive CoonMateoPedroPreminger2014.Object : Type

What a transitive verb takes as its object.

• dp : Object

  A full DP, which needs structural Case and satisfies the EPP of v.

• caseless : Object

  A reflexive, extended reflexive or bare NP, pseudo-incorporated ([Mas01]) and needing neither (§5.2).

• oblique : Object

  An object licensed inside its own oblique phrase, the demoted patient of an antipassive (59) or the relational-noun complement of a Mam infinitive (39a).

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqObject : DecidableEq Object

Equations

• CoonMateoPedroPreminger2014.instDecidableEqObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instReprObject : Repr Object

Equations

• CoonMateoPedroPreminger2014.instReprObject = { reprPrec := CoonMateoPedroPreminger2014.instReprObject.repr }

def CoonMateoPedroPreminger2014.instReprObject.repr : Object → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instFintypeObject : Fintype Object

Equations

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

def CoonMateoPedroPreminger2014.voiceAF : Minimalist.Voice.Head

Agent Focus as the marked Voice (66), agentive Voice that also assigns structural Case to the object.

Equations

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

inductive CoonMateoPedroPreminger2014.Predicate : Type

The verb phrase of a clause, an intransitive with the marker series of its sole argument or a transitive with its Voice and its object.

• intransitive (marking : Mayan.MarkerSet) : Predicate
• transitive (voice : Minimalist.Voice.Head) (object : Object) : Predicate

def CoonMateoPedroPreminger2014.instDecidableEqPredicate.decEq (x✝ x✝¹ : Predicate) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqPredicate : DecidableEq Predicate

Equations

• CoonMateoPedroPreminger2014.instDecidableEqPredicate = CoonMateoPedroPreminger2014.instDecidableEqPredicate.decEq

structure CoonMateoPedroPreminger2014.Clause : Type

A clause, with the head licensing its object, its finiteness, its verb phrase, the argument extracted and whether an adverb separates the verb from its object.

• licenser : Licenser

  The head licensing transitive objects.

• finite : Bool

  Whether the clause has finite Infl, the preverbal aspect marker.

• predicate : Predicate

  The verb phrase.

• extracted : Option ArgumentRole

  The argument A-bar extracted, if any.

• separated : Bool

  Whether adverbial material separates the verb from its object (81).

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqClause : DecidableEq Clause

Equations

• CoonMateoPedroPreminger2014.instDecidableEqClause = CoonMateoPedroPreminger2014.instDecidableEqClause.decEq

def CoonMateoPedroPreminger2014.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

def CoonMateoPedroPreminger2014.Predicate.voice? : Predicate → Option Minimalist.Voice.Head

The Voice head of a transitive verb phrase.

Equations

• (CoonMateoPedroPreminger2014.Predicate.transitive v object).voice? = some v
• (CoonMateoPedroPreminger2014.Predicate.intransitive marking).voice? = none

def CoonMateoPedroPreminger2014.Predicate.object? : Predicate → Option Object

The object of a transitive verb phrase.

Equations

• (CoonMateoPedroPreminger2014.Predicate.transitive v object).object? = some object
• (CoonMateoPedroPreminger2014.Predicate.intransitive marking).object? = none

def CoonMateoPedroPreminger2014.Predicate.marking? : Predicate → Option Mayan.MarkerSet

The marker series of an intransitive subject.

Equations

• (CoonMateoPedroPreminger2014.Predicate.intransitive m).marking? = some m
• (CoonMateoPedroPreminger2014.Predicate.transitive voice object).marking? = none

def CoonMateoPedroPreminger2014.Predicate.regular : Predicate → Predicate

The same verb phrase under regular transitive Voice, the derivation Agent Focus competes with.

Equations

• (CoonMateoPedroPreminger2014.Predicate.transitive voice o).regular = CoonMateoPedroPreminger2014.Predicate.transitive Minimalist.Voice.agentive o
• x✝.regular = x✝

def CoonMateoPedroPreminger2014.Predicate.FormallyTransitive (p : Predicate) : Prop

The verb phrase has formally transitive v, the phase head above Voice that assigns ergative to the subject and is spelled out by the status suffix ((55), [Har13b]). It is selected by a Voice head that would head a phase by [Cho01]'s criterion, unless that head cases the object itself and so leaves no ergative to assign (§4.2).

Equations

• p.FormallyTransitive = ∃ v ∈ p.voice?, v.IsPhasal ∧ ¬v.ChecksCase

def CoonMateoPedroPreminger2014.Predicate.ChecksCase (p : Predicate) : Prop

The Voice checks the object's Case, as Agent Focus does.

Equations

• p.ChecksCase = ∃ v ∈ p.voice?, v.ChecksCase

def CoonMateoPedroPreminger2014.Predicate.Raises (p : Predicate) (l : Licenser) : Prop

The object raises to the edge of the verb phrase: Case is assigned within the phase and Infl sits outside it, so a full DP object licensed by Infl must reach the edge (51), which the EPP of eventive v keeps true under Agent Focus (66); an object licensed by v stays in situ (52).

Equations

• p.Raises l = (p.object? = some CoonMateoPedroPreminger2014.Object.dp ∧ l = CoonMateoPedroPreminger2014.Licenser.infl)

def CoonMateoPedroPreminger2014.Predicate.ObjectLicensed (p : Predicate) (l : Licenser) (finite : Bool) : Prop

The object's Case is available (27): Voice checks it, v assigns it, or finite Infl does; a caseless or oblique object needs none. The low-abs non-finite cell takes the embedded clause to contain v, which the paper's fn. 12 leaves open.

Equations

• p.ObjectLicensed l finite = (p.object? = some CoonMateoPedroPreminger2014.Object.dp → p.ChecksCase ∨ l = CoonMateoPedroPreminger2014.Licenser.v ∨ finite = true)

def CoonMateoPedroPreminger2014.Predicate.SubjectLicensed (p : Predicate) (finite : Bool) : Prop

The absolutive on an intransitive subject needs finite Infl ((32), (33)); the ergative/possessive marking of a non-finite one is the nominalization's.

Equations

• p.SubjectLicensed finite = (p.marking? = some Mayan.MarkerSet.setB → finite = true)

def CoonMateoPedroPreminger2014.Predicate.Adjacent (p : Predicate) (separated : Bool) : Prop

A pseudo-incorporated object stays adjacent to the verb, the Chuj contrast (81) of [Hou13]; the paper's fn. 28 notes that the word-order reflex does not hold of Q'anjob'al extended reflexives.

Equations

• p.Adjacent separated = (p.object? = some CoonMateoPedroPreminger2014.Object.caseless → separated = false)

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Predicate.instDecidablePredFormallyTransitive : DecidablePred FormallyTransitive

Equations

• p.instDecidablePredFormallyTransitive = CoonMateoPedroPreminger2014.Predicate.instDecidablePredFormallyTransitive._aux_1 p

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Predicate.instDecidablePredChecksCase : DecidablePred ChecksCase

Equations

• p.instDecidablePredChecksCase = CoonMateoPedroPreminger2014.Predicate.instDecidablePredChecksCase._aux_1 p

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Predicate.instDecidableRaises (p : Predicate) (l : Licenser) : Decidable (p.Raises l)

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Predicate.instDecidableObjectLicensed (p : Predicate) (l : Licenser) (b : Bool) : Decidable (p.ObjectLicensed l b)

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Predicate.instDecidableSubjectLicensed (p : Predicate) (b : Bool) : Decidable (p.SubjectLicensed b)

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Predicate.instDecidableAdjacent (p : Predicate) (b : Bool) : Decidable (p.Adjacent b)

Equations

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

Trapping

def CoonMateoPedroPreminger2014.Trapped (c : Clause) : Prop

The subject is trapped (53): the raised object takes the single escape hatch of the phasal verb phrase, inside which the subject is generated, the three factors of (89).

Equations

• CoonMateoPedroPreminger2014.Trapped c = (c.predicate.FormallyTransitive ∧ c.predicate.Raises c.licenser)

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidablePredClauseTrapped : DecidablePred Trapped

Equations

• CoonMateoPedroPreminger2014.instDecidablePredClauseTrapped x✝ = { decide := decide x✝.predicate.FormallyTransitive && decide (x✝.predicate.Raises x✝.licenser), reflects_decide := ⋯ }

theorem CoonMateoPedroPreminger2014.not_trapped_of_v {c : Clause} (h : c.licenser = Licenser.v) : ¬Trapped c

Where v licenses the object nothing is trapped (52): the object never raises.

def CoonMateoPedroPreminger2014.SyntacticallyErgative (l : Licenser) : Prop

A language is syntactically ergative when the subject of a finite regular transitive with a full DP object is trapped when extracted (21c).

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidablePredLicenserSyntacticallyErgative : DecidablePred SyntacticallyErgative

Equations

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

theorem CoonMateoPedroPreminger2014.syntacticallyErgative_iff (l : Licenser) : SyntacticallyErgative l ↔ l = Licenser.infl

A language bans subject extraction exactly when Infl licenses the object ((19), (24)).

Case configurations

structure CoonMateoPedroPreminger2014.Configuration : Type

A clausal Case configuration (3), with the licensers of the transitive subject and of the object, where Infl licenses at most one of them.

• subject : Licenser

  The head licensing the transitive subject.

• object : Licenser

  The head licensing the transitive object.

• infl_once : self.subject = Licenser.infl → self.object = Licenser.v

  Infl licenses at most one argument.

def CoonMateoPedroPreminger2014.Configuration.MorphologicallyErgative (k : Configuration) : Prop

A configuration is morphologically ergative when v licenses the transitive subject.

Equations

• k.MorphologicallyErgative = (k.subject = CoonMateoPedroPreminger2014.Licenser.v)

theorem CoonMateoPedroPreminger2014.morphologicallyErgative_of_syntacticallyErgative (k : Configuration) (h : SyntacticallyErgative k.object) : k.MorphologicallyErgative

Syntactic ergativity entails morphological ergativity (10), since Infl licensing the object leaves the subject to v.

theorem CoonMateoPedroPreminger2014.v_not_syntacticallyErgative : { subject := Licenser.v, object := Licenser.v, infl_once := ⋯ }.MorphologicallyErgative ∧ ¬SyntacticallyErgative Licenser.v

The converse fails (10): the default-absolutive configuration is morphologically but not syntactically ergative.

Convergence

def CoonMateoPedroPreminger2014.Clause.regular (c : Clause) : Clause

The same clause under regular transitive Voice.

Equations

• c.regular = { licenser := c.licenser, finite := c.finite, predicate := c.predicate.regular, extracted := c.extracted, separated := c.separated }

def CoonMateoPedroPreminger2014.RegularCrashes (c : Clause) : Prop

The regular derivation crashes: its object is unlicensed, or its extracting subject is trapped.

Equations

• CoonMateoPedroPreminger2014.RegularCrashes c = (¬c.regular.predicate.ObjectLicensed c.licenser c.finite ∨ c.extracted = some ArgumentRole.A ∧ CoonMateoPedroPreminger2014.Trapped c.regular)

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidablePredClauseRegularCrashes : DecidablePred RegularCrashes

Equations

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

def CoonMateoPedroPreminger2014.LastResort (c : Clause) : Prop

Agent Focus is a last resort ([Ord95]; §4.2, §5.1): the Case-checking Voice merges only where the object would otherwise lack a source of Case or trap the extracting subject.

Equations

• CoonMateoPedroPreminger2014.LastResort c = (c.predicate.ChecksCase → CoonMateoPedroPreminger2014.RegularCrashes c)

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidablePredClauseLastResort : DecidablePred LastResort

Equations

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

def CoonMateoPedroPreminger2014.Converges (c : Clause) : Prop

A clause converges when its object and intransitive subject are licensed, an extracted subject is not trapped, a Case-checking Voice is a last resort, and a pseudo-incorporated object is adjacent to the verb.

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidablePredClauseConverges : DecidablePred Converges

Equations

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

theorem CoonMateoPedroPreminger2014.nonfinite_licensing (l : Licenser) : ((Predicate.transitive Minimalist.Voice.agentive Object.dp).ObjectLicensed l false ↔ l = Licenser.v) ∧ ¬(Predicate.intransitive Mayan.MarkerSet.setB).SubjectLicensed false

Non-finite licensing (27): a regular transitive object survives without Infl exactly where v licenses it, and an absolutive intransitive subject only under finite Infl.

theorem CoonMateoPedroPreminger2014.agent_focus : Converges { licenser := Licenser.infl, finite := true, predicate := Predicate.transitive voiceAF Object.dp, extracted := some ArgumentRole.A } ∧ ¬Converges { licenser := Licenser.infl, finite := true, predicate := Predicate.transitive Minimalist.Voice.agentive Object.dp, extracted := some ArgumentRole.A } ∧ Converges { licenser := Licenser.infl, finite := false, predicate := Predicate.transitive voiceAF Object.dp } ∧ ¬Converges { licenser := Licenser.infl, finite := false, predicate := Predicate.transitive Minimalist.Voice.agentive Object.dp }

Agent Focus in a high-abs language frees the extracting subject (67) and licenses the object of a non-finite transitive (70); the regular derivation crashes in both.

theorem CoonMateoPedroPreminger2014.last_resort : ¬Converges { licenser := Licenser.infl, finite := true, predicate := Predicate.transitive voiceAF Object.dp } ∧ ¬Converges { licenser := Licenser.v, finite := true, predicate := Predicate.transitive voiceAF Object.dp, extracted := some ArgumentRole.A } ∧ ¬Converges { licenser := Licenser.infl, finite := true, predicate := Predicate.transitive voiceAF Object.caseless, extracted := some ArgumentRole.A } ∧ Converges { licenser := Licenser.infl, finite := true, predicate := Predicate.transitive Minimalist.Voice.agentive Object.caseless, extracted := some ArgumentRole.A }

The last resort bars Agent Focus where nothing crashes: in a finite clause without subject extraction, in a low-abs language, and with a caseless object (75b), which instead lets the subject extract from a regular transitive (75a).

theorem CoonMateoPedroPreminger2014.antipassive_frees (l : Licenser) : ¬(Predicate.transitive Minimalist.Voice.antipassive Object.oblique).FormallyTransitive ∧ ¬(Predicate.transitive Minimalist.Voice.antipassive Object.oblique).Raises l ∧ ¬Trapped { licenser := l, finite := true, predicate := Predicate.transitive Minimalist.Voice.antipassive Object.oblique, extracted := some ArgumentRole.A }

The antipassive frees the subject (60) on either count: its v is intransitive, and its oblique patient never raises to the edge.

Agent Focus and intransitive v

def CoonMateoPedroPreminger2014.voiceOf : Mayan.VerbForm → Minimalist.Voice.Head

The Voice head of each verb form, regular Voice for the transitive and the marked Voice for Agent Focus.

Equations

• CoonMateoPedroPreminger2014.voiceOf Mayan.VerbForm.transitive = Minimalist.Voice.agentive
• CoonMateoPedroPreminger2014.voiceOf Mayan.VerbForm.agentFocus = CoonMateoPedroPreminger2014.voiceAF

theorem CoonMateoPedroPreminger2014.formallyTransitive_iff_hasSetA (f : Mayan.VerbForm) (o : Object) : (Predicate.transitive (voiceOf f) o).FormallyTransitive ↔ f.HasSetA

A form has Set A exactly when its v is formally transitive: the ergative that transitive v assigns is absent under Agent Focus (§4.1, §4.2).

theorem CoonMateoPedroPreminger2014.formallyTransitive_iff_statusSuffix (f : Mayan.VerbForm) (o : Object) : (Predicate.transitive (voiceOf f) o).FormallyTransitive ↔ Qanjobal.StatusSuffix.ofVerbForm f = Qanjobal.StatusSuffix.tv

The Q'anjob'al status suffix spells out v ((55), (65)): transitive -V' exactly when v is formally transitive, intransitive -i under Agent Focus.

The Mayan fragments

inductive CoonMateoPedroPreminger2014.Language : Type

The Mayan languages with registered fragments.

• chol : Language
• qanjobal : Language
• kaqchikel : Language
• tseltal : Language
• tsotsil : Language
• mam : Language
• kiche : Language
• yukatek : Language

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instDecidableEqLanguage : DecidableEq Language

Equations

• CoonMateoPedroPreminger2014.instDecidableEqLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoonMateoPedroPreminger2014.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instReprLanguage : Repr Language

Equations

• CoonMateoPedroPreminger2014.instReprLanguage = { reprPrec := CoonMateoPedroPreminger2014.instReprLanguage.repr }

@[instance_reducible]

instance CoonMateoPedroPreminger2014.instFintypeLanguage : Fintype Language

Equations

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

def CoonMateoPedroPreminger2014.Language.glottocode : Language → String

The Glottolog code of a language, the key the rows carry.

Equations

• CoonMateoPedroPreminger2014.Language.chol.glottocode = "chol1282"
• CoonMateoPedroPreminger2014.Language.qanjobal.glottocode = "qanj1241"
• CoonMateoPedroPreminger2014.Language.kaqchikel.glottocode = "kaqc1270"
• CoonMateoPedroPreminger2014.Language.tseltal.glottocode = "tzel1254"
• CoonMateoPedroPreminger2014.Language.tsotsil.glottocode = "tzot1259"
• CoonMateoPedroPreminger2014.Language.mam.glottocode = "mamm1241"
• CoonMateoPedroPreminger2014.Language.kiche.glottocode = "kich1262"
• CoonMateoPedroPreminger2014.Language.yukatek.glottocode = "yuca1254"

def CoonMateoPedroPreminger2014.Language.template : Language → Morphology.AffixTemplate Mayan.VerbSlot

The verbal complex of a language, from its fragment.

Equations

• CoonMateoPedroPreminger2014.Language.chol.template = Chol.template
• CoonMateoPedroPreminger2014.Language.qanjobal.template = Qanjobal.template
• CoonMateoPedroPreminger2014.Language.kaqchikel.template = Kaqchikel.template
• CoonMateoPedroPreminger2014.Language.tseltal.template = Tseltal.template
• CoonMateoPedroPreminger2014.Language.tsotsil.template = Tsotsil.template
• CoonMateoPedroPreminger2014.Language.mam.template = Mam.template
• CoonMateoPedroPreminger2014.Language.kiche.template = Kiche.template
• CoonMateoPedroPreminger2014.Language.yukatek.template = Yukatek.template

def CoonMateoPedroPreminger2014.Language.absPosition (L : Language) : Mayan.ABSPosition

The absolutive's position in a language, read off its verbal complex (16).

Equations

• L.absPosition = Mayan.absPosition L.template

def CoonMateoPedroPreminger2014.Language.licenser (L : Language) : Licenser

The head licensing a language's transitive objects.

Equations

• L.licenser = CoonMateoPedroPreminger2014.Licenser.ofPosition L.absPosition

def CoonMateoPedroPreminger2014.Language.setB : Language → Mayan.ExponentTable

The Set B exponents of a language, from its fragment.

Equations

• CoonMateoPedroPreminger2014.Language.chol.setB = Chol.setBExponent
• CoonMateoPedroPreminger2014.Language.qanjobal.setB = Qanjobal.setBExponent
• CoonMateoPedroPreminger2014.Language.kaqchikel.setB = Kaqchikel.setBExponent
• CoonMateoPedroPreminger2014.Language.tseltal.setB = Tseltal.setBExponent
• CoonMateoPedroPreminger2014.Language.tsotsil.setB = Tsotsil.setBExponent
• CoonMateoPedroPreminger2014.Language.mam.setB = Mam.setBExponent
• CoonMateoPedroPreminger2014.Language.kiche.setB = Kiche.setBExponent
• CoonMateoPedroPreminger2014.Language.yukatek.setB = Yukatek.setBExponent

def CoonMateoPedroPreminger2014.Language.assignCase : Language → UD.Aspect → ArgumentRole → Case

Case assignment by aspect in a language, from its fragment.

Equations

• CoonMateoPedroPreminger2014.Language.chol.assignCase = Chol.assignCase
• CoonMateoPedroPreminger2014.Language.qanjobal.assignCase = Qanjobal.assignCase
• CoonMateoPedroPreminger2014.Language.kaqchikel.assignCase = Kaqchikel.assignCase
• CoonMateoPedroPreminger2014.Language.tseltal.assignCase = Tseltal.assignCase
• CoonMateoPedroPreminger2014.Language.tsotsil.assignCase = Tsotsil.assignCase
• CoonMateoPedroPreminger2014.Language.mam.assignCase = Mam.assignCase
• CoonMateoPedroPreminger2014.Language.kiche.assignCase = Kiche.assignCase
• CoonMateoPedroPreminger2014.Language.yukatek.assignCase = Yukatek.assignCase

def CoonMateoPedroPreminger2014.Language.IsErgativePerfective (L : Language) : Prop

The language is ergatively aligned in the perfective (§2.1).

Equations

• L.IsErgativePerfective = Alignment.IsErgative (L.assignCase UD.Aspect.Perf)

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Language.instDecidablePredIsErgativePerfective : DecidablePred IsErgativePerfective

Equations

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

def CoonMateoPedroPreminger2014.Language.MarksExtraction : Language → ArgumentRole → Prop

The fragment records a reflex for the extraction of an argument on some verb, with third-person arguments where the marking depends on their person. The Yukatek fragment records no extraction reflexes, and its value is a junk False.

Equations

• One or more equations did not get rendered due to their size.
• CoonMateoPedroPreminger2014.Language.chol.MarksExtraction x✝ = ∃ m ∈ Chol.Extraction.realize (Mayan.ExtractionSite.argument x✝), m.Nonempty
• CoonMateoPedroPreminger2014.Language.qanjobal.MarksExtraction x✝ = ∃ m ∈ Qanjobal.Extraction.realize Person.third (Mayan.ExtractionSite.argument x✝), m.Nonempty
• CoonMateoPedroPreminger2014.Language.tseltal.MarksExtraction x✝ = ∃ m ∈ Tseltal.Extraction.realize (Mayan.ExtractionSite.argument x✝), m.Nonempty
• CoonMateoPedroPreminger2014.Language.tsotsil.MarksExtraction x✝ = ∃ m ∈ Tsotsil.Extraction.realize (Mayan.ExtractionSite.argument x✝), m.Nonempty
• CoonMateoPedroPreminger2014.Language.mam.MarksExtraction x✝ = (Mam.Extraction.realize (Mayan.ExtractionSite.argument x✝)).Nonempty
• CoonMateoPedroPreminger2014.Language.kiche.MarksExtraction x✝ = ∃ (c : Mayan.VerbClass), (Kiche.Extraction.realize c (Mayan.ExtractionSite.argument x✝)).Nonempty
• CoonMateoPedroPreminger2014.Language.yukatek.MarksExtraction x✝ = False

@[instance_reducible]

instance CoonMateoPedroPreminger2014.Language.instDecidableMarksExtraction (L : Language) (r : ArgumentRole) : Decidable (L.MarksExtraction r)

Equations

• CoonMateoPedroPreminger2014.Language.chol.instDecidableMarksExtraction x✝ = (Chol.Extraction.realize (Mayan.ExtractionSite.argument x✝)).decidableExistsMem
• CoonMateoPedroPreminger2014.Language.qanjobal.instDecidableMarksExtraction x✝ = (Qanjobal.Extraction.realize Person.third (Mayan.ExtractionSite.argument x✝)).decidableExistsMem
• CoonMateoPedroPreminger2014.Language.tseltal.instDecidableMarksExtraction x✝ = (Tseltal.Extraction.realize (Mayan.ExtractionSite.argument x✝)).decidableExistsMem
• CoonMateoPedroPreminger2014.Language.tsotsil.instDecidableMarksExtraction x✝ = (Tsotsil.Extraction.realize (Mayan.ExtractionSite.argument x✝)).decidableExistsMem
• CoonMateoPedroPreminger2014.Language.mam.instDecidableMarksExtraction x✝ = Finset.decidableNonempty
• CoonMateoPedroPreminger2014.Language.kaqchikel.instDecidableMarksExtraction x✝ = Fintype.decidableExistsFintype
• CoonMateoPedroPreminger2014.Language.kiche.instDecidableMarksExtraction x✝ = Fintype.decidableExistsFintype
• CoonMateoPedroPreminger2014.Language.yukatek.instDecidableMarksExtraction x✝ = { decide := false, reflects_decide := ⋯ }

theorem CoonMateoPedroPreminger2014.isErgativePerfective_iff (L : Language) : L.IsErgativePerfective ↔ L ≠ Language.mam

Every registered language but San Juan Atitán Mam, which is tripartite, assigns case ergatively in the perfective (§2.1).

theorem CoonMateoPedroPreminger2014.thirdSgZero_of_isErgativePerfective {L : Language} (h : L.IsErgativePerfective) : L.setB.IsThirdSgZero

Third person singular absolutive is null in every registered language ergative in the perfective (13); Mam's default Set B surfaces there.

theorem CoonMateoPedroPreminger2014.tada (L : Language) (h₁ : L ≠ Language.tsotsil) (h₂ : L ≠ Language.yukatek) {r : ArgumentRole} (hr : r ∈ ArgumentRole.core) : L.MarksExtraction r ↔ ¬Converges { licenser := L.licenser, finite := true, predicate := Predicate.transitive Minimalist.Voice.agentive Object.dp, extracted := some r }

Tada's generalization over the fragments (19), extended to every core argument. A registered language marks the extraction of a core argument from a finite transitive exactly when the regular derivation fails, so its subject's extraction is marked when the absolutive is high and its object's never. The recipient, an oblique whose extraction the K'ichean languages and Mam mark as a low adjunct's, is outside the generalization. Footnote 8 leaves Tsotsil out of table (19), its two absolutive series resisting the classification, and calls Yucatec an apparent outlier; the Yukatek fragment records no extraction reflexes, so both stay outside.

theorem CoonMateoPedroPreminger2014.tsotsil_marks_free_extraction : Language.tsotsil.MarksExtraction ArgumentRole.A ∧ Converges { licenser := Language.tsotsil.licenser, finite := true, predicate := Predicate.transitive Minimalist.Voice.agentive Object.dp, extracted := some ArgumentRole.A }

Tsotsil, low absolutive by its template, still marks the extraction of a transitive subject that the regular derivation allows, with its optional Agent Focus.

theorem CoonMateoPedroPreminger2014.converges_iff_verbForm {agent : Person} (ha : ¬agent.IsSAP) (finite : Bool) (e : Option ArgumentRole) (f : Mayan.VerbForm) : Converges { licenser := Language.qanjobal.licenser, finite := finite, predicate := Predicate.transitive (voiceOf f) Object.dp, extracted := e } ↔ Qanjobal.verbForm finite e agent = f

The derivation picks out the fragment's verb form (§4.2, §5.1): with a third-person agent and a full DP object, a Q'anjob'al clause converges under the Voice of exactly the form Qanjobal.verbForm records, Agent Focus in every non-finite transitive and under subject extraction.

The paper's examples

def CoonMateoPedroPreminger2014.absPositions : List (String × Mayan.ABSPosition)

The paper's labels for the absolutive positions.

Equations

• CoonMateoPedroPreminger2014.absPositions = [("high", Mayan.ABSPosition.high), ("low", Mayan.ABSPosition.low)]

def CoonMateoPedroPreminger2014.objects : List (String × Object)

The rows' labels for the objects.

Equations

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

def CoonMateoPedroPreminger2014.Predicate.ofRow (row : Datum) : Option Predicate

The verb phrase a row describes.

Equations

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

def CoonMateoPedroPreminger2014.Clause.ofRow (row : Datum) : Option Clause

The clause a row describes, its object's licenser read off the paper's classification of its language.

Equations

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

theorem CoonMateoPedroPreminger2014.analysed_rows (row : Datum) : row ∈ Examples.all → (row.feature? "predicate").isSome = true → ∃ c ∈ Clause.ofRow row, row.judgment = Judgment.acceptable ↔ Converges c

Every analysed example is grammatical exactly when its clause converges.

theorem CoonMateoPedroPreminger2014.rows_match_fragments (row : Datum) : row ∈ Examples.all → ∀ (L : Language), L.glottocode = row.language → row.parse? "absPosition" absPositions = some L.absPosition

The rows' classification of a registered language agrees with its verbal complex.