Mam Extraction Morphology Fragment

Theory-neutral data on extraction morphology in San Juan Ostuncalco (SJO) Mam (Mayan, Western Highlands of Guatemala), following [ETB26]. When an oblique undergoes Ā-movement (wh-movement, focus fronting, relativization), the optional enclitic =(y)a' may appear on the verbal complex — on Voice⁰ or Dir⁰ (directional auxiliary). Its distribution is conditioned by clause size (licensed only where Voice⁰ projects; impossible in VP-sized infinitival complements, [ETB26] §6) and by extraction target (oblique extraction only — subject extraction triggers Agent Focus -a, object extraction triggers neither, §3.1; temporal 'when' obliques also do not trigger it, §8.1).

The central finding is multiple spellout: in long-distance extraction through full CPs and aspectless clauses, =(y)a' can appear on both the matrix and embedded predicates — one per Voice/Dir head along the successive-cyclic movement path (Table 4, §6.2).

Main declarations

• Mam.MamClauseType with .projectsVoice: the three clause sizes (full CP, aspectless, infinitival) and whether each projects Voice.
• Mam.MamExtractionDatum, Mam.monoData: monoclausal extraction data points and their pooled list.
• Mam.MamLongDistanceDatum, Mam.ldData: long-distance data tracking =(y)a' on the matrix and embedded predicates independently (Table 4).
• Mam.eqya_iff_voice_and_oblique: the core generalization — =(y)a' is licensed iff the clause projects Voice and a non-temporal oblique extracts.
• Mam.MovementReflex with .islandSensitive: island sensitivity derived from movement being phase-bounded rather than stipulated.
• Mam.Extraction.realize: the AF- and =(y)a'-based extraction marking, with Mam.Extraction.strategy as the WALS-style label.

Implementation notes

All data is from [ETB26], "Wh-movement paths and oblique extraction in Mam (Mayan)", cited by section/example number.

Clause types

inductive Mam.MamClauseType : Type

The three clause sizes relevant for =(y)a' distribution — different structural sizes of the verbal domain ([ETB26] §6.1, following [Coo19]).

• fullCP : MamClauseType

  Full finite clause with aspect; projects Voice, so =(y)a' is licensed on oblique extraction.

• aspectless : MamClauseType

  VoiceP-sized complement: no aspect but projects Voice, so =(y)a' is licensed ([ETB26] §6.1).

• infinitival : MamClauseType

  VP-sized infinitival complement: no Voice projected, so =(y)a' is impossible — no Voice⁰ to host [oblique] ([ETB26] §6.1).

@[implicit_reducible]

instance Mam.instDecidableEqMamClauseType : DecidableEq MamClauseType

Equations

• Mam.instDecidableEqMamClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mam.instReprMamClauseType : Repr MamClauseType

Equations

• Mam.instReprMamClauseType = { reprPrec := Mam.instReprMamClauseType.repr }

def Mam.instReprMamClauseType.repr : MamClauseType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Mam.instReprMamClauseType.repr Mam.MamClauseType.fullCP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.MamClauseType.fullCP")).group prec✝

def Mam.MamClauseType.projectsVoice : MamClauseType → Bool

Does this clause type project Voice?

Equations

• Mam.MamClauseType.fullCP.projectsVoice = true
• Mam.MamClauseType.aspectless.projectsVoice = true
• Mam.MamClauseType.infinitival.projectsVoice = false

Extraction judgments

inductive Mam.MamExtractionJudgment : Type

Status of =(y)a' in a configuration — licensed (may grammatically appear; it is an optional enclitic) or blocked; optionality when licensed is orthogonal to the distributional constraints.

• licensed : MamExtractionJudgment

  =(y)a' is licensed (may appear) in this configuration

• blocked : MamExtractionJudgment

  =(y)a' is blocked (may not appear) in this configuration

@[implicit_reducible]

instance Mam.instDecidableEqMamExtractionJudgment : DecidableEq MamExtractionJudgment

Equations

• Mam.instDecidableEqMamExtractionJudgment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mam.instReprMamExtractionJudgment : Repr MamExtractionJudgment

Equations

• Mam.instReprMamExtractionJudgment = { reprPrec := Mam.instReprMamExtractionJudgment.repr }

def Mam.instReprMamExtractionJudgment.repr : MamExtractionJudgment → ℕ → Std.Format

Equations

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

Monoclausal data

structure Mam.MamExtractionDatum : Type

A monoclausal extraction data point: a clause type, what is extracted, and whether =(y)a' is licensed.

• label : String

  Descriptive label

• reference : String

  Section/example reference in [ETB26]

• clauseType : MamClauseType

  Type of clause

• obliqueExtracted : Bool

  Is an oblique being extracted?

• isTemporal : Bool

  Is the extracted oblique temporal ('when')? Temporal obliques do not trigger =(y)a' though genuinely oblique and extracted (§8.1, ex. 56) — encoded honestly rather than as obliqueExtracted := false. The paper leaves this unexplained: "we leave an account of this for future work" (§8.1).

• judgment : MamExtractionJudgment

  Judgment on =(y)a'

def Mam.instReprMamExtractionDatum.repr : MamExtractionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mam.instReprMamExtractionDatum : Repr MamExtractionDatum

Equations

• Mam.instReprMamExtractionDatum = { reprPrec := Mam.instReprMamExtractionDatum.repr }

def Mam.transOblExtraction : MamExtractionDatum

Transitive clause, oblique extraction: =(y)a' licensed. "With what did María clean the window?" — =(y)a' on predicate. Elkins et al. §4.1, ex. (22b).

Equations

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

def Mam.transSubjExtraction : MamExtractionDatum

Transitive clause, subject extraction: =(y)a' blocked. "Who opened the door?" — antipassive required, no =(y)a'. Elkins et al. §3.2, ex. (19).

Equations

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

def Mam.transObjExtraction : MamExtractionDatum

Transitive clause, object extraction: =(y)a' blocked. "What did María open?" — no =(y)a'. Elkins et al. §3.2, ex. (18b).

Equations

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

def Mam.passiveOblExtraction : MamExtractionDatum

Passive clause, oblique extraction: =(y)a' licensed. "Where were the tortillas sold by Juan?" — =(y)a' co-occurs with passive -njtz. Elkins et al. §7.2, ex. (54).

Equations

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

def Mam.temporalOblExtraction : MamExtractionDatum

Temporal oblique extraction: =(y)a' BLOCKED. "When" (b'iix taq) does not trigger =(y)a', unlike spatial and other obliques (§8.1, ex. (56)); encoded honestly as obliqueExtracted := true, isTemporal := true. Unexplained: "we leave an account of this for future work" (§8.1).

Equations

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

def Mam.monoData : List MamExtractionDatum

All monoclausal extraction data points.

Equations

• Mam.monoData = [Mam.transOblExtraction, Mam.transSubjExtraction, Mam.transObjExtraction, Mam.passiveOblExtraction, Mam.temporalOblExtraction]

Long-distance data (Table 4)

structure Mam.MamLongDistanceDatum : Type

A long-distance extraction data point: tracks =(y)a' status on both the matrix and embedded predicates independently. This captures the paper's central empirical finding (Table 4, §6.2): =(y)a' can appear on BOTH predicates along the successive-cyclic movement path.

• label : String

  Descriptive label

• reference : String

  Section/example reference

• embeddedClauseType : MamClauseType

  Type of embedded clause

• matrixJudgment : MamExtractionJudgment

  =(y)a' status on the matrix predicate

• embeddedJudgment : MamExtractionJudgment

  =(y)a' status on the embedded predicate

@[implicit_reducible]

instance Mam.instReprMamLongDistanceDatum : Repr MamLongDistanceDatum

Equations

• Mam.instReprMamLongDistanceDatum = { reprPrec := Mam.instReprMamLongDistanceDatum.repr }

def Mam.instReprMamLongDistanceDatum.repr : MamLongDistanceDatum → ℕ → Std.Format

Equations

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

def Mam.ldFullCP : MamLongDistanceDatum

Long-distance extraction from full CP: =(y)a' licensed on BOTH matrix and embedded predicates. Table 4, Row 1; §6.2, ex. (38)–(39).

Equations

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

def Mam.ldAspectless : MamLongDistanceDatum

Long-distance extraction from aspectless clause: =(y)a' licensed on BOTH. Table 4, Row 2; §6.2.

Equations

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

def Mam.ldInfinitival : MamLongDistanceDatum

Long-distance extraction from infinitival: =(y)a' licensed on matrix but BLOCKED on embedded. Table 4, Row 3; §6.2, ex. (46).

Equations

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

def Mam.ldEmbeddedQuestion : MamLongDistanceDatum

Embedded question (1-step extraction): =(y)a' BLOCKED on matrix, licensed on embedded. Table 4, Row 4; §6.2, ex. (41).

Equations

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

def Mam.ldData : List MamLongDistanceDatum

All long-distance extraction data points (Table 4).

Equations

• Mam.ldData = [Mam.ldFullCP, Mam.ldAspectless, Mam.ldInfinitival, Mam.ldEmbeddedQuestion]

Per-datum verification

theorem Mam.trans_obl_licensed : transOblExtraction.judgment = MamExtractionJudgment.licensed

theorem Mam.trans_subj_blocked : transSubjExtraction.judgment = MamExtractionJudgment.blocked

theorem Mam.trans_obj_blocked : transObjExtraction.judgment = MamExtractionJudgment.blocked

theorem Mam.passive_obl_licensed : passiveOblExtraction.judgment = MamExtractionJudgment.licensed

theorem Mam.temporal_obl_blocked : temporalOblExtraction.judgment = MamExtractionJudgment.blocked

Generalizations

theorem Mam.eqya_iff_voice_and_oblique : (monoData.all fun (d : MamExtractionDatum) => (d.clauseType.projectsVoice && d.obliqueExtracted && !d.isTemporal) == (d.judgment == MamExtractionJudgment.licensed)) = true

Core generalization (monoclausal): =(y)a' is licensed iff the clause projects Voice AND a non-temporal oblique is extracted.

The !d.isTemporal conjunct is a stipulation — the paper does not explain why temporal obliques are exempt (§8.1). It is separated out as a distinct condition rather than hidden in obliqueExtracted.

theorem Mam.ld_embedded_tracks_voice : (ldData.all fun (d : MamLongDistanceDatum) => d.embeddedClauseType.projectsVoice == (d.embeddedJudgment == MamExtractionJudgment.licensed)) = true

Multiple spellout: in long-distance extraction, =(y)a' is licensed on each predicate whose clause projects Voice. Matrix clause always projects Voice (it's a full CP).

theorem Mam.eqya_tracks_oblique_not_extraction : transSubjExtraction.clauseType = transOblExtraction.clauseType ∧ transObjExtraction.clauseType = transOblExtraction.clauseType ∧ transSubjExtraction.judgment = MamExtractionJudgment.blocked ∧ transObjExtraction.judgment = MamExtractionJudgment.blocked ∧ transOblExtraction.judgment = MamExtractionJudgment.licensed

=(y)a' tracks oblique, not extraction in general: subject and object extraction in the same clause size do not trigger =(y)a'.

theorem Mam.temporal_is_oblique_but_exempt : temporalOblExtraction.obliqueExtracted = true ∧ temporalOblExtraction.isTemporal = true ∧ temporalOblExtraction.judgment = MamExtractionJudgment.blocked

Temporal obliques are genuine obliques that undergo genuine extraction, but are exempt from =(y)a' marking. This is an open question.

Island sensitivity

structure Mam.MovementReflex : Type

A morphological reflex of Ā-movement inherits movement's locality: since Ā-movement is phase-bounded (Phase Impenetrability Condition, Phase.lean), any morpheme requiring movement through a probe's specifier is island-sensitive. Deriving island sensitivity from these two properties replaces a stipulated Bool ([Cho00] on PIC; [ETB26] §7.1).

• requiresMovement : Bool

  Spellout of features valued via Agree with an Ā-moved constituent (Agree analysis, §5).

• movementPhaseBounded : Bool

  Movement is phase-bounded (PIC, Phase.lean); islands are configurations where the phase edge is unavailable.

@[implicit_reducible]

instance Mam.instDecidableEqMovementReflex : DecidableEq MovementReflex

Equations

• Mam.instDecidableEqMovementReflex = Mam.instDecidableEqMovementReflex.decEq

def Mam.instDecidableEqMovementReflex.decEq (x✝ x✝¹ : MovementReflex) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Mam.instReprMovementReflex : Repr MovementReflex

Equations

• Mam.instReprMovementReflex = { reprPrec := Mam.instReprMovementReflex.repr }

def Mam.instReprMovementReflex.repr : MovementReflex → ℕ → Std.Format

Equations

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

def Mam.MovementReflex.islandSensitive (mr : MovementReflex) : Bool

Island sensitivity is derived: a movement reflex is island-sensitive iff the morpheme requires movement AND movement is phase-bounded. No movement → no Agree → no spellout.

Equations

• mr.islandSensitive = (mr.requiresMovement && mr.movementPhaseBounded)

def Mam.eqyaMovementReflex : MovementReflex

=(y)a' is a movement reflex: it requires Ā-movement of the oblique through Spec,VoiceP (so Voice can Agree [uOblique]), and movement is phase-bounded (PIC).

Equations

• Mam.eqyaMovementReflex = { requiresMovement := true, movementPhaseBounded := true }

def Mam.eqyaIslandSensitive : Bool

Island sensitivity of =(y)a' follows from its being a movement reflex. Derived from requiresMovement ∧ movementPhaseBounded, not stipulated.

Equations

• Mam.eqyaIslandSensitive = Mam.eqyaMovementReflex.islandSensitive

theorem Mam.eqya_island_sensitive_derived : eqyaMovementReflex.islandSensitive = true

Proof that the derivation yields island sensitivity.

Against Agent Focus

theorem Mam.passive_oblique_cooccurrence : passiveOblExtraction.judgment = MamExtractionJudgment.licensed

=(y)a' co-occurs with passive morphology -njtz ([ETB26] §7.2, ex. (53)–(54)): passive is conditioned by Voice.Flavor and =(y)a' by [+oblique] features — independent fields in Voice.Head, so the flavor does not affect the features (structural derivation in MinimalismOblExtraction.eqya_not_agent_focus).

Extraction marking

inductive Mam.Extraction.Site : Type

Reflex hosts for SJA Mam extraction marking: the verb (AF suffixes) and the Voice/Dir head hosting =(y)a'.

• verb : Site
• voiceHead : Site

@[implicit_reducible]

instance Mam.Extraction.instDecidableEqSite : DecidableEq Site

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Mam.Extraction.instReprSite.repr Mam.Extraction.Site.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mam.Extraction.Site.verb")).group prec✝

@[implicit_reducible]

instance Mam.Extraction.instReprSite : Repr Site

Equations

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

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

SJA Mam marks two extraction cells. Subject (A) extraction switches the verb to AF ([Sco23] §2.5.4.1 ex. 169, §2.7.1), combining the antipassive suffix -(a)n with the AF-specific -ta (b'yo-n-ta 'hit-AP-AF') — morphologically distinct from K'iche''s bare antipassive -n ([Mon17] Lesson 22); the SSAL-repair analysis lives in Studies/Erlewine2016.lean, and rival accounts are not encoded here. Oblique extraction places =(y)a' on the Voice/Dir head — conditioned by clause size, exempting temporal obliques (§8.1), island-sensitive (§7.1). Core-object extraction is unmarked.

Equations

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

def Mam.Extraction.strategy : Extraction.ExtractionMarkingStrategy

WALS-style label: dedicated morphemes mark extraction.

Equations

• Mam.Extraction.strategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme

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

theorem Mam.Extraction.eqya_not_on_subject : Features.Reflex.morpheme Site.voiceHead ∉ realize Extraction.ExtractionTarget.subject

=(y)a' tracks obliques, not subjects: no voice-head reflex under subject extraction (subject marking is verb-hosted AF instead).