Documentation

Linglib.Fragments.Kaqchikel.Agreement

Kaqchikel Agreement Fragment @cite{preminger-2014} #

Agreement morphology for Kaqchikel (K'ichean, Mayan), formalizing @cite{preminger-2014} Agreement and Its Failures, Chapters 3-4 and @cite{chomsky-2001} @cite{scott-2023} @cite{blake-1994} Appendix 9.A.

The System #

Kaqchikel has two agreement paradigms on the verb:

Set A (ERG): prefixes on Voice/v cross-referencing the transitive agent
Set B (ABS): preverbal markers on Infl/T cross-referencing the absolutive argument (transitive patient or intransitive S)

Morpheme order on the verb (276): aspect - ABS - ERG - stem. Set B (ABS) precedes Set A (ERG).

Position	Case	Agreement
A (transitive agent)	ERG	Set A
P (transitive patient)	ABS	Set B
S (intransitive subj)	ABS	Set B

Unlike Mam, where Infl's φ-probe is blocked in transitives and the patient goes unagreed, Kaqchikel cross-references both transitive arguments (@cite{preminger-2014}, Ch. 3 vs. @cite{scott-2023} for Mam).

Agent Focus Agreement (@cite{preminger-2014}, §3.3, table 22) #

In AF constructions (clause-local agent extraction), the normal two-slot agreement collapses to a single marker drawn from the absolutive (Set B) paradigm. The target is chosen by an omnivorous hierarchy:

[+participant] > [+plural] > default (3SG = ∅)

The probe does not distinguish subject from object — AF agreement is commutative: ⟨1SG subj, 3SG obj⟩ = ⟨3SG subj, 1SG obj⟩ → in-. This follows from Preminger's analysis: the probe (π⁰) seeks the closest [+participant]-bearing DP regardless of its thematic role.

Person Restriction (@cite{preminger-2014}, (25)) #

At most one core argument can bear [+participant]. Combinations like ⟨1SG, 2SG⟩ are ungrammatical regardless of subject/object assignment.

Feature Geometry (@cite{preminger-2014}, §4.3, (55)) #

Person features decompose as:

[φ] → [PERSON] → [participant] → [author]
[φ] → [NUMBER] → [plural]

Two probes in the AF clause:

π⁰: seeks [participant], triggers clitic doubling of full φ-set
#⁰: seeks [plural], triggers number agreement

Obligatory Operations #

Preminger's central theoretical claim: φ-agreement is obligatory — the grammar must attempt it — but can fail without crashing. When the probe finds no suitable goal, no agreement obtains and a default (3SG = ∅) surfaces. This contrasts with the standard Minimalist view where unvalued features cause the derivation to crash.

inductive Fragments.Kaqchikel.PersonNumber :

Person-number combinations for Kaqchikel agreement paradigms. Six cells: three persons × two numbers.

Instances For

instance Fragments.Kaqchikel.instDecidableEqPersonNumber :

DecidableEq PersonNumber

Equations

Fragments.Kaqchikel.instDecidableEqPersonNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Kaqchikel.instBEqPersonNumber.beq :

PersonNumber → PersonNumber → Bool

Equations

Fragments.Kaqchikel.instBEqPersonNumber.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Kaqchikel.instBEqPersonNumber :

BEq PersonNumber

Equations

Fragments.Kaqchikel.instBEqPersonNumber = { beq := Fragments.Kaqchikel.instBEqPersonNumber.beq }

instance Fragments.Kaqchikel.instReprPersonNumber :

Repr PersonNumber

Equations

Fragments.Kaqchikel.instReprPersonNumber = { reprPrec := Fragments.Kaqchikel.instReprPersonNumber.repr }

def Fragments.Kaqchikel.instReprPersonNumber.repr :

PersonNumber → ℕ → Std.Format

Equations

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

Instances For

def Fragments.Kaqchikel.personNumbers :

List PersonNumber

All six person-number values.

Equations

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

Instances For

def Fragments.Kaqchikel.PersonNumber.isPlural :

PersonNumber → Bool

Is this person-number [+plural]?

Equations

Instances For

def Fragments.Kaqchikel.PersonNumber.isParticipant (pn : PersonNumber) :

Is this person-number [+participant]? Derived from the feature geometry in PersonGeometry.lean (@cite{preminger-2014}, §4.3, (55)): [participant] ⊂ [PERSON] ⊂ [φ].

Equations

pn.isParticipant = (Minimalism.decomposePerson pn.person).hasParticipant

Instances For

def Fragments.Kaqchikel.PersonNumber.isAuthor (pn : PersonNumber) :

Is this person-number [+author]? Derived from the feature geometry: [author] ⊂ [participant] ⊂ [PERSON].

Equations

pn.isAuthor = (Minimalism.decomposePerson pn.person).hasAuthor

Instances For

def Fragments.Kaqchikel.PersonNumber.toPhiFeatures :

PersonNumber → List Minimalism.PhiFeature

Convert to PhiFeature list for the Agree infrastructure.

Equations

Instances For

def Fragments.Kaqchikel.setAExponent :

PersonNumber → String

Set A (ERG) markers: prefixes on Voice/v cross-referencing the transitive agent (@cite{preminger-2014}, Ch. 3, table (29)). Parenthesized segments are dropped in certain phonological contexts; the grapheme j represents a voiceless velar fricative.

Equations

Instances For

def Fragments.Kaqchikel.setAVocab :

Minimalism.Vocabulary

Set A as Vocabulary entries for Spellout, contextualized to Voice/v.

Equations

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

Instances For

def Fragments.Kaqchikel.setBExponent :

PersonNumber → String

Set B (ABS) markers: preverbal markers on Infl/T cross-referencing the absolutive argument. The 3SG form (∅) is also the Elsewhere entry — the default when no more specific entry matches, as in the failure case of obligatory agreement (Ch. 5).

Equations

Instances For

def Fragments.Kaqchikel.setBVocab :

Minimalism.Vocabulary

Set B as Vocabulary entries for Spellout, contextualized to Infl/T.

Equations

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

Instances For

inductive Fragments.Kaqchikel.KaqArgPosition :

Argument positions in a Kaqchikel clause.

agent : KaqArgPosition
A: transitive agent (external argument, Spec,vP → Spec,TP)
patient : KaqArgPosition
P: transitive patient (internal argument, complement of V)
intranS : KaqArgPosition
S: intransitive subject (sole argument)

Instances For

instance Fragments.Kaqchikel.instDecidableEqKaqArgPosition :

DecidableEq KaqArgPosition

Equations

Fragments.Kaqchikel.instDecidableEqKaqArgPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Kaqchikel.instBEqKaqArgPosition :

BEq KaqArgPosition

Equations

Fragments.Kaqchikel.instBEqKaqArgPosition = { beq := Fragments.Kaqchikel.instBEqKaqArgPosition.beq }

def Fragments.Kaqchikel.instBEqKaqArgPosition.beq :

KaqArgPosition → KaqArgPosition → Bool

Equations

Fragments.Kaqchikel.instBEqKaqArgPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Kaqchikel.instReprKaqArgPosition :

Repr KaqArgPosition

Equations

Fragments.Kaqchikel.instReprKaqArgPosition = { reprPrec := Fragments.Kaqchikel.instReprKaqArgPosition.repr }

def Fragments.Kaqchikel.instReprKaqArgPosition.repr :

KaqArgPosition → ℕ → Std.Format

Equations

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

Instances For

def Fragments.Kaqchikel.KaqArgPosition.case :

KaqArgPosition → Minimalism.CaseVal

Case assignment: ergative-absolutive alignment. Agent gets ERG (from Voice/v); patient and intranS both get ABS (from Infl/T).

Equations

Instances For

def Fragments.Kaqchikel.KaqArgPosition.isPhiAgreed :

KaqArgPosition → Bool

Is this position φ-Agreed-with? In Kaqchikel, ALL three argument positions trigger agreement: agent via Set A on Voice/v, patient and intranS via Set B on Infl/T. This contrasts with Mam, where the patient is NOT agreed with (Infl's probe is blocked by VoiceP; @cite{scott-2023}).

Equations

Instances For

def Fragments.Kaqchikel.KaqArgPosition.agreeProbe :

KaqArgPosition → Minimalism.Cat

Which head agrees with this position?

Equations

Instances For

def Fragments.Kaqchikel.kaqArgPositions :

List KaqArgPosition

The three argument positions.

Equations

Fragments.Kaqchikel.kaqArgPositions = [Fragments.Kaqchikel.KaqArgPosition.agent , Fragments.Kaqchikel.KaqArgPosition.patient , Fragments.Kaqchikel.KaqArgPosition.intranS ]

Instances For

def Fragments.Kaqchikel.PersonNumber.afRank (pn : PersonNumber) :

The omnivorous agreement hierarchy for AF.

Derived from probeResolutionRank (PersonGeometry.lean), which computes rank from the two-probe system:

Rank 2: visible to π⁰ ([+participant])
Rank 1: visible to #⁰ only ([+plural, −participant])
Rank 0: invisible to both probes (3SG, default/Elsewhere)

The hierarchy is not stipulated — it follows from the feature geometry and the probe targets.

Equations

pn.afRank = Minimalism.probeResolutionRank pn.person pn.isPlural

Instances For

def Fragments.Kaqchikel.personRestrictionOk (subj obj : PersonNumber) :

Person restriction (@cite{preminger-2014}, (25)): at most one core argument can be [+participant]. Returns true if the combination is licit.

Equations

Fragments.Kaqchikel.personRestrictionOk subj obj = !(subj.isParticipant && obj.isParticipant)

Instances For

def Fragments.Kaqchikel.afAgreementTarget (subj obj : PersonNumber) :

Option PersonNumber

Compute the AF agreement target: whichever argument has the higher rank in the omnivorous hierarchy. When both have the same rank, the subject is chosen (both yield the same marker, so the choice is observationally inert). Returns none if the person restriction is violated.

Equations

Fragments.Kaqchikel.afAgreementTarget subj obj = if (!Fragments.Kaqchikel.personRestrictionOk subj obj) = true then none else if subj.afRank ≥ obj.afRank then some subj else some obj

Instances For

def Fragments.Kaqchikel.afMarker (subj obj : PersonNumber) :

The AF agreement marker for a given subject-object combination. Returns the Set B exponent of the omnivorous target, or none if the person restriction is violated.

Equations

Fragments.Kaqchikel.afMarker subj obj = Option.map Fragments.Kaqchikel.setBExponent (Fragments.Kaqchikel.afAgreementTarget subj obj)

Instances For

structure Fragments.Kaqchikel.AFAgreementDatum :

An AF agreement datum: subject φ, object φ, and the resulting single agreement marker (or none for person-restriction violations).

subject : PersonNumber
object : PersonNumber
marker : Option String

Instances For

def Fragments.Kaqchikel.instReprAFAgreementDatum.repr :

AFAgreementDatum → ℕ → Std.Format

Equations

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

Instances For

instance Fragments.Kaqchikel.instReprAFAgreementDatum :

Repr AFAgreementDatum

Equations

Fragments.Kaqchikel.instReprAFAgreementDatum = { reprPrec := Fragments.Kaqchikel.instReprAFAgreementDatum.repr }

def Fragments.Kaqchikel.afParadigm :

List AFAgreementDatum

The empirical AF agreement paradigm (@cite{preminger-2014}, table (22)). Each row records the observed agreement marker for a given subject-object combination in clause-local agent extraction.

The first 11 rows reproduce the paper's table exactly. Rows 12–15 demonstrate commutativity (§3.2, fn. a): the table uses set notation {φ₁, φ₂}, so swapping subj/obj yields the same marker. Rows 16–17 test person restriction violations ((25)).

Equations

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

Instances For

def Fragments.Kaqchikel.VerbForm.agreementSlots :

VerbForm → ℕ

Number of agreement slots for each verb form. Transitive: two slots (Set A + Set B). AF: one slot (single omnivorous marker from the ABS paradigm).

Equations

Instances For

inductive Fragments.Kaqchikel.AgreeOutcome :

The result of an obligatory agreement operation.

Preminger's key insight: the probe must attempt to Agree (agreement is obligatory), but if it finds no suitable goal, the derivation does NOT crash — it continues with the probe's features unvalued, and the Elsewhere vocabulary entry (3SG ∅) surfaces at PF.

success : PersonNumber → AgreeOutcome
Probe successfully valued by a goal's φ-features.
failure : AgreeOutcome
Probe attempted but found no suitable goal; default surfaces.

Instances For

instance Fragments.Kaqchikel.instDecidableEqAgreeOutcome :

DecidableEq AgreeOutcome

Equations

Fragments.Kaqchikel.instDecidableEqAgreeOutcome = Fragments.Kaqchikel.instDecidableEqAgreeOutcome.decEq

def Fragments.Kaqchikel.instBEqAgreeOutcome.beq :

AgreeOutcome → AgreeOutcome → Bool

Equations

Instances For

instance Fragments.Kaqchikel.instBEqAgreeOutcome :

BEq AgreeOutcome

Equations

Fragments.Kaqchikel.instBEqAgreeOutcome = { beq := Fragments.Kaqchikel.instBEqAgreeOutcome.beq }

instance Fragments.Kaqchikel.instReprAgreeOutcome :

Repr AgreeOutcome

Equations

Fragments.Kaqchikel.instReprAgreeOutcome = { reprPrec := Fragments.Kaqchikel.instReprAgreeOutcome.repr }

def Fragments.Kaqchikel.instReprAgreeOutcome.repr :

AgreeOutcome → ℕ → Std.Format

Equations

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

Instances For

def Fragments.Kaqchikel.AgreeOutcome.exponent :

AgreeOutcome → String

The morphological exponent for an agreement outcome. Success: Set B form of the agreed-with argument. Failure: Elsewhere entry (3SG ∅).

Equations

Instances For

theorem Fragments.Kaqchikel.failed_agreement_is_3sg :

AgreeOutcome.failure.exponent = setBExponent PersonNumber.p3sg

Failed agreement surfaces as 3SG — the Elsewhere entry.

theorem Fragments.Kaqchikel.agent_case :

KaqArgPosition.agent.case = Minimalism.CaseVal.erg

Agent gets ERG (from Voice).

theorem Fragments.Kaqchikel.patient_case :

KaqArgPosition.patient.case = Minimalism.CaseVal.abs

Patient gets ABS (from Infl).

theorem Fragments.Kaqchikel.intranS_case :

KaqArgPosition.intranS.case = Minimalism.CaseVal.abs

Intransitive S gets ABS (from Infl).

theorem Fragments.Kaqchikel.erg_abs_alignment :

KaqArgPosition.agent.case ≠ KaqArgPosition.patient.case ∧ KaqArgPosition.patient.case = KaqArgPosition.intranS.case

Ergative-absolutive alignment: the agent is distinguished (ERG) while patient and intranS share a case value (ABS).

theorem Fragments.Kaqchikel.all_positions_agreed :

(kaqArgPositions.all fun (p : KaqArgPosition) => p.isPhiAgreed) = true

All three argument positions trigger φ-agreement.

theorem Fragments.Kaqchikel.author_entails_participant :

(personNumbers.all fun (pn : PersonNumber) => if pn.isAuthor = true then pn.isParticipant else true) = true

[+author] entails [+participant] (@cite{preminger-2014}, (55)): [author] ⊂ [participant] in the feature geometry.

theorem Fragments.Kaqchikel.third_not_participant :

PersonNumber.p3sg.isParticipant = false ∧ PersonNumber.p3pl.isParticipant = false

3rd person is [-participant].

theorem Fragments.Kaqchikel.af_rank_grounded :

PersonNumber.p1sg.afRank = 2 ∧ PersonNumber.p2sg.afRank = 2 ∧ PersonNumber.p3pl.afRank = 1 ∧ PersonNumber.p3sg.afRank = 0

The AF hierarchy is grounded in the two-probe system: person-number values that bear [+participant] get rank 2 (visible to π⁰), 3PL gets rank 1 (visible to #⁰ only), and 3SG gets rank 0.

isParticipant is derived from decomposePerson, not stipulated. Verify it gives the expected values.

theorem Fragments.Kaqchikel.af_paradigm_correct :

(afParadigm.all fun (d : AFAgreementDatum) => afMarker d.subject d.object == d.marker) = true

The entire AF paradigm (table 22) is correctly predicted by the omnivorous hierarchy computation. Each empirical datum matches the output of afMarker.

theorem Fragments.Kaqchikel.af_commutative :

(personNumbers.all fun (s : PersonNumber) => personNumbers.all fun (o : PersonNumber) => afMarker s o == afMarker o s) = true

AF agreement is commutative: swapping subject and object yields the same marker for ALL person-number combinations (@cite{preminger-2014}, §3.3, (67)). This follows from the omnivorous hierarchy — the probe sees both arguments symmetrically.

theorem Fragments.Kaqchikel.participant_over_plural :

afMarker PersonNumber.p1sg PersonNumber.p3pl = some "in-" ∧ afMarker PersonNumber.p3pl PersonNumber.p2sg = some "at-"

[+participant] outranks [+plural]: when one argument is 1st/2nd person and the other is 3PL, the marker reflects the participant, not the plural.

theorem Fragments.Kaqchikel.person_restriction_blocks :

afMarker PersonNumber.p1sg PersonNumber.p2sg = none ∧ afMarker PersonNumber.p2sg PersonNumber.p1sg = none

Person restriction blocks two [+participant] arguments.

theorem Fragments.Kaqchikel.person_restriction_symmetric :

(personNumbers.all fun (s : PersonNumber) => personNumbers.all fun (o : PersonNumber) => personRestrictionOk s o == personRestrictionOk o s) = true

Person restriction is symmetric.

theorem Fragments.Kaqchikel.default_3sg :

afMarker PersonNumber.p3sg PersonNumber.p3sg = some "∅"

Default 3SG: when both arguments are 3SG, the Elsewhere entry (∅) surfaces — the least specified vocabulary item.

theorem Fragments.Kaqchikel.af_single_slot :

VerbForm.agentFocus.agreementSlots = 1

AF has a single agreement slot (one marker from the ABS paradigm).

theorem Fragments.Kaqchikel.trans_dual_slots :

VerbForm.transitive.agreementSlots = 2

Transitive has dual agreement slots (Set A + Set B).

theorem Fragments.Kaqchikel.af_no_ergative :

VerbForm.agentFocus.hasSetA = false ∧ VerbForm.agentFocus.agreementSlots = 1

AF loses ergative (Set A) agreement: the single AF marker is drawn from the absolutive paradigm, not the ergative. Cross-references VerbForm.hasSetA from AgentFocus.lean.

theorem Fragments.Kaqchikel.trans_has_ergative :

VerbForm.transitive.hasSetA = true ∧ VerbForm.transitive.agreementSlots = 2

Transitive retains ergative (Set A) agreement.

def Fragments.Kaqchikel.caseInventory :

Kaqchikel case inventory, derived from argument position case values.

Equations

Fragments.Kaqchikel.caseInventory = [Core.Case.erg , Core.Case.abs ]

Instances For

theorem Fragments.Kaqchikel.inventory_covers_positions :

(kaqArgPositions.all fun (p : KaqArgPosition) => caseInventory.any fun (x : Core.Case) => x == p.case.toCase) = true

The inventory covers all argument positions: every position's case is in the inventory.

theorem Fragments.Kaqchikel.inventory_valid :

Core.validInventory caseInventory = true

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