Mam Agreement Fragment @cite{scott-2023}

@cite{deal-2021} @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.

Crucially, transitive objects are NOT cross-referenced by either set. Objects co-occur with default Set B and require full overt pronouns (@cite{scott-2023}, ch. 3–4).

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.Mam.setAVocab : Minimalism.Vocabulary

Set A (ERG) vocabulary entries: φ-features on Voice (mapped to.v) yield the morphological exponent. Set A markers are prefixes/proclitics 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.Mam.setBVocab : Minimalism.Vocabulary

Set B (ABS) vocabulary entries: φ-features on Infl (mapped to.T) yield the morphological exponent (@cite{scott-2023}, Table 3.5).

Crucially, the 2/3SG form (∅/tz'=) is the Elsewhere entry — it has no feature specification and is selected when no more specific entry matches. This is the form that appears both for (a) real agreement with a 2/3SG intransitive S and (b) default Set B in transitives when Infl's probe is blocked by VoiceP.

Equations

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

inductive Fragments.Mam.MamArgPosition : Type

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

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

instance Fragments.Mam.instDecidableEqMamArgPosition : DecidableEq MamArgPosition

Equations

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

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

Equations

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

instance Fragments.Mam.instBEqMamArgPosition : BEq MamArgPosition

Equations

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

def Fragments.Mam.instReprMamArgPosition.repr : MamArgPosition → ℕ → Std.Format

Equations

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

instance Fragments.Mam.instReprMamArgPosition : Repr MamArgPosition

Equations

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

def Fragments.Mam.MamArgPosition.case : MamArgPosition → Minimalism.CaseVal

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.Mam.MamArgPosition.agent.case = Minimalism.CaseVal.erg
• Fragments.Mam.MamArgPosition.patient.case = Minimalism.CaseVal.acc
• Fragments.Mam.MamArgPosition.intranS.case = Minimalism.CaseVal.abs

def Fragments.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.Mam.MamArgPosition.agent.isPhiAgreed = true
• Fragments.Mam.MamArgPosition.patient.isPhiAgreed = false
• Fragments.Mam.MamArgPosition.intranS.isPhiAgreed = true

def Fragments.Mam.MamArgPosition.agreeProbe : MamArgPosition → Option Minimalism.Cat

Which head φ-Agrees with this argument (if any)? Returns the category of the probe head. Voice is mapped to.v.

Equations

• Fragments.Mam.MamArgPosition.agent.agreeProbe = some Minimalism.Cat.v
• Fragments.Mam.MamArgPosition.patient.agreeProbe = none
• Fragments.Mam.MamArgPosition.intranS.agreeProbe = some Minimalism.Cat.T

def Fragments.Mam.MamArgPosition.canBeNull : MamArgPosition → Bool

Can a pronoun in this argument position be reduced (or null)?

Scott's analysis (ch. 4): when a pronoun's φ-features are redundantly expressed by agreement morphology on the verb, the pronominal base morpheme is deleted. For 2nd/3rd person, this yields a fully null pronoun. For 1st person, the disagreement enclitic =i remains (realizing [participant], which agreement does not copy).

This function captures the coarse generalization: agreed-with positions allow reduced/null pronouns; unagreed-with positions require full overt pronouns. The finer-grained 1st-person =i residue is not modeled here.

Equations

• Fragments.Mam.MamArgPosition.agent.canBeNull = true
• Fragments.Mam.MamArgPosition.patient.canBeNull = false
• Fragments.Mam.MamArgPosition.intranS.canBeNull = true

def Fragments.Mam.mamArgPositions : List MamArgPosition

The three argument positions.

Equations

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

theorem Fragments.Mam.agent_case : MamArgPosition.agent.case = Minimalism.CaseVal.erg

Agent gets ERG (inherent, from Voice).

theorem Fragments.Mam.patient_case : MamArgPosition.patient.case = Minimalism.CaseVal.acc

Patient gets ACC (structural, from Voice).

theorem Fragments.Mam.intranS_case : MamArgPosition.intranS.case = Minimalism.CaseVal.abs

Intransitive S gets ABS (structural, from Infl).

theorem Fragments.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.Mam.reduction_iff_phi_agreed : (mamArgPositions.all fun (pos : MamArgPosition) => pos.canBeNull == pos.isPhiAgreed) = true

Pronoun reduction correlates with φ-agreement: an argument position allows reduced/null pronouns iff it triggers agreement on the verb.

def Fragments.Mam.caseInventory : List Core.Case

Mam case inventory, derived from argument position case values.

Equations

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

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

The inventory covers all argument positions.

theorem Fragments.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).