Alstott & Aravind (2026): aspectual coercion in before- and after-clauses

Telic before-clauses and atelic after-clauses each have a weak and a strong reading. Under-specification theories (Anscombe's entries with a weakened before, weakBefore, weakAfter) give them one LF with the weak truth conditions; Rett's ambiguity theory (before, after) gives the strong reading by default and derives the weak one by inserting completive or inchoative. Since coercion has a processing cost, only Rett's theory predicts that a before-clause is harder to read in a before-finish context than in a before-start context, and an after-clause harder in an after-start context: on the paper's own experimental contexts the default reading is true in one context and false in the other (exp2_rett_asymmetric, exp4_rett_asymmetric), while the under-specification reading, and the while-competition implicature that might strengthen it, hold in both (exp2_underspecification_symmetric, exp4_underspecification_symmetric). Four self-paced reading experiments find the predicted asymmetries for before (Exp. 2) and after (Exp. 4), a cost for completive coercion in at-modifier sentences (Exp. 1b), and no cost for inchoative coercion in atelic within-modifier sentences (Exps. 1a, 3), against Brennan & Pylkkänen.

The last result motivates the paper's non-coercive account of within-modifiers: the assertion (33b) together with the scalar implicature over shorter spans entails that the state began inside the span, with no operator involved (within_implicature_onset), and the same entry handles telic within-sentences (within_accomplishment_iff). Rett's operator assignment (rettOperator) matches the observed costs on every construction but atelic within (connective_costs_track_rett, within_disconfirms_inchoat), and the revised assignment matches all of them (costs_track_revised); coerced sentences are also rated less natural exactly where they are slower (naturalness_tracks_cost). The costs in Exps. 2 and 4 appear one word later than in Exp. 1b, which the paper tentatively attributes to pragmatic as against semantic coercion.

References

• [AA26]
• [Ret20a]
• [Ans64]
• [Hei74]
• [Kri10]
• [Con10]
• [BP10]
• [Del83]

The two theories (§2.1)

def AlstottAravind2026.weakBefore {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

The under-specification entry for before, (7a), holds when some run-time of the main clause is partly preceded by every run-time of the embedded clause. It is Anscombe's entry with some subinterval following in place of every, the weakening accomplishments require.

Equations

• AlstottAravind2026.weakBefore A B = ∃ i ∈ A, ∀ j ∈ B, i.toProd.2 < j.toProd.2

def AlstottAravind2026.weakAfter {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

The under-specification entry for after, (7b), holds when some run-time of the main clause fully follows some run-time of the embedded clause.

Equations

• AlstottAravind2026.weakAfter A B = ∃ i ∈ A, ∃ j ∈ B, j.toProd.2 < i.toProd.1

def AlstottAravind2026.Overlap {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

Temporal overlap — the while reading a competition-based implicature negates (§8.1).

Equations

• AlstottAravind2026.Overlap A B = ∃ t ∈ Tense.timeTrace A, t ∈ Tense.timeTrace B

theorem AlstottAravind2026.weakBefore_stative_accomplishment_iff {T : Type u_1} [LinearOrder T] (a b : NonemptyInterval T) : weakBefore (Set.Iic a) {b} ↔ a.toProd.1 < b.toProd.2

A stative is weakly before an accomplishment iff its onset precedes the telos.

theorem AlstottAravind2026.weakAfter_stative_stative_iff {T : Type u_1} [LinearOrder T] (a b : NonemptyInterval T) : weakAfter (Set.Iic a) (Set.Iic b) ↔ b.toProd.1 < a.toProd.2

A stative is weakly after a stative iff its end follows the other's onset.

theorem AlstottAravind2026.overlap_stative_accomplishment_iff {T : Type u_1} [LinearOrder T] (a b : NonemptyInterval T) : Overlap (Set.Iic a) {b} ↔ a.toProd.1 ≤ b.toProd.2 ∧ b.toProd.1 ≤ a.toProd.2

A stative and an accomplishment overlap iff neither ends before the other starts.

The experimental contexts (29) and (31)

Time is measured in minutes; a stative denotes an interval with its subintervals, an accomplishment its single run-time.

def AlstottAravind2026.hectorBuilds : NonemptyInterval ℕ

Hector builds the tent 4:00–4:30pm, minutes after noon.

Equations

• AlstottAravind2026.hectorBuilds = { fst := 240, snd := 270, fst_le_snd := AlstottAravind2026.hectorBuilds._proof_2 }

def AlstottAravind2026.emmaIrritableA : NonemptyInterval ℕ

Emma is irritable 2:00–4:30pm in the before-start context, (29a).

Equations

• AlstottAravind2026.emmaIrritableA = { fst := 120, snd := 270, fst_le_snd := AlstottAravind2026.emmaIrritableA._proof_2 }

def AlstottAravind2026.emmaIrritableB : NonemptyInterval ℕ

Emma is irritable 4:15–4:30pm in the before-finish context, (29b).

Equations

• AlstottAravind2026.emmaIrritableB = { fst := 255, snd := 270, fst_le_snd := AlstottAravind2026.emmaIrritableB._proof_2 }

def AlstottAravind2026.laraFears : NonemptyInterval ℕ

Lara fears the dog 10:00–10:15am, minutes after midnight.

Equations

• AlstottAravind2026.laraFears = { fst := 600, snd := 615, fst_le_snd := AlstottAravind2026.laraFears._proof_2 }

def AlstottAravind2026.daveRegretfulA : NonemptyInterval ℕ

Dave is regretful 10:05–10:15am in the after-start context, (31a).

Equations

• AlstottAravind2026.daveRegretfulA = { fst := 605, snd := 615, fst_le_snd := AlstottAravind2026.daveRegretfulA._proof_2 }

def AlstottAravind2026.daveRegretfulB : NonemptyInterval ℕ

Dave is regretful from 10:05am for many days in the after-finish context, (31b).

Equations

• AlstottAravind2026.daveRegretfulB = { fst := 605, snd := 4935, fst_le_snd := AlstottAravind2026.daveRegretfulB._proof_2 }

@[reducible, inline]

abbrev AlstottAravind2026.tent : Set (NonemptyInterval ℕ)

Equations

• AlstottAravind2026.tent = {AlstottAravind2026.hectorBuilds}

@[reducible, inline]

abbrev AlstottAravind2026.irritableA : Set (NonemptyInterval ℕ)

Equations

• AlstottAravind2026.irritableA = Set.Iic AlstottAravind2026.emmaIrritableA

@[reducible, inline]

abbrev AlstottAravind2026.irritableB : Set (NonemptyInterval ℕ)

Equations

• AlstottAravind2026.irritableB = Set.Iic AlstottAravind2026.emmaIrritableB

@[reducible, inline]

abbrev AlstottAravind2026.fear : Set (NonemptyInterval ℕ)

Equations

• AlstottAravind2026.fear = Set.Iic AlstottAravind2026.laraFears

@[reducible, inline]

abbrev AlstottAravind2026.regretfulA : Set (NonemptyInterval ℕ)

Equations

• AlstottAravind2026.regretfulA = Set.Iic AlstottAravind2026.daveRegretfulA

@[reducible, inline]

abbrev AlstottAravind2026.regretfulB : Set (NonemptyInterval ℕ)

Equations

• AlstottAravind2026.regretfulB = Set.Iic AlstottAravind2026.daveRegretfulB

theorem AlstottAravind2026.exp2_rett_asymmetric : Rett2020a.before irritableA tent ∧ ¬Rett2020a.before irritableB tent ∧ Rett2020a.before irritableB (Rett2020a.completive tent)

In Exp. 2 Rett's default before-start reading is true in the before-start context and false in the before-finish context, where completive restores truth, so coercion is needed in (29b) only.

theorem AlstottAravind2026.exp2_underspecification_symmetric : (weakBefore irritableA tent ∧ weakBefore irritableB tent) ∧ Overlap irritableA tent ∧ Overlap irritableB tent

In Exp. 2 the under-specification reading is true in both contexts, and so is the overlap a while-competition implicature would negate, so neither distinguishes (29a) from (29b) (§8.1).

theorem AlstottAravind2026.exp4_rett_asymmetric : ¬Rett2020a.after regretfulA fear ∧ Rett2020a.after regretfulA (Rett2020a.inchoative fear) ∧ Rett2020a.after regretfulB fear

In Exp. 4 Rett's default after-finish reading is false in the after-start context, where inchoative restores truth, and true in the after-finish context, so coercion is needed in (31a) only.

theorem AlstottAravind2026.exp4_underspecification_symmetric : weakAfter regretfulA fear ∧ weakAfter regretfulB fear

In Exp. 4 the under-specification reading is true in both contexts.

A non-coercive account of within-modifiers (§8.2)

def AlstottAravind2026.within (t d : ℕ) (p : Set (NonemptyInterval ℕ)) : Prop

Within d at the reference time t, (33b), holds when the clause holds throughout some subinterval of [t, t + d].

Equations

• AlstottAravind2026.within t d p = ∃ i ∈ p, t ≤ i.toProd.1 ∧ i.toProd.2 ≤ t + d

theorem AlstottAravind2026.within_implicature_onset {s f t d d' : ℕ} (hsf : s ≤ f) (h : within t d (Set.Iic { fst := s, snd := f, fst_le_snd := hsf })) (h' : ¬within t d' (Set.Iic { fst := s, snd := f, fst_le_snd := hsf })) : t + d' < s ∧ s ≤ t + d

For a state holding throughout [s, f], within d says the state reaches into the span, and the negation of the alternative with a shorter span d' (35) says it does not reach into the shorter span; together they locate the state's onset inside (t + d', t + d] — the change-of-state reading without any operator.

theorem AlstottAravind2026.within_accomplishment_iff (t d : ℕ) (i : NonemptyInterval ℕ) : within t d {i} ↔ t ≤ i.toProd.1 ∧ i.toProd.2 ≤ t + d

For an accomplishment with run-time i, within d says the whole run-time lies in the span, (36), by the same entry and with no operator either.

Predictions against the four experiments

def AlstottAravind2026.rettOperator (row : Datum) : Option String

The operator Rett's theory inserts (§3) is inchoative for atelic within-modifier sentences and after-start readings of atelic after-clauses, and completive for accomplishment at-modifier sentences and before-finish readings of telic before-clauses.

Equations

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

def AlstottAravind2026.revisedOperator (row : Datum) : Option String

The paper's revision (§8.2) inserts no operator in within-modifier sentences.

Equations

• AlstottAravind2026.revisedOperator row = if row.feature? "construction" = some "within" then none else AlstottAravind2026.rettOperator row

def AlstottAravind2026.IsAspectualTrial (row : Datum) : Prop

The aspectual-coercion trials and their controls.

Equations

• AlstottAravind2026.IsAspectualTrial row = (row.feature? "trial" = some "aspectualCoercion" ∨ row.feature? "trial" = some "aspectualControl")

@[instance_reducible]

instance AlstottAravind2026.instDecidablePredDatumIsAspectualTrial : DecidablePred IsAspectualTrial

Equations

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

theorem AlstottAravind2026.connective_costs_track_rett (row : Datum) : row ∈ Examples.all → IsAspectualTrial row → row.feature? "construction" ≠ some "within" → ((rettOperator row).isSome = true ↔ row.feature? "rtCost" = some "yes")

Off the within-modifier trials, a sentence was read more slowly than its control exactly when Rett's theory inserts an operator (Exps. 1b, 2, 4).

theorem AlstottAravind2026.within_disconfirms_inchoat (row : Datum) : row ∈ Examples.all → IsAspectualTrial row → row.feature? "construction" = some "within" → rettOperator row = some "inchoative" ∧ row.feature? "rtCost" = some "no"

On the atelic within-modifier trials Rett's theory inserts inchoative and no cost was found (Exps. 1a, 3).

theorem AlstottAravind2026.costs_track_revised (row : Datum) : row ∈ Examples.all → IsAspectualTrial row → ((revisedOperator row).isSome = true ↔ row.feature? "rtCost" = some "yes")

With the §8.2 revision, operator insertion and observed cost coincide on every aspectual trial.

theorem AlstottAravind2026.naturalness_tracks_cost (row : Datum) : row ∈ Examples.all → IsAspectualTrial row → (row.feature? "naturalness" = some "lower" ↔ row.feature? "rtCost" = some "yes")

Coerced sentences are rated less natural than their controls exactly where they are read more slowly.