Erlewine (2016): Anti-locality and Optimality in Kaqchikel Agent Focus

Kaqchikel marks the Ā-extraction of a transitive subject with Agent Focus (AF), a verb form with an AF suffix and no Set A agreement. Erlewine argues that the trigger is movement that is too short: Spec-to-Spec Anti-Locality bans a step from the specifier of a phrase that crosses no other maximal projection, and a subject that T's optional Set A probe has moved to Spec,TP sits one step below Spec,CP, while an intransitive subject stays in situ. AF is the derivation that skips Spec,TP at the cost of an argument left un-cross-referenced, chosen by ranked constraints over competing derivations of the whole clause: anti-locality outranks cross-referencing, so AF disappears when an adverb or another operator intervenes, and cross-referencing participants outranks both, so the full transitive returns when both arguments are first or second person, an exception the paper argues no last-resort account of AF can make. Rerankings give the typology of Popti', Akatek and Ch'ol.

Main statements

• rows_optimal: every example is grammatical exactly when an optimal derivation realizes its verb form.
• af_iff_immediately_preverbal: with at most one participant argument, Kaqchikel AF is optimal exactly when the subject moves to the layer immediately above TP.
• exists_optimal_agentFocus_iff: the grammar derives the Kaqchikel fragment's Agent Focus reflex for arguments of every person.
• lastResort_matches_iff: the last-resort model of Coon, Mateo Pedro and Preminger, run on the Kaqchikel examples, judges an example correctly exactly when its subject is not extracted past an intervening layer and its arguments are not both participants.

Implementation notes

• A clause is the spine VP, vP, TP and the layers above TP, an adverb's projection after Cinque, the CPs of Rizzi's split periphery and the topic projection, indexed from the bottom; the crossing set of a step is the interval of projections from the origin's up to the landing site's. Long-distance extraction is the embedded clause's competition, since movement stops at the embedded Spec,CP.
• A candidate is a choice of the optional Set A probe and of the Set B probe's target; the two probes cannot share a goal, the Set A probe sees only the subject at the vP edge, and Popti' and Akatek restrict Set B to the object. The constraint preferring plural targets is not modelled.
• The last-resort model is the one formalized in Studies/CoonMateoPedroPreminger2014.lean, run on each Kaqchikel example with Infl licensing the object, the Voice of the attested form and the extracted argument's role; its authors propose it for Q'anjob'al only, as the paper's fn. 46 notes.
• Example and footnote numbers are the published version's; the examples are Data.Examples.Erlewine2016.

References

• [Erl16]
• [Abe03]
• [Cin99]
• [Riz97]
• [Sti06]
• [Pre11a]
• [CMPP14]
• [PS93]

inductive Erlewine2016.Arg : Type

The arguments of a verb.

• subj : Arg
• obj : Arg

@[instance_reducible]

instance Erlewine2016.instDecidableEqArg : DecidableEq Arg

Equations

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

@[instance_reducible]

instance Erlewine2016.instReprArg : Repr Arg

Equations

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

def Erlewine2016.instReprArg.repr : Arg → ℕ → Std.Format

Equations

• Erlewine2016.instReprArg.repr Erlewine2016.Arg.subj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Erlewine2016.Arg.subj")).group prec✝
• Erlewine2016.instReprArg.repr Erlewine2016.Arg.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Erlewine2016.Arg.obj")).group prec✝

inductive Erlewine2016.Layer : Type

A layer of the clause above TP, an adverb's projection, a CP of the periphery, or the topic projection.

• advP : Layer
• cP : Layer
• topP : Layer

@[instance_reducible]

instance Erlewine2016.instDecidableEqLayer : DecidableEq Layer

Equations

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

@[instance_reducible]

instance Erlewine2016.instReprLayer : Repr Layer

Equations

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

def Erlewine2016.instReprLayer.repr : Layer → ℕ → Std.Format

Equations

• Erlewine2016.instReprLayer.repr Erlewine2016.Layer.advP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Erlewine2016.Layer.advP")).group prec✝
• Erlewine2016.instReprLayer.repr Erlewine2016.Layer.cP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Erlewine2016.Layer.cP")).group prec✝
• Erlewine2016.instReprLayer.repr Erlewine2016.Layer.topP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Erlewine2016.Layer.topP")).group prec✝

structure Erlewine2016.Input : Type

A clause and its extraction, with whether it is transitive, the layers above TP from the bottom, the extracted argument with the index of the layer it lands in, and the person of each argument.

• transitive : Bool
• layers : List Layer
• extracted : Option (Arg × ℕ)
• subj : Person
• obj : Person

def Erlewine2016.instDecidableEqInput.decEq (x✝ x✝¹ : Input) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Erlewine2016.instDecidableEqInput : DecidableEq Input

Equations

• Erlewine2016.instDecidableEqInput = Erlewine2016.instDecidableEqInput.decEq

@[instance_reducible]

instance Erlewine2016.instReprInput : Repr Input

Equations

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

def Erlewine2016.instReprInput.repr : Input → ℕ → Std.Format

Equations

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

def Erlewine2016.argsOf (transitive : Bool) : List Arg

The arguments of a transitive or intransitive clause.

Equations

• Erlewine2016.argsOf transitive = if transitive = true then [Erlewine2016.Arg.subj, Erlewine2016.Arg.obj] else [Erlewine2016.Arg.subj]

def Erlewine2016.Input.args (i : Input) : List Arg

The arguments of the clause.

Equations

• i.args = Erlewine2016.argsOf i.transitive

def Erlewine2016.Input.person (i : Input) : Arg → Person

The person of an argument.

Equations

• i.person Erlewine2016.Arg.subj = i.subj
• i.person Erlewine2016.Arg.obj = i.obj

The spine and anti-locality

def Erlewine2016.tP : ℕ

The index of TP in the spine VP, vP, TP, layers.

Equations

• Erlewine2016.tP = 2

def Erlewine2016.layerIndex (k : ℕ) : ℕ

The index of the kth layer above TP.

Equations

• Erlewine2016.layerIndex k = 3 + k

def Erlewine2016.Arg.base : Arg → ℕ

The base position of an argument, Spec,vP for the subject and the complement of V for the object (§4.1).

Equations

• Erlewine2016.Arg.subj.base = 1
• Erlewine2016.Arg.obj.base = 0

def Erlewine2016.crosses (α β : ℕ) : Finset ℕ

The projections a step crosses (43), those dominating the origin, which lies within projection α, but not the landing site, the specifier of projection β.

Equations

• Erlewine2016.crosses α β = Finset.Ico α β

def Erlewine2016.TooClose (α β : ℕ) : Prop

Spec-to-Spec Anti-Locality, (42): a step is too close when it crosses no maximal projection other than the one it leaves.

Equations

• Erlewine2016.TooClose α β = ∀ γ ∈ Erlewine2016.crosses α β, γ = α

@[instance_reducible]

instance Erlewine2016.instDecidableTooClose (α β : ℕ) : Decidable (TooClose α β)

Equations

• Erlewine2016.instDecidableTooClose α β = id inferInstance

theorem Erlewine2016.tooClose_iff {α β : ℕ} (h : α < β) : TooClose α β ↔ β = α + 1

An upward step is too close exactly when its landing site immediately dominates its origin, the configuration of (44).

Derivations and constraints

structure Erlewine2016.Candidate : Type

A derivation of the clause (§5.1), fixing whether T's optional Set A probe is used, moving the subject to Spec,TP, and the argument its Set B probe targets.

• aProbe : Bool
• bTarget : Arg

def Erlewine2016.instDecidableEqCandidate.decEq (x✝ x✝¹ : Candidate) : Decidable (x✝ = x✝¹)

Equations

• Erlewine2016.instDecidableEqCandidate.decEq { aProbe := a, bTarget := a_1 } { aProbe := b, bTarget := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Erlewine2016.instDecidableEqCandidate : DecidableEq Candidate

Equations

• Erlewine2016.instDecidableEqCandidate = Erlewine2016.instDecidableEqCandidate.decEq

def Erlewine2016.instReprCandidate.repr : Candidate → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Erlewine2016.instReprCandidate : Repr Candidate

Equations

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

def Erlewine2016.candidatesOf (transitive objectOnly : Bool) : List Candidate

The candidates of a numeration. The Set B target is an argument, the two probes cannot share a goal, and where Set B is restricted to the object it targets the object.

Equations

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

def Erlewine2016.candidates (i : Input) (objectOnly : Bool) : List Candidate

The candidates of a clause.

Equations

• Erlewine2016.candidates i objectOnly = Erlewine2016.candidatesOf i.transitive objectOnly

theorem Erlewine2016.candidates_ne_nil (i : Input) (o : Bool) : candidates i o ≠ []

def Erlewine2016.CrossRef (c : Candidate) (a : Arg) : Prop

An argument is cross-referenced when the Set A probe targets it, the subject having moved to Spec,TP, or the Set B probe does, (46).

Equations

• Erlewine2016.CrossRef c a = (c.aProbe = true ∧ a = Erlewine2016.Arg.subj ∨ c.bTarget = a)

@[instance_reducible]

instance Erlewine2016.instDecidableCrossRef (c : Candidate) (a : Arg) : Decidable (CrossRef c a)

Equations

• Erlewine2016.instDecidableCrossRef c a = id inferInstance

def Erlewine2016.Candidate.origin (c : Candidate) : Arg → ℕ

The position an extracted argument moves from, Spec,TP for a subject the Set A probe has attracted, its base position otherwise.

Equations

• c.origin Erlewine2016.Arg.subj = if c.aProbe = true then Erlewine2016.tP else Erlewine2016.Arg.subj.base
• c.origin Erlewine2016.Arg.obj = Erlewine2016.Arg.obj.base

def Erlewine2016.ssal (i : Input) : OptimalityTheory.Constraint Candidate

Spec-to-Spec Anti-Locality as a violable constraint: one violation per step that is too close.

Equations

• Erlewine2016.ssal i c = match i.extracted with | none => 0 | some (a, k) => if Erlewine2016.TooClose (c.origin a) (Erlewine2016.layerIndex k) then 1 else 0

def Erlewine2016.xref (i : Input) : OptimalityTheory.Constraint Candidate

XRef assigns one violation per argument not cross-referenced.

Equations

• Erlewine2016.xref i c = (List.filter (fun (x : Erlewine2016.Arg) => decide ¬Erlewine2016.CrossRef c x) i.args).length

def Erlewine2016.xrefP (i : Input) : OptimalityTheory.Constraint Candidate

XRef-Participant assigns one violation per participant argument not cross-referenced (§5.2), deriving the Set B agreement of [Pre11a] and the salience hierarchy of [Sti06].

Equations

• Erlewine2016.xrefP i c = (List.filter (fun (a : Erlewine2016.Arg) => decide ((i.person a).IsSAP ∧ ¬Erlewine2016.CrossRef c a)) i.args).length

structure Erlewine2016.Grammar : Type

A grammar of §6.1, with a ranking of the constraints and whether Set B is restricted to the object.

• ranking : List (Input → OptimalityTheory.Constraint Candidate)
• objectOnly : Bool

def Erlewine2016.Grammar.tableau (g : Grammar) (i : Input) : OptimalityTheory.Tableau Candidate (List.map (fun (x : Input → OptimalityTheory.Constraint Candidate) => x i) g.ranking).length

The competition of a clause under a grammar.

Equations

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

def Erlewine2016.kaqchikel : Grammar

Kaqchikel ranks XRef-Participant ≫ SSAL ≫ XRef, Set B free to target either argument.

Equations

• Erlewine2016.kaqchikel = { ranking := [Erlewine2016.xrefP, Erlewine2016.ssal, Erlewine2016.xref], objectOnly := false }

def Erlewine2016.popti : Grammar

Popti' has the Kaqchikel ranking with Set B restricted to the object.

Equations

• Erlewine2016.popti = { ranking := [Erlewine2016.xrefP, Erlewine2016.ssal, Erlewine2016.xref], objectOnly := true }

def Erlewine2016.akatek : Grammar

Akatek ranks SSAL above both cross-referencing constraints, Set B restricted to the object.

Equations

• Erlewine2016.akatek = { ranking := [Erlewine2016.ssal, Erlewine2016.xrefP, Erlewine2016.xref], objectOnly := true }

def Erlewine2016.chol : Grammar

Ch'ol, a Mayan language without AF, ranks XRef ≫ SSAL.

Equations

• Erlewine2016.chol = { ranking := [Erlewine2016.xref, Erlewine2016.ssal], objectOnly := false }

Realization

def Erlewine2016.Candidate.AFSuffix (args : List Arg) (c : Candidate) : Prop

The AF suffix is realized when some argument is not cross-referenced (48).

Equations

• Erlewine2016.Candidate.AFSuffix args c = ∃ a ∈ args, ¬Erlewine2016.CrossRef c a

@[instance_reducible]

instance Erlewine2016.instDecidableAFSuffix (args : List Arg) (c : Candidate) : Decidable (Candidate.AFSuffix args c)

Equations

• Erlewine2016.instDecidableAFSuffix args c = id inferInstance

theorem Erlewine2016.afSuffix_iff_xref_pos (i : Input) (c : Candidate) : Candidate.AFSuffix i.args c ↔ 0 < xref i c

The AF suffix marks a violation of XRef.

def Erlewine2016.Candidate.form (args : List Arg) (c : Candidate) : Mayan.VerbForm

The verb form of a derivation, Set A being realized only when the subject moved to Spec,TP.

Equations

• Erlewine2016.Candidate.form args c = if Erlewine2016.Candidate.AFSuffix args c then Mayan.VerbForm.agentFocus else Mayan.VerbForm.transitive

theorem Erlewine2016.form_hasSetA (o : Bool) (c : Candidate) : c ∈ candidatesOf true o → ((Candidate.form (argsOf true) c).HasSetA ↔ c.aProbe = true)

Among the candidates of a transitive clause, the AF form is exactly the absence of the Set A probe: the derivation that skips Spec,TP loses Set A and gains the suffix.

The rows

def Erlewine2016.clauseTable : List (String × Bool)

The clause types as named in the rows.

Equations

• Erlewine2016.clauseTable = [("transitive", true), ("intransitive", false)]

def Erlewine2016.layerTable : List (String × List Layer)

The layers above TP as named in the rows.

Equations

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

def Erlewine2016.extractedTable : List (String × Option Arg)

The extracted argument as named in the rows.

Equations

• Erlewine2016.extractedTable = [("none", none), ("subject", some Erlewine2016.Arg.subj), ("object", some Erlewine2016.Arg.obj)]

def Erlewine2016.personTable : List (String × Person)

The persons as named in the rows.

Equations

• Erlewine2016.personTable = [("1", Person.first), ("2", Person.second), ("3", Person.third)]

def Erlewine2016.verbTable : List (String × Mayan.VerbForm)

The verb forms as named in the rows.

Equations

• Erlewine2016.verbTable = [("AF", Mayan.VerbForm.agentFocus), ("full", Mayan.VerbForm.transitive)]

def Erlewine2016.grammarTable : List (String × Grammar)

The grammars by glottocode.

Equations

• Erlewine2016.grammarTable = [("kaqc1270", Erlewine2016.kaqchikel), ("popt1235", Erlewine2016.popti), ("west2635", Erlewine2016.akatek), ("chol1282", Erlewine2016.chol)]

structure Erlewine2016.Row : Type

A row, with the clause, its language's grammar, the attested form and the judgment.

• input : Input
• grammar : Grammar
• form : Mayan.VerbForm
• judgment : Judgment

def Erlewine2016.Row.ofDatum (ex : Datum) : Option Row

A row from an example; landing layers count from one in the rows.

Equations

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

theorem Erlewine2016.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def Erlewine2016.rows : List Row

The rows of all four languages.

Equations

• Erlewine2016.rows = List.filterMap Erlewine2016.Row.ofDatum Erlewine2016.Examples.all

def Erlewine2016.kaqchikelRows : List Row

The Kaqchikel rows.

Equations

• Erlewine2016.kaqchikelRows = List.filterMap Erlewine2016.Row.ofDatum (List.filter (fun (x : Datum) => decide (x.language = "kaqc1270")) Erlewine2016.Examples.all)

theorem Erlewine2016.rows_optimal (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ ∃ c ∈ (r.grammar.tableau r.input).optimal, Candidate.form r.input.args c = r.form)

In every row the attested form is grammatical exactly when an optimal derivation realizes it.

theorem Erlewine2016.af_iff_immediately_preverbal (r : Row) : r ∈ kaqchikelRows → ¬(r.input.subj.IsSAP ∧ r.input.obj.IsSAP) → ((∃ c ∈ (kaqchikel.tableau r.input).optimal, Candidate.AFSuffix r.input.args c) ↔ r.input.extracted = some (Arg.subj, 0))

The generalization of §3. With at most one participant argument, AF is optimal in Kaqchikel exactly when the subject moves to the layer immediately above TP.

The competitions of §5 and §6

def Erlewine2016.subjectExtraction (s o : Person) : Input

Subject extraction to Spec,CP in a simple transitive clause.

Equations

• Erlewine2016.subjectExtraction s o = { transitive := true, layers := [Erlewine2016.Layer.cP], extracted := some (Erlewine2016.Arg.subj, 0), subj := s, obj := o }

theorem Erlewine2016.no_extraction_full (s o : Person) : (kaqchikel.tableau { transitive := true, layers := [Layer.cP], extracted := none, subj := s, obj := o }).optimal = {{ aProbe := true, bTarget := Arg.obj }}

Without extraction (§5.1), cross-referencing selects the derivation that moves the subject to Spec,TP; this is also what an evaluation at TP would select before the anti-locality violation of a later extraction is visible, the argument of §5.3 for evaluation at the clause.

theorem Erlewine2016.subject_extraction_af : (kaqchikel.tableau (subjectExtraction Person.third Person.third)).optimal = {{ aProbe := false, bTarget := Arg.subj }, { aProbe := false, bTarget := Arg.obj }}

Under subject extraction with two third-person arguments (§5.1), both AF derivations beat the derivation through Spec,TP, and the two constraints do not decide the Set B target.

theorem Erlewine2016.participant_breaks_tie : (kaqchikel.tableau (subjectExtraction Person.second Person.third)).optimal = {{ aProbe := false, bTarget := Arg.subj }} ∧ (kaqchikel.tableau (subjectExtraction Person.third Person.second)).optimal = {{ aProbe := false, bTarget := Arg.obj }}

A participant argument breaks the tie, Set B cross-referencing it (§5.2).

theorem Erlewine2016.participant_exception : (kaqchikel.tableau (subjectExtraction Person.first Person.second)).optimal = {{ aProbe := true, bTarget := Arg.obj }}

With two participant arguments the full-agreement transitive is optimal (§5.2), the anti-locality violation notwithstanding.

theorem Erlewine2016.exists_optimal_agentFocus_iff (c : Mayan.VerbClass) (s o : Person) : (∃ d ∈ (kaqchikel.tableau (subjectExtraction s o)).optimal, Candidate.form (argsOf true) d = Mayan.VerbForm.agentFocus) ↔ (Kaqchikel.Extraction.realize c s o (Mayan.ExtractionSite.argument ArgumentRole.A)).Nonempty

Subject extraction to Spec,CP has an optimal AF derivation exactly when the arguments are not both participants, which is when the Kaqchikel fragment records the Agent Focus reflex.

theorem Erlewine2016.no_af_without_short_step : (kaqchikel.tableau { transitive := true, layers := [Layer.cP], extracted := some (Arg.obj, 0), subj := Person.third, obj := Person.third }).optimal = {{ aProbe := true, bTarget := Arg.obj }} ∧ ∀ c ∈ (kaqchikel.tableau { transitive := false, layers := [Layer.cP], extracted := some (Arg.subj, 0), subj := Person.third, obj := Person.third }).optimal, ¬Candidate.AFSuffix (argsOf false) c

Object extraction and intransitive subject extraction cross enough structure (§4.2), and no optimal derivation bears the AF suffix.

theorem Erlewine2016.typology : (popti.tableau (subjectExtraction Person.second Person.third)).optimal = {{ aProbe := true, bTarget := Arg.obj }} ∧ (popti.tableau (subjectExtraction Person.third Person.second)).optimal = {{ aProbe := false, bTarget := Arg.obj }} ∧ (akatek.tableau (subjectExtraction Person.first Person.third)).optimal = {{ aProbe := false, bTarget := Arg.obj }} ∧ (chol.tableau (subjectExtraction Person.third Person.second)).optimal = {{ aProbe := true, bTarget := Arg.obj }}

The typology of rerankings (§6.1). Popti' keeps the full form when the subject is a participant and uses AF when it is not; Akatek uses AF for a participant subject; Ch'ol keeps the full form throughout.

The last-resort alternative

def Erlewine2016.Arg.role (transitive : Bool) : Arg → ArgumentRole

The role of an argument in a transitive or intransitive clause.

Equations

• Erlewine2016.Arg.role transitive Erlewine2016.Arg.subj = if transitive = true then ArgumentRole.A else ArgumentRole.S
• Erlewine2016.Arg.role transitive Erlewine2016.Arg.obj = ArgumentRole.P

def Erlewine2016.Row.lastResortClause (r : Row) : CoonMateoPedroPreminger2014.Clause

The clause the last-resort model of Coon, Mateo Pedro and Preminger assigns a Kaqchikel row, finite, with Infl licensing the object as Kaqchikel's high absolutive has it, the Voice of the attested form, and the extracted argument by its role.

Equations

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

def Erlewine2016.Row.DistantSubject (r : Row) : Prop

The subject is extracted past an intervening layer, an adverb, another operator or a topic (§3).

Equations

• r.DistantSubject = ∃ e ∈ r.input.extracted, e.1 = Erlewine2016.Arg.subj ∧ e.2 ≠ 0

def Erlewine2016.Row.TwoParticipants (r : Row) : Prop

Both arguments are participants (§5.2).

Equations

• r.TwoParticipants = (r.input.subj.IsSAP ∧ r.input.obj.IsSAP)

@[instance_reducible]

instance Erlewine2016.instDecidablePredRowDistantSubject : DecidablePred Row.DistantSubject

Equations

• Erlewine2016.instDecidablePredRowDistantSubject r = Erlewine2016.instDecidablePredRowDistantSubject._aux_1 r

@[instance_reducible]

instance Erlewine2016.instDecidablePredRowTwoParticipants : DecidablePred Row.TwoParticipants

Equations

• Erlewine2016.instDecidablePredRowTwoParticipants x✝ = { decide := decide x✝.input.subj.IsSAP && decide x✝.input.obj.IsSAP, reflects_decide := ⋯ }

theorem Erlewine2016.lastResort_matches_iff (r : Row) : r ∈ kaqchikelRows → ((r.judgment = Judgment.acceptable ↔ CoonMateoPedroPreminger2014.Converges r.lastResortClause) ↔ ¬r.DistantSubject ∧ ¬r.TwoParticipants)

The last-resort model merges the Case-assigning AF Voice only where the regular derivation would crash, so it sees neither person nor what lies between the extracted subject and the verb. It judges a Kaqchikel example correctly exactly when the subject is not extracted past an intervening layer, the locality such Case-based accounts miss (fn. 47), and the arguments are not both participants, the exception for which a last resort would need a last resort of its own (§5.3, (81)); the optimality grammar fits every example (rows_optimal).