Erlewine 2016: Anti-Locality and Optimality in Kaqchikel Agent Focus

[Erl16] [Erl18]

[Erl16] analyzes Kaqchikel Agent Focus as the optimal output of a competition between derivations, ranked by three violable constraints: XRef-Participant ≫ Spec-to-Spec Anti-Locality (SSAL) ≫ XRef (cross-referencing). The core two-candidate competition is decided by the SSAL ≫ XRef sub-ranking; top-ranked XRef-Participant produces the participant exception below. The fragment in Fragments/Mayan/Kaqchikel/Extraction.lean carries the typology-neutral extraction profile; this study file adds the theory-laden OT machinery and verifies the paper's results.

The Derivation ([Erl16] §§4–5)

Why the transitive derivation crashes

In a normal Kaqchikel transitive, the agent base-generates in Spec,vP and is attracted to Spec,TP by the A-probe on T (receiving Set A agreement). For Ā-extraction, the agent must then move from Spec,TP to Spec,CP. But CP immediately dominates TP, so this step crosses no intervening maximal projection — violating Spec-to-Spec Anti-Locality.

Why AF is selected

The grammar generates a competing candidate — the AF structure — with an intransitive-like v that does NOT introduce the agent in Spec,vP. The agent extracts directly to Spec,CP without passing through Spec,TP, so no SSAL violation occurs. But the agent never enters Spec,TP, so the A-probe cannot establish Set A (ergative) agreement — violating the lower-ranked XRef constraint.

The evaluation selects AF because SSAL ≫ XRef: avoiding the too-local movement outranks maintaining cross-referencing agreement.

Key insight: locality, not extraction per se

AF is triggered by the locality of movement, not by agent extraction per se. Two signatures ([Erl16] §§2.2, 3): intervening preverbal material lengthens the subject's movement and obviates AF — the full-agreement transitive resurfaces and AF becomes ungrammatical; and long-distance subject extraction places AF on the embedded verb, whose subject makes the too-local first step, while the matrix verb, whose own subject has not moved, must stay transitive.

Connection to Position.lean

The specToSpecAntiLocality predicate (Position.lean) formalizes the constraint that blocks the transitive derivation: movement from Spec,XP to Spec,YP is blocked when YP immediately dominates XP. In Kaqchikel, XP = TP and YP = CP. SSAL traces to [abels-2003]'s anti-locality theory, with refinements in [boskovic-1997] and many subsequent papers; [Erl16]'s contribution is the specific application to Kichean AF as an OT-competing-candidate analysis.

Connection to Constraint

The OT tableau uses the lexicographic comparison from Phonology/OptimalityTheory/Tableau.lean. The key result af_is_optimal shows that AF beats the transitive under strict ranking — and satisfaction_ordering_incomparable shows this requires OT's lexicographic comparison, not satisfaction ordering's subset inclusion.

Anti-agreement

AF is an instance of a broader cross-linguistic pattern of anti-agreement: when extraction forces a DP to skip an A-position (to avoid SSAL), the agreement morphology associated with that position is lost — Kaqchikel Set A under agent extraction, Trentino Italian nominative under extraction, Karitiâna absolutive under extraction. All derive from the same mechanism: SSAL forces skipping an A-position, and agreement with the head at that position fails.

Contrast with Toba Batak

Both Kaqchikel and Toba Batak have extraction restrictions derived from anti-locality in predicate-fronting contexts, but the repair strategies differ: Toba Batak restricts extraction to the pivot position (structural restriction), while Kaqchikel repairs the derivation via AF (alternation strategy). Both use specToSpecAntiLocality from Position.lean.

Competing derivations

inductive Erlewine2016.AFCandidate : Type

A candidate derivation for clause-local transitive agent extraction. The OT competition evaluates these: which structure best satisfies the ranked constraints? Both candidates share the same clausal spine (CP > TP > vP > VP); they differ in the v head and the agent's movement path.

• transitiveExtraction : AFCandidate

  Normal transitive derivation: transitive v introduces agent in Spec,vP. A-probe on T attracts agent to Spec,TP (triggering Set A agreement). Subsequent Ā-extraction from Spec,TP to Spec,CP violates SSAL because CP immediately dominates TP.

• agentFocusExtraction : AFCandidate

  Agent Focus derivation: intransitive-like v, agent NOT in Spec,vP. Agent extracts directly to Spec,CP without passing through Spec,TP. No SSAL violation, but cross-referencing is incomplete: no Set A (ergative) agreement because the agent never enters Spec,TP.

@[instance_reducible]

instance Erlewine2016.instDecidableEqAFCandidate : DecidableEq AFCandidate

Equations

• Erlewine2016.instDecidableEqAFCandidate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Erlewine2016.instReprAFCandidate : Repr AFCandidate

Equations

• Erlewine2016.instReprAFCandidate = { reprPrec := Erlewine2016.instReprAFCandidate.repr }

def Erlewine2016.instReprAFCandidate.repr : AFCandidate → ℕ → Std.Format

Equations

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

def Erlewine2016.AFCandidate.verbForm : AFCandidate → Mayan.VerbForm

The verb form that surfaces for each candidate.

Equations

• Erlewine2016.AFCandidate.transitiveExtraction.verbForm = Mayan.VerbForm.transitive
• Erlewine2016.AFCandidate.agentFocusExtraction.verbForm = Mayan.VerbForm.agentFocus

def Erlewine2016.AFCandidate.violatesAntiLocality : AFCandidate → Bool

Does this candidate violate Spec-to-Spec Anti-Locality (SSAL)? The transitive derivation does: the step Spec,TP → Spec,CP crosses no intervening maximal projection (CP immediately dominates TP).

Equations

• Erlewine2016.AFCandidate.transitiveExtraction.violatesAntiLocality = true
• Erlewine2016.AFCandidate.agentFocusExtraction.violatesAntiLocality = false

def Erlewine2016.AFCandidate.violatesXRef : AFCandidate → Bool

Does this candidate violate the XRef (cross-referencing) constraint? AF loses Set A agreement because the agent never enters Spec,TP where the A-probe resides. The transitive candidate maintains full cross-referencing (Set A + Set B).

Equations

• Erlewine2016.AFCandidate.transitiveExtraction.violatesXRef = false
• Erlewine2016.AFCandidate.agentFocusExtraction.violatesXRef = true

The constraints and rankings

def Erlewine2016.ssalConstraint : Constraints.Constraint AFCandidate

Spec-to-Spec Anti-Locality: movement from Spec,XP to Spec,YP is banned when YP immediately dominates XP. Outranks XRef; outranked only by XRef-Participant.

Equations

• Erlewine2016.ssalConstraint c = if c.violatesAntiLocality = true then 1 else 0

def Erlewine2016.xrefConstraint : Constraints.Constraint AFCandidate

XRef (cross-referencing, lowest-ranked): every argument DP must be cross-referenced by a pronominal morpheme on the verb (Set A for ergative, Set B for absolutive).

Equations

• Erlewine2016.xrefConstraint c = if c.violatesXRef = true then 1 else 0

def Erlewine2016.xrefPConstraint (bothParticipants : Bool) : Constraints.Constraint AFCandidate

XRef-Participant (top-ranked): every 1st/2nd-person argument must be cross-referenced. Parameterized by whether both arguments are participants: the AF candidate's single Set B slot can cross-reference only one of them, so AF incurs a violation exactly then; the full-agreement transitive never does.

Equations

• Erlewine2016.xrefPConstraint bothParticipants Erlewine2016.AFCandidate.agentFocusExtraction = if bothParticipants = true then 1 else 0
• Erlewine2016.xrefPConstraint bothParticipants Erlewine2016.AFCandidate.transitiveExtraction = 0

def Erlewine2016.afRanking : List (Constraints.Constraint AFCandidate)

The core two-constraint competition for Kaqchikel AF: SSAL ≫ XRef. Decides the outcome whenever XRef-Participant is inactive (at most one participant argument) — see fullRanking.

Equations

• Erlewine2016.afRanking = [Erlewine2016.ssalConstraint, Erlewine2016.xrefConstraint]

def Erlewine2016.fullRanking (bothParticipants : Bool) : List (Constraints.Constraint AFCandidate)

The full Kaqchikel ranking ([Erl16]'s (83)): XRef-Participant ≫ SSAL ≫ XRef.

Equations

• Erlewine2016.fullRanking bothParticipants = [Erlewine2016.xrefPConstraint bothParticipants, Erlewine2016.ssalConstraint, Erlewine2016.xrefConstraint]

def Erlewine2016.afCandidates : List AFCandidate

The two candidates in the OT competition.

Equations

• Erlewine2016.afCandidates = [Erlewine2016.AFCandidate.transitiveExtraction, Erlewine2016.AFCandidate.agentFocusExtraction]

Anti-locality grounds the transitive crash

theorem Erlewine2016.transitive_crashes : AFCandidate.transitiveExtraction.violatesAntiLocality = true

The transitive candidate violates SSAL. The agent, having moved to Spec,TP via the A-probe, cannot continue to Spec,CP because CP immediately dominates TP — the movement is too local.

theorem Erlewine2016.af_survives : AFCandidate.agentFocusExtraction.violatesAntiLocality = false

The AF candidate does NOT violate SSAL. The agent skips Spec,TP and extracts directly to Spec,CP, crossing enough structure to satisfy anti-locality.

theorem Erlewine2016.candidates_differ : ssalConstraint AFCandidate.transitiveExtraction ≠ ssalConstraint AFCandidate.agentFocusExtraction ∨ xrefConstraint AFCandidate.transitiveExtraction ≠ xrefConstraint AFCandidate.agentFocusExtraction

The two candidates have different violation profiles: they disagree on at least one constraint.

The evaluation selects AF

theorem Erlewine2016.af_is_optimal : (OptimalityTheory.Tableau.ofRanking afCandidates afRanking ⋯).optimal = {AFCandidate.agentFocusExtraction}

AF is the unique optimal candidate. SSAL ≫ XRef means the derivation that avoids anti-locality wins, even though it loses Set A agreement. This is the central result of [Erl16].

theorem Erlewine2016.af_morphology : AFCandidate.agentFocusExtraction.verbForm = Mayan.VerbForm.agentFocus ∧ Mayan.VerbForm.agentFocus.hasSetA = false ∧ Mayan.VerbForm.agentFocus.hasAFSuffix = true

The winning candidate surfaces with AF morphology: the AF suffix (-ö or -n), no Set A (ergative) agreement.

Lexicographic vs satisfaction ordering

theorem Erlewine2016.satisfaction_ordering_incomparable : ¬(ssalConstraint AFCandidate.transitiveExtraction ≤ ssalConstraint AFCandidate.agentFocusExtraction ∧ xrefConstraint AFCandidate.transitiveExtraction ≤ xrefConstraint AFCandidate.agentFocusExtraction) ∧ ¬(ssalConstraint AFCandidate.agentFocusExtraction ≤ ssalConstraint AFCandidate.transitiveExtraction ∧ xrefConstraint AFCandidate.agentFocusExtraction ≤ xrefConstraint AFCandidate.transitiveExtraction)

Under componentwise ≤ (satisfaction ordering), neither candidate dominates: the transitive satisfies XRef but violates SSAL, while AF satisfies SSAL but violates XRef. Each satisfies a constraint the other violates — they are incomparable. OT's lexicographic ranking is what breaks the tie in favor of AF.

theorem Erlewine2016.transitive_worse_on_ssal : ssalConstraint AFCandidate.transitiveExtraction > ssalConstraint AFCandidate.agentFocusExtraction

The transitive candidate is lexicographically worse because it violates the HIGHER-ranked constraint (SSAL, position 0). AF violates only the lower-ranked constraint (XRef, position 1).

Anti-locality predicate grounding

theorem Erlewine2016.antilocality_grounded : ssalConstraint AFCandidate.transitiveExtraction = 1 ∧ ssalConstraint AFCandidate.agentFocusExtraction = 0

The transitive candidate's violation profile reflects specToSpecAntiLocality from Position.lean. The SSAL constraint assigns 1 violation to the transitive candidate and 0 to AF, grounding the OT violation count in the structural predicate.

theorem Erlewine2016.antilocality_drives_af : ssalConstraint AFCandidate.agentFocusExtraction = 0 ∧ (OptimalityTheory.Tableau.ofRanking afCandidates afRanking ⋯).optimal = {AFCandidate.agentFocusExtraction}

AF wins because it has 0 violations of the highest-ranked constraint. The connection to specToSpecAntiLocality: the transitive derivation would require movement from Spec,TP to Spec,CP where CP immediately dominates TP — exactly what the predicate bans. AF avoids this by not placing the agent in Spec,TP at all.

SSAL-inactive contexts: where AF does not appear

Wherever the extractee's movement is not too short, SSAL assigns no violations and XRef alone decides — the full-agreement transitive wins and AF is ungrammatical. Three empirical cells share this violation profile ([Erl16] §§2.2, 3.1): patient extraction (the patient starts in Comp,VP and never passes through Spec,TP), subject extraction across intervening preverbal material (adverb obviation), and the matrix clause of a long-distance extraction (the matrix subject has not moved). Long-distance subject extraction is the two halves side by side: the embedded clause is exactly the af_is_optimal competition — the subject's first step, embedded Spec,TP → Spec,CP, would be too short — so AF appears on the embedded verb, while the matrix verb sits in an SSAL-inactive context and must stay transitive.

def Erlewine2016.ssalInactive : Constraints.Constraint AFCandidate

SSAL in a context where no candidate's movement is too short: vacuously satisfied by both candidates.

Equations

• Erlewine2016.ssalInactive x✝ = 0

theorem Erlewine2016.transitive_optimal_when_ssal_inactive : (OptimalityTheory.Tableau.ofRanking afCandidates [ssalInactive, xrefConstraint] ⋯).optimal = {AFCandidate.transitiveExtraction}

Without an anti-locality violation at stake, the full-agreement transitive is the unique winner — AF is ungrammatical wherever the subject's movement is not too short. Derives the extraction asymmetry (patient extraction never triggers AF), adverb obviation, and the transitive matrix verb under long-distance extraction.

The participant exception (XRef-Participant)

theorem Erlewine2016.af_optimal_full_ranking : (OptimalityTheory.Tableau.ofRanking afCandidates (fullRanking false) ⋯).optimal = {AFCandidate.agentFocusExtraction}

With at most one participant argument, XRef-Participant is inactive and the full ranking agrees with the core competition: AF wins.

theorem Erlewine2016.participant_exception : (OptimalityTheory.Tableau.ofRanking afCandidates (fullRanking true) ⋯).optimal = {AFCandidate.transitiveExtraction}

When both arguments are 1st/2nd person, top-ranked XRef-Participant reverses the outcome: the full-agreement transitive appears even under subject extraction, because AF's single Set B slot would leave a participant argument un-cross-referenced ([Erl16] §5.2).

Reranking and the typology of Mayan AF

[Erl16] §6.1 (his (84)): rerankings of the same three constraints predict three attested language types. Kaqchikel and Popti' instantiate XRef-Participant ≫ SSAL ≫ XRef (AF with the participant exception; in Popti' the exception surfaces whenever the extracted subject is a participant, since Popti's Set B strictly targets the object). Akatek ranks SSAL above both cross-referencing constraints: AF regardless of the arguments' φ-features. Languages ranking XRef ≫ SSAL lack AF altogether — transitive subjects extract with the full-agreement transitive, e.g. Ch'ol (his (93)–(94)): grammatical extraction, not a gap. The two-candidate competition here collapses his AF candidates (which differ in Set B target) into one.

theorem Erlewine2016.akatek_af_regardless_of_participants (b : Bool) : (OptimalityTheory.Tableau.ofRanking afCandidates [ssalConstraint, xrefPConstraint b, xrefConstraint] ⋯).optimal = {AFCandidate.agentFocusExtraction}

Akatek (SSAL ≫ {XRef-Participant, XRef}): AF wins regardless of the arguments' φ-features — no participant exception.

theorem Erlewine2016.no_af_language_transitive_wins : (OptimalityTheory.Tableau.ofRanking afCandidates [xrefConstraint, ssalConstraint] ⋯).optimal = {AFCandidate.transitiveExtraction}

A no-AF language (XRef ≫ SSAL): the full-agreement transitive wins, so transitive subjects extract without AF and without ill-formedness, at the cost of a low-ranked anti-locality violation — Ch'ol's pattern.

Contrast with Q'anjob'al ([CMPP14])

Different Mayan languages circumvent syntactic ergativity through different mechanisms. Q'anjob'al's AF Voice assigns case to the object, freeing the phase-edge escape hatch ([CMPP14]); Kaqchikel's AF avoids the too-local Spec,TP → Spec,CP step at the cost of Set A agreement ([Erl16], for whom the case-based account is the principal foil). Both share the underlying problem — agentive Voice is a phase head trapping the subject — and the same surface effect, loss of Set A.

theorem Erlewine2016.af_mechanism_contrast : CoonMateoPedroPreminger2014.voiceAF.checksCase = true ∧ CoonMateoPedroPreminger2014.kaqVoice.checksCase = false

Q'anjob'al AF Voice checks case; Kaqchikel's regular Voice does NOT. This is the core parametric difference: Q'anjob'al's AF is a case-assigning repair, while Kaqchikel's AF is a locality repair.

theorem Erlewine2016.shared_phase_problem : Minimalist.Voice.agentive.IsPhasal ∧ CoonMateoPedroPreminger2014.kaqVoice.IsPhasal

Both languages share the underlying problem: agentive Voice is a phase head, creating a locality boundary that traps the subject.

theorem Erlewine2016.both_have_extraction_asymmetries : Qanjobal.absPosition = Mayan.ABSPosition.high ∧ Kaqchikel.absPosition = Mayan.ABSPosition.high ∧ Extraction.Marked Qanjobal.Extraction.realize Extraction.ExtractionTarget.subject ∧ Extraction.Marked Kaqchikel.Extraction.realize Extraction.ExtractionTarget.subject

Both Q'anjob'al and Kaqchikel are HIGH-ABS languages that mark transitive-subject extraction.

theorem Erlewine2016.both_af_lose_setA : Qanjobal.agentFocusForm.hasSetA = false ∧ Mayan.VerbForm.agentFocus.hasSetA = false

Kaqchikel AF loses Set A agreement (the agent never enters Spec,TP). Q'anjob'al AF also loses Set A agreement. Same surface morphological effect, different underlying mechanism.

Extraction strategy

theorem Erlewine2016.strategy_is_af : Kaqchikel.Extraction.strategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme

Kaqchikel marks transitive-subject extraction with dedicated AF morphology (-ö or -n) — the same surface strategy-type as Mam's extraction marker, in contrast to Toba Batak's structural pivot restriction ([Erl18]). Same underlying problem (anti-locality), different marking.