Mam Agreement Fragment @cite{scott-2023}

@cite{deal-2024} @cite{woolford-1997} @cite{blake-1994}

Agreement morphology and pronoun realization data for San Juan Atitán (SJA) Mam, a Mayan language with morphologically tripartite agreement alignment: S, A, and O each trigger distinct marking patterns on the verb.

The System

Mam has two agreement paradigms on the verb:

• Set A (ERG): prefixes on Voice cross-referencing the transitive agent
• Set B (ABS): preverbal markers on Infl cross-referencing the absolutive argument (intransitive S). In transitives, Infl's φ-probe is blocked by transitive VoiceP and default Set B (∅/tz'=) appears instead.

In the default construction, transitive objects are not cross-referenced by either set — they co-occur with default Set B (tz'=) and require full overt pronouns. However, some speakers accept agreeing Set B for objects as a more formal variant (@cite{scott-2023}, ch. 3, ex. 156).

Case Licensing

Case is NOT assigned via dependent case. Instead:

• ERG: inherent case from Voice
• ACC: structural case from Voice (object licensing; low-abs syntax)
• ABS: structural case from Infl (high-abs morphology; for intransitive S)

This gives a tripartite underlying Case system (ERG, ACC, ABS) despite Mam having no independent case morphology on DPs — case is visible only through agreement patterns.

Argument Positions

Position	Case	Agreement	Pronoun
A (transitive agent)	ERG (from Voice)	Set A	reduced/null
S (intransitive subj)	ABS (from Infl)	Set B	reduced/null
P (transitive patient)	ACC (from Voice)	default Set B	overt

def Fragments.Mayan.Mam.setAMarkers : List (Core.Prominence.PersonLevel × Bool × String)

Set A (ERG) markers: prefixes/proclitics on the verb that cross-reference the transitive agent (@cite{scott-2023}, Table 2.8).

Equations

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

def Fragments.Mayan.Mam.setBMarkers : List (Core.Prominence.PersonLevel × Bool × String)

Set B (ABS) markers: preverbal markers on Infl that cross-reference the absolutive argument (@cite{scott-2023}, Table 3.5). The 2/3SG form tz'= is the default — it appears both for real agreement with a 2/3SG intransitive S and for default Set B in transitives when Infl's probe is blocked by VoiceP. 1SG = chin, 2SG = tz'=, 3SG = tz'=, 1PL = qo, 2PL = chi, 3PL = chi.

Equations

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

def Fragments.Mayan.Mam.defaultSetB : String

The default (Elsewhere) Set B marker. Surfaces in transitives when Infl's probe is blocked, and also for 2/3SG intransitive S.

Equations

• Fragments.Mayan.Mam.defaultSetB = "tz'="

def Fragments.Mayan.Mam.lookupMarker (markers : List (Core.Prominence.PersonLevel × Bool × String)) (person : Core.Prominence.PersonLevel) (sg : Bool) : Option String

Look up a marker by person and number (true = singular).

Equations

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

inductive Fragments.Mayan.Mam.MamArgPosition : Type

Argument positions in a Mam clause (@cite{scott-2023}, ch. 3).

• agent : MamArgPosition
• patient : MamArgPosition
• intranS : MamArgPosition

instance Fragments.Mayan.Mam.instDecidableEqMamArgPosition : DecidableEq MamArgPosition

Equations

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

instance Fragments.Mayan.Mam.instBEqMamArgPosition : BEq MamArgPosition

Equations

• Fragments.Mayan.Mam.instBEqMamArgPosition = { beq := Fragments.Mayan.Mam.instBEqMamArgPosition.beq }

def Fragments.Mayan.Mam.instBEqMamArgPosition.beq : MamArgPosition → MamArgPosition → Bool

Equations

• Fragments.Mayan.Mam.instBEqMamArgPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Mam.instReprMamArgPosition : Repr MamArgPosition

Equations

• Fragments.Mayan.Mam.instReprMamArgPosition = { reprPrec := Fragments.Mayan.Mam.instReprMamArgPosition.repr }

def Fragments.Mayan.Mam.instReprMamArgPosition.repr : MamArgPosition → Nat → Std.Format

Equations

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

def Fragments.Mayan.Mam.MamArgPosition.case : MamArgPosition → Core.Case

The case each argument position receives. A gets ERG (inherent, from Voice), P gets ACC (structural, from Voice), S gets ABS (structural, from Infl). Three distinct underlying cases.

Equations

• Fragments.Mayan.Mam.MamArgPosition.agent.case = Core.Case.erg
• Fragments.Mayan.Mam.MamArgPosition.patient.case = Core.Case.acc
• Fragments.Mayan.Mam.MamArgPosition.intranS.case = Core.Case.abs

def Fragments.Mayan.Mam.MamArgPosition.isPhiAgreed : MamArgPosition → Bool

Is this argument position φ-Agreed-with by some probe?

Agent: Voice probes for φ, finds agent in Spec,VoiceP → Set A Intransitive S: Infl probes for φ, finds S → Set B Patient: Infl's φ-probe has a disjunctive satisfaction condition [SAT: φ or Voice_TR]. In transitives, the probe encounters transitive Voice and stops — no φ-features are copied, and default Set B (the Elsewhere form) surfaces.

Equations

• Fragments.Mayan.Mam.MamArgPosition.agent.isPhiAgreed = true
• Fragments.Mayan.Mam.MamArgPosition.patient.isPhiAgreed = false
• Fragments.Mayan.Mam.MamArgPosition.intranS.isPhiAgreed = true

def Fragments.Mayan.Mam.MamArgPosition.canBeReduced (pos : MamArgPosition) : Bool

Can a pronoun in this argument position undergo reduction?

Scott's analysis (ch. 4, §4.4.3): first person pronouns in agreed-with positions are reduced via an impoverishment rule that deletes [±singular] in the context of [+author]^F (where F marks that the feature has been agreed with). This bleeds insertion of the pronominal base morphemes qin ([+author,+singular]) and qo ([+author,-singular]), leaving only the disagreement enclitic =i.

Non-first person pronouns are NOT reduced — their subj/poss forms are identical to their independent forms (Table 4.25, p. 200). Whether actual reduction occurs depends on person (see derivePronounForm), but only agreed-with positions are eligible.

Equations

• pos.canBeReduced = pos.isPhiAgreed

def Fragments.Mayan.Mam.mamArgPositions : List MamArgPosition

The three argument positions.

Equations

• Fragments.Mayan.Mam.mamArgPositions = [Fragments.Mayan.Mam.MamArgPosition.agent, Fragments.Mayan.Mam.MamArgPosition.patient, Fragments.Mayan.Mam.MamArgPosition.intranS]

theorem Fragments.Mayan.Mam.agent_case : MamArgPosition.agent.case = Core.Case.erg

Agent gets ERG (inherent, from Voice).

theorem Fragments.Mayan.Mam.patient_case : MamArgPosition.patient.case = Core.Case.acc

Patient gets ACC (structural, from Voice).

theorem Fragments.Mayan.Mam.intranS_case : MamArgPosition.intranS.case = Core.Case.abs

Intransitive S gets ABS (structural, from Infl).

theorem Fragments.Mayan.Mam.tripartite : MamArgPosition.agent.case ≠ MamArgPosition.patient.case ∧ MamArgPosition.agent.case ≠ MamArgPosition.intranS.case ∧ MamArgPosition.patient.case ≠ MamArgPosition.intranS.case

Three distinct underlying cases — morphologically tripartite.

theorem Fragments.Mayan.Mam.reduction_eligible_iff_phi_agreed : (mamArgPositions.all fun (pos : MamArgPosition) => pos.canBeReduced == pos.isPhiAgreed) = true

Reduction eligibility correlates with φ-agreement: an argument position is eligible for pronoun reduction iff it triggers agreement on the verb. (Actual reduction further requires [+author]; see derivePronounForm.)

def Fragments.Mayan.Mam.caseInventory : List Core.Case

Mam case inventory, derived from argument position case values.

Equations

• Fragments.Mayan.Mam.caseInventory = [Core.Case.erg, Core.Case.acc, Core.Case.abs]

theorem Fragments.Mayan.Mam.inventory_covers_positions : (mamArgPositions.all fun (p : MamArgPosition) => caseInventory.any fun (x : Core.Case) => x == p.case) = true

The inventory covers all argument positions.

theorem Fragments.Mayan.Mam.inventory_valid : Core.validInventory caseInventory = true

Mam's {ERG, ACC, ABS} inventory is valid per Blake's case hierarchy (all are core cases at rank 6, trivially no gaps).

inductive Fragments.Mayan.Mam.PersonFeature : Type

Person features relevant for pronoun reduction.

Scott decomposes person into binary features following @cite{harbour-2016} (Table 4.3-4.4):

• [±author]: distinguishes 1st from non-1st
• [±participant]: distinguishes local (1st/2nd) from 3rd

Agreement (Set A and Set B) copies only [±author] and ±singular (Tables 4.7-4.8). It does NOT copy [±participant].

The =i enclitic is the disagreement enclitic — it realizes disagreeing values of [±author] and [±participant] (ex. 59, adapting @cite{noyer-1992} / @cite{harbour-2016}):

• 1SG/1PL.EXCL: [+author, -participant] → disagree → =i
• 2SG/2PL: [-author, +participant] → disagree → =i
• 1PL.INCL: [+author, +participant] → agree → no =i
• 3SG/3PL: [-author, -participant] → agree → no =i

• person : PersonFeature
• number : PersonFeature
• participant : PersonFeature

instance Fragments.Mayan.Mam.instDecidableEqPersonFeature : DecidableEq PersonFeature

Equations

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

def Fragments.Mayan.Mam.instBEqPersonFeature.beq : PersonFeature → PersonFeature → Bool

Equations

• Fragments.Mayan.Mam.instBEqPersonFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Mam.instBEqPersonFeature : BEq PersonFeature

Equations

• Fragments.Mayan.Mam.instBEqPersonFeature = { beq := Fragments.Mayan.Mam.instBEqPersonFeature.beq }

instance Fragments.Mayan.Mam.instReprPersonFeature : Repr PersonFeature

Equations

• Fragments.Mayan.Mam.instReprPersonFeature = { reprPrec := Fragments.Mayan.Mam.instReprPersonFeature.repr }

def Fragments.Mayan.Mam.instReprPersonFeature.repr : PersonFeature → Nat → Std.Format

Equations

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

def Fragments.Mayan.Mam.baseFeatures : List PersonFeature

The pronominal base morpheme's features.

Equations

• Fragments.Mayan.Mam.baseFeatures = [Fragments.Mayan.Mam.PersonFeature.person, Fragments.Mayan.Mam.PersonFeature.number]

def Fragments.Mayan.Mam.encliticFeature : PersonFeature

The =i enclitic's feature: [participant].

Equations

• Fragments.Mayan.Mam.encliticFeature = Fragments.Mayan.Mam.PersonFeature.participant

def Fragments.Mayan.Mam.agreedFeatures : List PersonFeature

Features that agreement morphology copies (person and number only).

Equations

• Fragments.Mayan.Mam.agreedFeatures = [Fragments.Mayan.Mam.PersonFeature.person, Fragments.Mayan.Mam.PersonFeature.number]

def Fragments.Mayan.Mam.isRedundant (f : PersonFeature) : Bool

A feature is redundantly expressed by agreement iff agreement copies it.

Equations

• Fragments.Mayan.Mam.isRedundant f = Fragments.Mayan.Mam.agreedFeatures.any fun (x : Fragments.Mayan.Mam.PersonFeature) => x == f

def Fragments.Mayan.Mam.allRedundant (feats : List PersonFeature) : Bool

A morpheme is deleted when ALL its features are redundantly expressed by agreement.

Equations

• Fragments.Mayan.Mam.allRedundant feats = feats.all Fragments.Mayan.Mam.isRedundant

theorem Fragments.Mayan.Mam.base_is_redundant : allRedundant baseFeatures = true

The pronominal base is deleted: [person, number] are both copied by agreement, making the base fully redundant.

theorem Fragments.Mayan.Mam.enclitic_survives : isRedundant encliticFeature = false

The =i enclitic survives: [participant] is NOT copied by agreement.

inductive Fragments.Mayan.Mam.PronounForm : Type

Pronoun realization after impoverishment (@cite{scott-2023}, §4.4.3).

• reduced: 1st person agreed-with — impoverishment deletes [±singular] in the context of [+author]^F, bleeding insertion of pronominal base morphemes qin/qo. Only =i remains.
• full: unreduced — the full independent pronoun form. This covers 2nd/3rd person subj/poss (which ARE identical to their independent forms, Table 4.25), as well as all object pronouns (which are not agreed-with and thus not eligible for reduction).

• reduced : PronounForm
• full : PronounForm

instance Fragments.Mayan.Mam.instDecidableEqPronounForm : DecidableEq PronounForm

Equations

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

def Fragments.Mayan.Mam.instBEqPronounForm.beq : PronounForm → PronounForm → Bool

Equations

• Fragments.Mayan.Mam.instBEqPronounForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Mam.instBEqPronounForm : BEq PronounForm

Equations

• Fragments.Mayan.Mam.instBEqPronounForm = { beq := Fragments.Mayan.Mam.instBEqPronounForm.beq }

instance Fragments.Mayan.Mam.instReprPronounForm : Repr PronounForm

Equations

• Fragments.Mayan.Mam.instReprPronounForm = { reprPrec := Fragments.Mayan.Mam.instReprPronounForm.repr }

def Fragments.Mayan.Mam.instReprPronounForm.repr : PronounForm → Nat → Std.Format

Equations

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

def Fragments.Mayan.Mam.isFirstPerson : Core.Prominence.PersonLevel → Bool

Is this person 1st (= [+author])? Only [+author] persons are eligible for the impoverishment rule (84) that deletes [±singular] and bleeds base morpheme insertion.

Equations

• Fragments.Mayan.Mam.isFirstPerson Core.Prominence.PersonLevel.first = true
• Fragments.Mayan.Mam.isFirstPerson x✝ = false

def Fragments.Mayan.Mam.derivePronounForm (pos : MamArgPosition) (person : Core.Prominence.PersonLevel) : PronounForm

Derive pronoun form from agreement status and person.

The impoverishment rule (ex. 84/94) targets [+author] features that bear the F diacritic (indicating agreement has occurred): [+/−singular] → ∅ / [+author]^F

This deletes [±singular] from 1st person agreed-with pronouns, bleeding insertion of qin ([+author,+singular]) and qo ([+author,−singular]). Only =i remains.

For 2nd/3rd person, the rule does not apply (they are [-author]), so their subj/poss forms equal their independent forms (Table 4.25). For unagreed-with positions (objects), there is no F diacritic, so impoverishment does not apply regardless of person.

Equations

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

theorem Fragments.Mayan.Mam.first_agent_reduced : derivePronounForm MamArgPosition.agent Core.Prominence.PersonLevel.first = PronounForm.reduced

1st person agent: reduced (base deleted, only =i remains).

theorem Fragments.Mayan.Mam.third_agent_full : derivePronounForm MamArgPosition.agent Core.Prominence.PersonLevel.third = PronounForm.full

3rd person agent: full independent form (impoverishment does not apply to [-author]).

theorem Fragments.Mayan.Mam.second_agent_full : derivePronounForm MamArgPosition.agent Core.Prominence.PersonLevel.second = PronounForm.full

2nd person agent: full independent form (=i IS the independent 2SG pronoun, not a reduction).

theorem Fragments.Mayan.Mam.first_patient_full : derivePronounForm MamArgPosition.patient Core.Prominence.PersonLevel.first = PronounForm.full

1st person patient: full pronoun (no agreement → no F diacritic).

theorem Fragments.Mayan.Mam.third_patient_full : derivePronounForm MamArgPosition.patient Core.Prominence.PersonLevel.third = PronounForm.full

3rd person patient: full pronoun (no agreement → no F diacritic).

theorem Fragments.Mayan.Mam.first_intranS_reduced : derivePronounForm MamArgPosition.intranS Core.Prominence.PersonLevel.first = PronounForm.reduced

1st person intransitive S: reduced (Set B agreement triggers impoverishment, deleting base).

theorem Fragments.Mayan.Mam.third_intranS_full : derivePronounForm MamArgPosition.intranS Core.Prominence.PersonLevel.third = PronounForm.full

3rd person intransitive S: full independent form.

theorem Fragments.Mayan.Mam.first_vs_nonfirst_asymmetry : derivePronounForm MamArgPosition.agent Core.Prominence.PersonLevel.first ≠ derivePronounForm MamArgPosition.agent Core.Prominence.PersonLevel.third ∧ derivePronounForm MamArgPosition.intranS Core.Prominence.PersonLevel.first ≠ derivePronounForm MamArgPosition.intranS Core.Prominence.PersonLevel.third

Key asymmetry: for agreed-with positions, 1st person is reduced while 2nd/3rd retain full independent forms. This follows from the impoverishment rule targeting [+author] only.

theorem Fragments.Mayan.Mam.patient_person_irrelevant : derivePronounForm MamArgPosition.patient Core.Prominence.PersonLevel.first = derivePronounForm MamArgPosition.patient Core.Prominence.PersonLevel.third

For unagreed-with positions, person is irrelevant: all get full pronouns.

def Fragments.Mayan.Mam.absPosition : ABSPosition

Mam is HIGH-ABS: Set B (absolutive) markers appear pre-stem on Infl, immediately following the aspect marker. Morpheme template: ASP-ABS-ERG-ROOT-SUFFIX (@cite{scott-2023}, §2.5.1).

Equations

• Fragments.Mayan.Mam.absPosition = Fragments.Mayan.ABSPosition.high

theorem Fragments.Mayan.Mam.mam_case_locus : toCaseLocus absPosition = CaseLocus.absNom

HIGH-ABS yields ABS=NOM case locus: Infl assigns case to the absolutive argument (@cite{scott-2023}, §3.3).

theorem Fragments.Mayan.Mam.setA_1sg : lookupMarker setAMarkers Core.Prominence.PersonLevel.first true = some "n-/w-"

Set A 1SG marker.

theorem Fragments.Mayan.Mam.setA_3sg : lookupMarker setAMarkers Core.Prominence.PersonLevel.third true = some "t-"

Set A 3SG marker is "t-" (the default).

theorem Fragments.Mayan.Mam.setB_1sg : lookupMarker setBMarkers Core.Prominence.PersonLevel.first true = some "chin"

Set B 1SG marker is "chin".

theorem Fragments.Mayan.Mam.setB_3sg : lookupMarker setBMarkers Core.Prominence.PersonLevel.third true = some defaultSetB

Set B 3SG marker is the default "tz'=".