[AA26]: On aspectual coercion in before- and after-clauses

[AA26] [Ret20]

Self-paced reading data from 4 experiments testing [Ret20]'s prediction that aspectual coercion (INCHOAT, COMPLET) incurs measurable processing cost. Under-specification theories (e.g. [Ans64]) do not predict such costs.

Results Summary

Exp	Coercion type	RT effect	Naturalness	Supports Rett?
1a	INCHOAT (within-modifier)	null	null	No
1b	COMPLET (at-modifier)	sig verb+1	sig lower	Yes
2	COMPLET (before-clause)	sig verb+2†	sig lower	Yes
3	INCHOAT (subj-experiencer)	null	null	No
4	INCHOAT (after-clause)	sig verb+2†	sig lower	Yes

† = exploratory analysis (pre-registered verb/verb+1 regions were null)

Key findings:

• Completive coercion consistently shows processing cost (Exps 1b, 2)
• Inchoative coercion in after-clauses shows delayed cost (Exp 4)
• Inchoative coercion in within-modifier contexts shows no cost (Exps 1a, 3)
• Complement coercion (sanity check) replicates across all experiments
• Delayed spillover (verb+2) in connective contexts vs verb+1 in modifier contexts may reflect pragmatic vs semantic coercion (§5.3, §7.3)

@[reducible, inline]

abbrev SelfPacedReading.Region : Type

Offset from a designated critical region ("the effect appeared at verb+1"): 0 is the critical region; positive offsets are spillover regions; negative offsets are precritical regions. Int rather than an enum: negative offsets and arithmetic come for free. Formerly the Processing/SelfPacedReading.lean paradigm vocabulary, demoted to its sole consumer.

Equations

• SelfPacedReading.Region = ℤ

def SelfPacedReading.Region.critical : Region

The designated critical region of the stimulus.

Equations

• SelfPacedReading.Region.critical = 0

def SelfPacedReading.Region.spillover (n : ℕ) : Region

The n-th spillover region (post-critical).

Equations

• SelfPacedReading.Region.spillover n = ↑n

def SelfPacedReading.Region.precritical (n : ℕ) : Region

The n-th precritical region (pre-critical).

Equations

• SelfPacedReading.Region.precritical n = -↑n

inductive AlstottAravind2026.Experiment : Type

Experiment identifiers. Exp 1 has two sub-experiments (a and b).

• exp1a : Experiment
• exp1b : Experiment
• exp2 : Experiment
• exp3 : Experiment
• exp4 : Experiment

@[instance_reducible]

instance AlstottAravind2026.instDecidableEqExperiment : DecidableEq Experiment

Equations

• AlstottAravind2026.instDecidableEqExperiment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlstottAravind2026.instReprExperiment.repr : Experiment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlstottAravind2026.instReprExperiment : Repr Experiment

Equations

• AlstottAravind2026.instReprExperiment = { reprPrec := AlstottAravind2026.instReprExperiment.repr }

@[instance_reducible]

instance AlstottAravind2026.instInhabitedExperiment : Inhabited Experiment

Equations

• AlstottAravind2026.instInhabitedExperiment = { default := AlstottAravind2026.instInhabitedExperiment.default }

inductive AlstottAravind2026.CoercionType : Type

Types of aspectual coercion tested across experiments.

• inchoative : CoercionType
• completive : CoercionType
• complement : CoercionType

@[instance_reducible]

instance AlstottAravind2026.instDecidableEqCoercionType : DecidableEq CoercionType

Equations

• AlstottAravind2026.instDecidableEqCoercionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlstottAravind2026.instReprCoercionType : Repr CoercionType

Equations

• AlstottAravind2026.instReprCoercionType = { reprPrec := AlstottAravind2026.instReprCoercionType.repr }

def AlstottAravind2026.instReprCoercionType.repr : CoercionType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlstottAravind2026.instInhabitedCoercionType : Inhabited CoercionType

Equations

• AlstottAravind2026.instInhabitedCoercionType = { default := AlstottAravind2026.instInhabitedCoercionType.default }

structure AlstottAravind2026.ExperimentResult : Type

Result from a self-paced reading experiment.

Region uses SelfPacedReading.Region (offset from the designated critical region): Region.critical is the verb, Region.spillover 1 is verb+1, Region.spillover 2 is verb+2.

• experiment : Experiment
• condition : String
• coercionType : CoercionType
• effectBeta : Rat

  Mixed-effects regression coefficient (log RT)

• se : Rat

  Standard error of the coefficient

• pValue : Rat

  p-value

• region : SelfPacedReading.Region

  Region (offset from critical verb) where effect was measured

• significant : Bool

  Whether the effect reached significance (Bonferroni-corrected α = 0.025)

• exploratory : Bool

  Whether the analysis was exploratory (not pre-registered)

def AlstottAravind2026.instReprExperimentResult.repr : ExperimentResult → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlstottAravind2026.instReprExperimentResult : Repr ExperimentResult

Equations

• AlstottAravind2026.instReprExperimentResult = { reprPrec := AlstottAravind2026.instReprExperimentResult.repr }

structure AlstottAravind2026.NaturalnessResult : Type

Naturalness rating result (ordinal logistic regression).

• experiment : Experiment
• coercionType : CoercionType
• ratingBeta : Rat

  Regression coefficient for coercion vs control

• se : Rat

  Standard error of the coefficient

• pValue : Rat

  p-value

• significant : Bool

  Significant difference?

def AlstottAravind2026.instReprNaturalnessResult.repr : NaturalnessResult → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlstottAravind2026.instReprNaturalnessResult : Repr NaturalnessResult

Equations

• AlstottAravind2026.instReprNaturalnessResult = { reprPrec := AlstottAravind2026.instReprNaturalnessResult.repr }

def AlstottAravind2026.exp1a_rt : ExperimentResult

Exp 1a: INCHOAT with within-modifier + be-stative verb. E.g. "Within fifteen minutes Jessica was mad in office hours." No significant RT slowdown; no naturalness difference.

Equations

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

def AlstottAravind2026.exp1a_naturalness : NaturalnessResult

Equations

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

def AlstottAravind2026.exp1b_rt : ExperimentResult

Exp 1b: COMPLET with at-modifier + accomplishment verb. E.g. "At 9pm sharp Hector built the humble tent." Significant slowdown at verb+1; lower naturalness. Supports Rett's COMPLET operator.

Equations

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

def AlstottAravind2026.exp1b_naturalness : NaturalnessResult

Equations

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

def AlstottAravind2026.exp2_rt : ExperimentResult

Exp 2: COMPLET in before-clause with accomplishment EE. E.g. "Emma was irritable before Hector built the tent in the woods." Pre-registered regions (verb, verb+1) showed null effects. Exploratory verb+2 analysis found significant slowdown; lower naturalness. Delayed effect consistent with pragmatic (vs semantic) coercion.

Equations

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

def AlstottAravind2026.exp2_naturalness : NaturalnessResult

Equations

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

def AlstottAravind2026.exp3_rt : ExperimentResult

Exp 3: INCHOAT with subject-experiencer verbs in within-modifier context. E.g. "Within fifteen minutes Jessica tolerated the unhelpful professor." No significant RT effect; no naturalness difference.

Equations

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

def AlstottAravind2026.exp3_naturalness : NaturalnessResult

Equations

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

def AlstottAravind2026.exp4_rt : ExperimentResult

Exp 4: INCHOAT in after-clause with subject-experiencer EE. E.g. "Dave was regretful after Lara feared the large dog." Pre-registered regions (verb, verb+1) showed null effects. Exploratory verb+2 analysis found significant slowdown; lower naturalness. INCHOAT cost detected in after-clauses but not within-modifier contexts.

Equations

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

def AlstottAravind2026.exp4_naturalness : NaturalnessResult

Equations

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

def AlstottAravind2026.complement_coercion_exp1a : ExperimentResult

Complement coercion (e.g., "continued his article") in Exp 1a at noun+1. This replicates across all experiments, confirming paradigm sensitivity.

Equations

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

def AlstottAravind2026.complement_coercion_exp1b : ExperimentResult

Complement coercion in Exp 1b at noun+1.

Equations

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

def AlstottAravind2026.complement_coercion_exp3 : ExperimentResult

Complement coercion in Exp 3 at noun+1.

Equations

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

theorem AlstottAravind2026.rett_predicts_completive_cost : exp1b_rt.significant = true ∧ exp2_rt.significant = true

Rett's theory correctly predicts completive coercion costs where they occur. Both Exps 1b (at-modifier) and 2 (before-clause) show significant slowdowns.

theorem AlstottAravind2026.rett_predicts_inchoative_in_after : exp4_rt.significant = true ∧ exp4_rt.coercionType = CoercionType.inchoative

Rett's theory correctly predicts inchoative coercion cost in after-clauses. Exp 4 shows significant slowdown for after-start readings.

theorem AlstottAravind2026.within_modifier_not_replicated : exp1a_rt.significant = false ∧ exp3_rt.significant = false

Within-modifier INCHOAT shows no cost: Exps 1a and 3 show null results. This dissociation (null in within-modifier, significant in after-clause) suggests INCHOAT cost is construction-specific, not universal. The paper's §8.2 proposes a non-coercive, Krifka-style scalar implicature analysis for atelic within-modifier sentences.

theorem AlstottAravind2026.complement_coercion_replicates : complement_coercion_exp1a.significant = true ∧ complement_coercion_exp1b.significant = true ∧ complement_coercion_exp3.significant = true

Complement coercion sanity check passes in both sub-experiments.

Processing measure: all experiments use self-paced reading; the dependent variable is log-transformed reading time (ms).

theorem AlstottAravind2026.connective_vs_modifier_spillover : exp2_rt.region = SelfPacedReading.Region.spillover 2 ∧ exp2_rt.exploratory = true ∧ exp4_rt.region = SelfPacedReading.Region.spillover 2 ∧ exp4_rt.exploratory = true ∧ exp1b_rt.region = SelfPacedReading.Region.spillover 1 ∧ exp1b_rt.exploratory = false

Delayed effect in connective contexts: cost at verb+2 (not verb+1). Both connective experiments (2, 4) show verb+2 spillover, while the modifier experiment (1b) shows verb+1. Consistent with pragmatic coercion in connectives being slower to detect than semantic coercion in modifier contexts. Both connective results are exploratory.

theorem AlstottAravind2026.exp2_tests_before_coercion : exp2_rt.coercionType = CoercionType.completive ∧ English.TemporalExpressions.before_.coercedReading = some English.TemporalExpressions.Reading.beforeFinish

Exp 2 tests the Fragment's coercedReading for before: COMPLET triggers the before-finish reading.

theorem AlstottAravind2026.exp4_tests_after_coercion : exp4_rt.coercionType = CoercionType.inchoative ∧ English.TemporalExpressions.after_.coercedReading = some English.TemporalExpressions.Reading.afterStart

Exp 4 tests the Fragment's coercedReading for after: INCHOAT triggers the after-start reading.

theorem AlstottAravind2026.exp1b_tests_at_modifier_coercion : exp1b_rt.coercionType = CoercionType.completive ∧ English.TemporalExpressions.at_punct.triggeredCoercion = some "COMPLET"

theorem AlstottAravind2026.exp1a_tests_within_modifier_coercion : exp1a_rt.coercionType = CoercionType.inchoative ∧ English.TemporalExpressions.within_.triggeredCoercion = some "INCHOAT"

theorem AlstottAravind2026.complet_consistently_costly : exp1b_rt.significant = true ∧ exp2_rt.significant = true ∧ exp1b_rt.coercionType = CoercionType.completive ∧ exp2_rt.coercionType = CoercionType.completive

COMPLET is consistently costly across both completive experiments.

theorem AlstottAravind2026.inchoat_construction_specific : exp4_rt.significant = true ∧ exp1a_rt.significant = false ∧ exp3_rt.significant = false ∧ exp4_rt.coercionType = CoercionType.inchoative ∧ exp1a_rt.coercionType = CoercionType.inchoative ∧ exp3_rt.coercionType = CoercionType.inchoative

INCHOAT cost is construction-specific: present in after-clauses (Exp 4), absent in within-modifier contexts (Exps 1a, 3).

theorem AlstottAravind2026.complet_effect_exceeds_inchoat : exp1b_rt.effectBeta > exp1a_rt.effectBeta

Completive effect size exceeds inchoative in modifier contexts.

theorem AlstottAravind2026.rt_naturalness_converge : exp1b_rt.significant = exp1b_naturalness.significant ∧ exp2_rt.significant = exp2_naturalness.significant ∧ exp4_rt.significant = exp4_naturalness.significant ∧ exp1a_rt.significant = exp1a_naturalness.significant ∧ exp3_rt.significant = exp3_naturalness.significant

RT significance and naturalness significance converge in all 5 experiments: every experiment that shows an RT effect also shows a naturalness effect, and every null RT result has a null naturalness result.

theorem AlstottAravind2026.tagalog_overt_coercion : Tagalog.TemporalConnectives.bago_aia.culminating = true ∧ Tagalog.TemporalConnectives.bago_aia.reading = English.TemporalExpressions.Reading.beforeFinish ∧ Tagalog.TemporalConnectives.bago_neut.culminating = false ∧ Tagalog.TemporalConnectives.bago_neut.reading = English.TemporalExpressions.Reading.beforeStart

Tagalog overtly marks what English coerces covertly: PFV.AIA (ability/involuntary action) → before-finish (COMPLET); PFV.NEUT (neutral) → before-start (no coercion).

theorem AlstottAravind2026.serbian_overt_coercion : Serbian.TemporalConnectives.pre_pfv.culminating = true ∧ Serbian.TemporalConnectives.pre_pfv.reading = English.TemporalExpressions.Reading.beforeFinish ∧ Serbian.TemporalConnectives.pre_impf.culminating = false ∧ Serbian.TemporalConnectives.pre_impf.reading = English.TemporalExpressions.Reading.beforeStart

Serbian overtly marks what English coerces covertly: perfective → before-finish (COMPLET); imperfective → before-start (no coercion).

theorem AlstottAravind2026.complet_triple_convergence : exp2_rt.significant = true ∧ exp2_rt.coercionType = CoercionType.completive ∧ Tagalog.TemporalConnectives.bago_aia.culminating = true ∧ Serbian.TemporalConnectives.pre_pfv.culminating = true

Triple convergence: English processing data (Exp 2), Tagalog morphology, and Serbian morphology all independently support covert COMPLET.

inductive AlstottAravind2026.RivalAccount : Type

Rival accounts of before/after readings compared by the paper. Only [Ret20]'s ambiguity account posits covert aspectual operators (INCHOAT/COMPLET); under-specification accounts ([Ans64], [Kri10]) and intensional accounts ([BC03], [OST24]) derive the non-default readings from a single lexical entry without covert operators.

• ambiguity : RivalAccount
• underspecification : RivalAccount
• intensional : RivalAccount

@[instance_reducible]

instance AlstottAravind2026.instDecidableEqRivalAccount : DecidableEq RivalAccount

Equations

• AlstottAravind2026.instDecidableEqRivalAccount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlstottAravind2026.instReprRivalAccount.repr : RivalAccount → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlstottAravind2026.instReprRivalAccount : Repr RivalAccount

Equations

• AlstottAravind2026.instReprRivalAccount = { reprPrec := AlstottAravind2026.instReprRivalAccount.repr }

def AlstottAravind2026.RivalAccount.positsCoercion : RivalAccount → Bool

Does the account posit covert coercion operators — and with them a measurable processing cost for non-default readings? This is the empirical discriminator the paper's four experiments test.

Equations

• AlstottAravind2026.RivalAccount.ambiguity.positsCoercion = true
• AlstottAravind2026.RivalAccount.underspecification.positsCoercion = false
• AlstottAravind2026.RivalAccount.intensional.positsCoercion = false

theorem AlstottAravind2026.data_supports_rett : RivalAccount.ambiguity.positsCoercion = true ∧ exp1b_rt.significant = true ∧ exp2_rt.significant = true ∧ exp4_rt.significant = true

The data confirm the ambiguity account's distinctive prediction: significant processing costs exist for coerced readings (Exps 1b, 2, 4), which only a coercion-positing account predicts.

theorem AlstottAravind2026.coercion_has_crosslinguistic_reflexes : RivalAccount.ambiguity.positsCoercion = true ∧ Tagalog.TemporalConnectives.bago_aia.culminating = true ∧ Serbian.TemporalConnectives.pre_pfv.culminating = true

Rett's coercion operators have overt cross-linguistic reflexes: the theory posits coercion, and languages like Tagalog and Serbian realize it morphologically.