K'iche' Extraction Morphology

Theory-neutral data on the extraction particle wi (the "fronting particle") in K'iche' and Kaqchikel (K'ichean Mayan), following [MR21], [ETB26], and [Mon17]. When a low adjunct (locative, instrumental, comitative, indirect object) undergoes Ā-extraction, wi appears as a verbal enclitic; [MR21] analyze it as Chain Reduction via Substitution, with the lower copy of the moved adjunct (bearing [APPL]) substituted by wi rather than deleted.

Main declarations

• Kiche.KicheExtractionDatum, Kiche.allData: the wi-distribution data points.
• Kiche.KicheLongDistanceDatum, Kiche.ldData: long-distance extraction data across embedded CP vs AspP.
• Kiche.fronting_particle_generalization: matrix wi is contingent on an overt embedded complementizer.
• Kiche.Extraction.realize: the AF- and wi-based extraction marking, with Kiche.Extraction.strategy as the WALS-style label.

Implementation notes

wi triggers only on low adjuncts introduced in Spec,ApplP (instrumentals, locatives, comitatives, indirect objects); temporal and reason adjuncts do not trigger it. It is obligatory in K'iche', optional in Patzún Kaqchikel, and absent in some Kaqchikel dialects (e.g. Tecpán). [MR21] §4 argues wi is not a pronoun, applicative head, movement trigger, or AF morpheme. The Fronting Particle Generalization ([MR21] definition (5), first observed by Can Pixabaj 2015) is stated and checked at fronting_particle_generalization.

Extracted argument types

inductive Kiche.ExtractedArgType : Type

Types of extracted arguments relevant for wi distribution.

• obliqueSpatial : ExtractedArgType
• obliqueTemporal : ExtractedArgType
• obliqueReason : ExtractedArgType
• obliqueInstrumental : ExtractedArgType
• subject : ExtractedArgType
• object : ExtractedArgType

@[implicit_reducible]

instance Kiche.instDecidableEqExtractedArgType : DecidableEq ExtractedArgType

Equations

• Kiche.instDecidableEqExtractedArgType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kiche.instReprExtractedArgType.repr : ExtractedArgType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiche.instReprExtractedArgType : Repr ExtractedArgType

Equations

• Kiche.instReprExtractedArgType = { reprPrec := Kiche.instReprExtractedArgType.repr }

def Kiche.ExtractedArgType.isOblique : ExtractedArgType → Bool

Is this argument type an oblique?

Equations

• Kiche.ExtractedArgType.obliqueSpatial.isOblique = true
• Kiche.ExtractedArgType.obliqueTemporal.isOblique = true
• Kiche.ExtractedArgType.obliqueReason.isOblique = true
• Kiche.ExtractedArgType.obliqueInstrumental.isOblique = true
• Kiche.ExtractedArgType.subject.isOblique = false
• Kiche.ExtractedArgType.object.isOblique = false

wi distribution data

structure Kiche.KicheExtractionDatum : Type

A K'iche' extraction data point: what is extracted and whether wi appears after the verb.

• label : String
• reference : String
• extractedType : ExtractedArgType
• wiLicensed : Bool

@[implicit_reducible]

instance Kiche.instReprKicheExtractionDatum : Repr KicheExtractionDatum

Equations

• Kiche.instReprKicheExtractionDatum = { reprPrec := Kiche.instReprKicheExtractionDatum.repr }

def Kiche.instReprKicheExtractionDatum.repr : KicheExtractionDatum → ℕ → Std.Format

Equations

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

def Kiche.spatialOblExtraction : KicheExtractionDatum

Spatial oblique extraction ("Where did you go yesterday?"): wi licensed. [Mon17] Lesson 14; [MR21] §2, ex. (9a).

Equations

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

def Kiche.instrumentalOblExtraction : KicheExtractionDatum

Instrumental oblique extraction ("With what did they eat their food?"): wi licensed. [MR21] §2, ex. (9b).

Equations

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

def Kiche.temporalOblExtraction : KicheExtractionDatum

Temporal oblique extraction ("When did you eat beans?"): wi NOT licensed — parallel to Mam, where temporal obliques are also exempt. [MR21] §2, ex. (12c).

Equations

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

def Kiche.reasonOblExtraction : KicheExtractionDatum

Reason oblique extraction ("Why did Juan work?"): wi NOT licensed — key contrast with Mam, where SJO =(y)a' IS licensed with reason extraction. [MR21] §2 (adapted from Elkins et al. Table 3).

Equations

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

def Kiche.subjectExtraction : KicheExtractionDatum

Subject extraction ("Who bought it?"): wi NOT licensed — Agent Focus morphology -Vk appears instead. [MR21] §2, item (6c).

Equations

• Kiche.subjectExtraction = { label := "Subject extraction (AF, no wi)", reference := "Mendes & Ranero 2021, §2, item (6c)", extractedType := Kiche.ExtractedArgType.subject, wiLicensed := false }

def Kiche.objectExtraction : KicheExtractionDatum

Object extraction ("What did you buy?"): wi NOT licensed. [ETB26].

Equations

• Kiche.objectExtraction = { label := "Object extraction (no wi)", reference := "Elkins et al. 2026", extractedType := Kiche.ExtractedArgType.object, wiLicensed := false }

def Kiche.allData : List KicheExtractionDatum

All K'iche' extraction data points.

Equations

• Kiche.allData = [Kiche.spatialOblExtraction, Kiche.instrumentalOblExtraction, Kiche.temporalOblExtraction, Kiche.reasonOblExtraction, Kiche.subjectExtraction, Kiche.objectExtraction]

Generalizations

theorem Kiche.wi_subset_of_obliques : (allData.all fun (d : KicheExtractionDatum) => d.wiLicensed == (d.extractedType == ExtractedArgType.obliqueSpatial || d.extractedType == ExtractedArgType.obliqueInstrumental)) = true

Among the formalized data points, wi is licensed exactly for spatial and instrumental obliques; the full trigger set also includes comitatives and indirect objects ([MR21] §2; [ETB26] Table 3), not yet formalized here.

theorem Kiche.wi_not_core_args : subjectExtraction.wiLicensed = false ∧ objectExtraction.wiLicensed = false

wi does not appear with subject or object extraction.

theorem Kiche.temporal_exempt : temporalOblExtraction.wiLicensed = false

Temporal exemption is shared across Mayan: neither wi (K'ichean) nor =(y)a' (Mam) appears with temporal oblique extraction.

Embedded clause types and the Fronting Particle Generalization

inductive Kiche.KicheEmbeddedClauseType : Type

Embedded clause types for long-distance wi distribution: whether the embedded clause has an overt complementizer (CP) or not (a structurally reduced AspP). [MR21] §2, exx. (17)–(20), (34)–(37).

• cp : KicheEmbeddedClauseType

  Full CP with overt complementizer chi.

• aspP : KicheEmbeddedClauseType

  Reduced AspP without complementizer.

@[implicit_reducible]

instance Kiche.instDecidableEqKicheEmbeddedClauseType : DecidableEq KicheEmbeddedClauseType

Equations

• Kiche.instDecidableEqKicheEmbeddedClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiche.instReprKicheEmbeddedClauseType : Repr KicheEmbeddedClauseType

Equations

• Kiche.instReprKicheEmbeddedClauseType = { reprPrec := Kiche.instReprKicheEmbeddedClauseType.repr }

def Kiche.instReprKicheEmbeddedClauseType.repr : KicheEmbeddedClauseType → ℕ → Std.Format

Equations

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

def Kiche.KicheEmbeddedClauseType.hasComp : KicheEmbeddedClauseType → Bool

Does this clause type have an overt complementizer?

Equations

• Kiche.KicheEmbeddedClauseType.cp.hasComp = true
• Kiche.KicheEmbeddedClauseType.aspP.hasComp = false

structure Kiche.KicheLongDistanceDatum : Type

Long-distance extraction datum for K'ichean wi.

• label : String
• reference : String
• embeddedType : KicheEmbeddedClauseType
• wiOnMatrix : Bool

  Does wi appear on the matrix predicate?

• wiOnEmbedded : Bool

  Does wi appear on the embedded predicate?

def Kiche.instReprKicheLongDistanceDatum.repr : KicheLongDistanceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiche.instReprKicheLongDistanceDatum : Repr KicheLongDistanceDatum

Equations

• Kiche.instReprKicheLongDistanceDatum = { reprPrec := Kiche.instReprKicheLongDistanceDatum.repr }

def Kiche.ldFromCP : KicheLongDistanceDatum

LD from embedded CP: wi on BOTH matrix and embedded predicates. [MR21] §3, ex. (34); adapted from Can Pixabaj 2015: 166–167.

Equations

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

def Kiche.ldFromAspP : KicheLongDistanceDatum

LD from embedded AspP: wi only on embedded predicate, NOT matrix. [MR21] §3, ex. (35); adapted from Can Pixabaj 2015: 163.

Equations

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

def Kiche.ldData : List KicheLongDistanceDatum

Equations

• Kiche.ldData = [Kiche.ldFromCP, Kiche.ldFromAspP]

theorem Kiche.fronting_particle_generalization : (ldData.all fun (d : KicheLongDistanceDatum) => d.embeddedType.hasComp == d.wiOnMatrix) = true

The Fronting Particle Generalization ([MR21] definition (5); first discussed by Can Pixabaj 2015): in long-distance Ā-extraction of a low adjunct from a single embedded clause, matrix wi is contingent on an overt complementizer in the embedded clause. Structurally ([MR21] §3), C⁰ is a phase head — an embedded CP forces a stopover in embedded Spec,CP whose intermediate copy undergoes Chain Reduction via Substitution (matrix wi), while an embedded AspP has no phase boundary and the adjunct moves directly to matrix Spec,CP (no matrix wi).

Extraction marking

inductive Kiche.Extraction.Site : Type

Reflex hosts for K'iche' extraction marking.

• verb : Site

@[implicit_reducible]

instance Kiche.Extraction.instDecidableEqSite : DecidableEq Site

Equations

• Kiche.Extraction.instDecidableEqSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiche.Extraction.instReprSite : Repr Site

Equations

• Kiche.Extraction.instReprSite = { reprPrec := Kiche.Extraction.instReprSite.repr }

def Kiche.Extraction.instReprSite.repr : Site → ℕ → Std.Format

Equations

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

def Kiche.Extraction.realize : Extraction.ExtractionTarget → List (Features.Reflex Site)

K'iche' marks two extraction cells on the verb: subject extraction switches it to AF (the voice marker -n, [Mon17] Lesson 22; Lessons 30, 33 for radical transitives and perfect aspect; shared with the Absolutive Antipassive of Lesson 21, from which AF differs syntactically, not morphologically), and oblique extraction adds wi via copy spellout at the foot of the Ā-chain ([MR21]). Core-object extraction is unmarked.

Equations

• Kiche.Extraction.realize Extraction.ExtractionTarget.subject = [Features.Reflex.morpheme Kiche.Extraction.Site.verb]
• Kiche.Extraction.realize Extraction.ExtractionTarget.oblique = [Features.Reflex.morpheme Kiche.Extraction.Site.verb]
• Kiche.Extraction.realize x✝ = []

def Kiche.Extraction.strategy : Extraction.ExtractionMarkingStrategy

WALS-style label: dedicated morphemes mark extraction.

Equations

• Kiche.Extraction.strategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme

theorem Kiche.Extraction.marks_oblique : Extraction.Marked realize Extraction.ExtractionTarget.oblique