Mayan extraction morphology

In most Mayan languages the focusing, questioning or relativization of a transitive subject changes the verb: it takes the Agent Focus form, which lacks the Set A marker and carries a suffix of its own, so that a clause with two arguments is inflected like an intransitive, as Stiebels and Polian describe it. The form is obligatory in the languages with the ergative extraction constraint, optional in Tsotsil, and absent in Chol and Tseltal; Mam extracts a transitive subject through its antipassive instead. Several languages also mark the extraction of non-core arguments and adjuncts, K'iche' and Kaqchikel with the particle wi and Mam with the enclitic =(y)a', and which classes of adjunct license the marker varies.

Each language's Extraction.realize records the reflexes an extraction from each site licenses, as a finite set of Reflex Mayan.Host. The reflex of transitive-subject extraction is the marker of the voice the verb switches to, Agent Focus or the antipassive. A fragment whose sources leave some sites undescribed gives its values in Option, none at those sites and some ∅ where an extraction is documented as unmarked.

Main declarations

• Mayan.VerbForm: the transitive and Agent Focus forms, with Mayan.VerbForm.HasSetA.
• Mayan.Adjunct, Mayan.ExtractionSite: the adjunct classes, and the extraction sites, an argument by its role or an adjunct by its class.
• Mayan.Host: the constituents an extraction reflex is hosted by.

Implementation notes

The argument sites are the comparative roles, so a recipient is .argument .R however a language codes it. The K'ichean languages and Mam code it as an oblique introduced by a relational noun, the indirect object or dative of Mendes and Ranero and of Elkins, Torrence and Brown, and its extraction is marked as a low adjunct's is. Chol and the Tseltalan languages make it the primary object of the applicative -be, cross-referenced by Set B, and it extracts as the patient does.

References

• [EBT26]
• [MR21b]
• [Pol17a]
• [Sti06]

inductive Mayan.VerbForm : Type

A transitive verb has the canonical transitive form and the Agent Focus form, which transitive-subject extraction selects wherever a language has it.

• transitive : VerbForm
• agentFocus : VerbForm

@[instance_reducible]

instance Mayan.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

• Mayan.instDecidableEqVerbForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mayan.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

• Mayan.instReprVerbForm.repr Mayan.VerbForm.transitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbForm.transitive")).group prec✝
• Mayan.instReprVerbForm.repr Mayan.VerbForm.agentFocus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbForm.agentFocus")).group prec✝

@[instance_reducible]

instance Mayan.instReprVerbForm : Repr VerbForm

Equations

• Mayan.instReprVerbForm = { reprPrec := Mayan.instReprVerbForm.repr }

@[instance_reducible]

instance Mayan.instFintypeVerbForm : Fintype VerbForm

Equations

• Mayan.instFintypeVerbForm = { elems := { val := ↑Mayan.VerbForm.enumList, nodup := Mayan.VerbForm.enumList_nodup }, complete := Mayan.instFintypeVerbForm._proof_1 }

def Mayan.VerbForm.HasSetA (f : VerbForm) : Prop

The form bears Set A: the canonical transitive does, while the Agent Focus form is inflected as an intransitive and bears only Set B ([Pol17a]).

Equations

• f.HasSetA = (f = Mayan.VerbForm.transitive)

@[instance_reducible]

instance Mayan.instDecidablePredVerbFormHasSetA : DecidablePred VerbForm.HasSetA

Equations

• Mayan.instDecidablePredVerbFormHasSetA f = Mayan.instDecidablePredVerbFormHasSetA._aux_1 f

inductive Mayan.Adjunct : Type

The classes of adjunct that Mayan extraction morphology distinguishes. Comitatives, which the K'ichean particle also tracks, are not carried.

• instrument : Adjunct
• benefactive : Adjunct
• locative : Adjunct
• reason : Adjunct
• purpose : Adjunct
• manner : Adjunct
• temporal : Adjunct

@[instance_reducible]

instance Mayan.instDecidableEqAdjunct : DecidableEq Adjunct

Equations

• Mayan.instDecidableEqAdjunct x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mayan.instReprAdjunct.repr : Adjunct → ℕ → Std.Format

Equations

• Mayan.instReprAdjunct.repr Mayan.Adjunct.instrument prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.instrument")).group prec✝
• Mayan.instReprAdjunct.repr Mayan.Adjunct.benefactive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.benefactive")).group prec✝
• Mayan.instReprAdjunct.repr Mayan.Adjunct.locative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.locative")).group prec✝
• Mayan.instReprAdjunct.repr Mayan.Adjunct.reason prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.reason")).group prec✝
• Mayan.instReprAdjunct.repr Mayan.Adjunct.purpose prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.purpose")).group prec✝
• Mayan.instReprAdjunct.repr Mayan.Adjunct.manner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.manner")).group prec✝
• Mayan.instReprAdjunct.repr Mayan.Adjunct.temporal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Adjunct.temporal")).group prec✝

@[instance_reducible]

instance Mayan.instReprAdjunct : Repr Adjunct

Equations

• Mayan.instReprAdjunct = { reprPrec := Mayan.instReprAdjunct.repr }

@[instance_reducible]

instance Mayan.instFintypeAdjunct : Fintype Adjunct

Equations

• Mayan.instFintypeAdjunct = { elems := { val := ↑Mayan.Adjunct.enumList, nodup := Mayan.Adjunct.enumList_nodup }, complete := Mayan.instFintypeAdjunct._proof_1 }

inductive Mayan.ExtractionSite : Type

An extraction site is an argument, by its role, or an adjunct, by its class, the granularity the marking distinguishes.

• argument (r : ArgumentRole) : ExtractionSite
• adjunct (a : Adjunct) : ExtractionSite

@[instance_reducible]

instance Mayan.instDecidableEqExtractionSite : DecidableEq ExtractionSite

Equations

• Mayan.instDecidableEqExtractionSite = Mayan.instDecidableEqExtractionSite.decEq

def Mayan.instDecidableEqExtractionSite.decEq (x✝ x✝¹ : ExtractionSite) : Decidable (x✝ = x✝¹)

Equations

• Mayan.instDecidableEqExtractionSite.decEq (Mayan.ExtractionSite.argument a) (Mayan.ExtractionSite.argument b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Mayan.instDecidableEqExtractionSite.decEq (Mayan.ExtractionSite.argument r) (Mayan.ExtractionSite.adjunct a) = isFalse ⋯
• Mayan.instDecidableEqExtractionSite.decEq (Mayan.ExtractionSite.adjunct a) (Mayan.ExtractionSite.argument r) = isFalse ⋯
• Mayan.instDecidableEqExtractionSite.decEq (Mayan.ExtractionSite.adjunct a) (Mayan.ExtractionSite.adjunct b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Mayan.instReprExtractionSite.repr : ExtractionSite → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Mayan.instReprExtractionSite : Repr ExtractionSite

Equations

• Mayan.instReprExtractionSite = { reprPrec := Mayan.instReprExtractionSite.repr }

@[instance_reducible]

instance Mayan.instFintypeExtractionSite : Fintype ExtractionSite

Equations

• Mayan.instFintypeExtractionSite = Fintype.ofEquiv (ArgumentRole ⊕ Mayan.Adjunct) Mayan.ExtractionSite.proxyTypeEquiv

inductive Mayan.Host : Type

An extraction reflex is hosted by the verb stem, which a voice suffix alters, by the verbal complex, the word a particle or enclitic closes, by a directional auxiliary, or by the extracted phrase itself.

• verb : Host
• verbalComplex : Host
• directional : Host
• phrase : Host

@[instance_reducible]

instance Mayan.instDecidableEqHost : DecidableEq Host

Equations

• Mayan.instDecidableEqHost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Mayan.instReprHost : Repr Host

Equations

• Mayan.instReprHost = { reprPrec := Mayan.instReprHost.repr }

def Mayan.instReprHost.repr : Host → ℕ → Std.Format

Equations

• Mayan.instReprHost.repr Mayan.Host.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Host.verb")).group prec✝
• Mayan.instReprHost.repr Mayan.Host.verbalComplex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Host.verbalComplex")).group prec✝
• Mayan.instReprHost.repr Mayan.Host.directional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Host.directional")).group prec✝
• Mayan.instReprHost.repr Mayan.Host.phrase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Host.phrase")).group prec✝

@[instance_reducible]

instance Mayan.instFintypeHost : Fintype Host

Equations

• Mayan.instFintypeHost = { elems := { val := ↑Mayan.Host.enumList, nodup := Mayan.Host.enumList_nodup }, complete := Mayan.instFintypeHost._proof_1 }