Documentation

Linglib.Phenomena.TenseAspect.Diagnostics

Aspectual Diagnostics #

@cite{vendler-1957} @cite{dowty-1979}

Empirical tests for determining aspectual class. The for-X and in-X adverbial, progressive, stop-V-ing, and imperative diagnostics formalized here are the textbook tests originating with Vendler 1957 (the four-class taxonomy) and Dowty 1979 (the syntactic-test battery). Anchored on a documented empirical pattern (per CLAUDE.md anchoring rule), not on a specific paper-replication.

Core Tests #

Test	States	Activities	Achievements	Accomplishments
"for X"	✓	✓	✗	?
"in X"	✗	✗	✓	✓
Progressive	?	✓	?	✓
"stop V-ing"	?	✓	?	✓
Imperative	✗	✓	?	✓

"For X" vs "In X" Tests #

The classic tests from @cite{vendler-1957} and @cite{dowty-1979}:

"for an hour" — compatible with atelic predicates
- "John ran for an hour" ✓ (activity)
- "John knew French for ten years" ✓ (state)
- *"John recognized Mary for an hour" ✗ (achievement)
- ?"John built the house for a year" — coerced to activity
"in an hour" — compatible with telic predicates
- *"John ran in an hour" ✗ (activity, unless goal implied)
- "John built the house in a year" ✓ (accomplishment)
- "John recognized Mary in a second" ✓ (achievement)
- *"John knew French in ten years" ✗ (state)

Progressive Test #

Activities and accomplishments take the progressive naturally
States typically resist the progressive (*"John is knowing French")
Achievements take the progressive with special interpretations:
- Slow-motion: "The bomb is exploding" (stretched out)
- Preliminary stages: "John is dying" (process leading to death)

inductive Phenomena.TenseAspect.Diagnostics.DiagnosticResult :

Result of applying a diagnostic test.

Accept: Test is felicitous (grammatical, acceptable)
Reject: Test is infelicitous (ungrammatical, unacceptable)
Marginal: Test is degraded but not completely out
Coerced: Test is acceptable but requires meaning shift

Instances For

@[implicit_reducible]

instance Phenomena.TenseAspect.Diagnostics.instDecidableEqDiagnosticResult :

DecidableEq DiagnosticResult

Equations

Phenomena.TenseAspect.Diagnostics.instDecidableEqDiagnosticResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult :

Repr DiagnosticResult

Equations

Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult = { reprPrec := Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult.repr }

def Phenomena.TenseAspect.Diagnostics.instReprDiagnosticResult.repr :

DiagnosticResult → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.DiagnosticResult.fromBool :

Bool → DiagnosticResult

Convert Bool prediction to DiagnosticResult.

Equations

Instances For

def Phenomena.TenseAspect.Diagnostics.forXPrediction :

Features.VendlerClass → DiagnosticResult

Prediction for "for X" adverbial compatibility.

"For X" measures the duration of an atelic (unbounded) eventuality:

"ran for an hour" ✓
"knew French for ten years" ✓
*"arrived for an hour" ✗
?"built the house for a year" — coerces to repetitive

States and activities accept "for X" straightforwardly. Achievements reject "for X" (no duration to measure). Accomplishments can accept "for X" but with coercion to activity/repetition.

Equations

Instances For

theorem Phenomena.TenseAspect.Diagnostics.forX_identifies_atelic (c : Features.VendlerClass) :

forXPrediction c = DiagnosticResult.accept ↔ c = Features.VendlerClass.state ∨ c = Features.VendlerClass.activity

The "for X" test identifies atelic predicates.

States and activities pass; achievements fail; accomplishments require coercion.

def Phenomena.TenseAspect.Diagnostics.inXPrediction :

Features.VendlerClass → DiagnosticResult

Prediction for "in X" adverbial compatibility.

"In X" measures time to reach a culmination point:

*"ran in an hour" ✗ (no endpoint to reach)
"arrived in an hour" ✓ (punctual, endpoint reached)
"built the house in a year" ✓ (durative, endpoint reached)
*"knew French in ten years" ✗ (no endpoint, state)

Only telic predicates have a culmination point to measure.

Equations

Instances For

theorem Phenomena.TenseAspect.Diagnostics.inX_identifies_telic (c : Features.VendlerClass) :

inXPrediction c = DiagnosticResult.accept ↔ c.telicity = Features.Telicity.telic

The "in X" test identifies telic predicates.

Achievements and accomplishments pass; states and activities fail.

def Phenomena.TenseAspect.Diagnostics.progressivePrediction :

Features.VendlerClass → DiagnosticResult

Prediction for progressive compatibility.

The progressive requires ongoing, dynamic eventualities:

"John is running" ✓ (activity — paradigmatic)
"John is building a house" ✓ (accomplishment — in progress)
*"John is knowing French" ✗ (state — no stages)
?"John is arriving" — marginal (achievement, requires interpretation)

States generally reject the progressive (no stages, no development). Achievements take the progressive marginally (slow-motion, preliminary).

Equations

Instances For

theorem Phenomena.TenseAspect.Diagnostics.progressive_accepts_durative_dynamic (c : Features.VendlerClass) :

progressivePrediction c = DiagnosticResult.accept ↔ c.duration = Features.Duration.durative ∧ c.dynamicity = Features.Dynamicity.dynamic

The progressive test distinguishes dynamic and durative predicates.

Activities and accomplishments clearly accept; states reject; achievements are marginal.

def Phenomena.TenseAspect.Diagnostics.stopVingPrediction :

Features.VendlerClass → DiagnosticResult

Prediction for "stop V-ing" compatibility.

"Stop V-ing" presupposes an ongoing activity that ceases:

"John stopped running" ✓ (activity)
"John stopped building the house" ✓ (accomplishment, activity in progress)
?"John stopped knowing French" — marginal (states don't "stop")
?"John stopped recognizing her" — requires iterative reading

This test identifies predicates with internal duration/stages.

Equations

Instances For

def Phenomena.TenseAspect.Diagnostics.imperativePrediction :

Features.VendlerClass → DiagnosticResult

Prediction for imperative compatibility.

Imperatives require agentive control:

"Run!" ✓ (activity)
"Build a house!" ✓ (accomplishment)
*"Know French!" ✗ (state, not controllable)
?"Recognize her!" — marginal (achievement, not directly controllable)

Equations

Instances For

structure Phenomena.TenseAspect.Diagnostics.DiagnosticBattery :

Result of running all diagnostic tests on a Vendler class.

forX : DiagnosticResult
inX : DiagnosticResult
progressive : DiagnosticResult
stopVing : DiagnosticResult
imperative : DiagnosticResult

Instances For

@[implicit_reducible]

instance Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery :

Repr DiagnosticBattery

Equations

Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery = { reprPrec := Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery.repr }

def Phenomena.TenseAspect.Diagnostics.instReprDiagnosticBattery.repr :

DiagnosticBattery → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery :

BEq DiagnosticBattery

Equations

Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery = { beq := Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery.beq }

def Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery.beq :

DiagnosticBattery → DiagnosticBattery → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.TenseAspect.Diagnostics.instBEqDiagnosticBattery.beq x✝¹ x✝ = false

Instances For

def Phenomena.TenseAspect.Diagnostics.runDiagnostics (c : Features.VendlerClass) :

DiagnosticBattery

Run all diagnostics for a Vendler class.

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.stateDiagnostics :

DiagnosticBattery

Expected diagnostic battery for states.

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.activityDiagnostics :

DiagnosticBattery

Expected diagnostic battery for activities.

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.achievementDiagnostics :

DiagnosticBattery

Expected diagnostic battery for achievements.

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.accomplishmentDiagnostics :

DiagnosticBattery

Expected diagnostic battery for accomplishments.

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.semelfactiveDiagnostics :

DiagnosticBattery

Expected diagnostic battery for semelfactives.

Equations

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

Instances For

theorem Phenomena.TenseAspect.Diagnostics.diagnostics_correct (c : Features.VendlerClass) :

runDiagnostics c = match c with | Features.VendlerClass.state => stateDiagnostics | Features.VendlerClass.activity => activityDiagnostics | Features.VendlerClass.achievement => achievementDiagnostics | Features.VendlerClass.accomplishment => accomplishmentDiagnostics | Features.VendlerClass.semelfactive => semelfactiveDiagnostics

Running diagnostics on each class gives the expected battery.

structure Phenomena.TenseAspect.Diagnostics.VerbAspectData :

Attested aspectual data for sample verbs.

verbLemma : String
Verb lemma
vendlerClass : Features.VendlerClass
Assigned Vendler class
forXExample : String
Example sentence for "for X"
forXJudgment : DiagnosticResult
Judgment for "for X"

Instances For

def Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData.repr :

VerbAspectData → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData :

Repr VerbAspectData

Equations

Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData = { reprPrec := Phenomena.TenseAspect.Diagnostics.instReprVerbAspectData.repr }

def Phenomena.TenseAspect.Diagnostics.runData :

"run" — activity

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.knowData :

"know" — state

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.buildData :

"build" — accomplishment

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.arriveData :

"arrive" — achievement

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.recognizeData :

"recognize" — achievement

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.loveData :

"love" — state

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.writeData :

"write" — accomplishment (with bounded object)

Equations

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

Instances For

def Phenomena.TenseAspect.Diagnostics.allVerbData :

List VerbAspectData

All sample verb data

Equations

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

Instances For

The diagnostic predictions above are hand-coded per class. These derivation theorems show they are consequences of Smith's 3-feature decomposition, not independent stipulations.

theorem Phenomena.TenseAspect.Diagnostics.inX_from_telicity (c : Features.VendlerClass) :

inXPrediction c = DiagnosticResult.accept ↔ c.telicity = Features.Telicity.telic

"in X" acceptance is equivalent to telicity. This is the content of inX_identifies_telic, but stated purely in terms of the feature function — the diagnostic follows from the telicity feature.

theorem Phenomena.TenseAspect.Diagnostics.forX_from_features (c : Features.VendlerClass) :

forXPrediction c = DiagnosticResult.accept ↔ c.telicity = Features.Telicity.atelic ∧ c.duration = Features.Duration.durative

"for X" acceptance is equivalent to atelicity + duration. Semelfactives are atelic but only accept "for X" with coercion (because they are punctual — no duration to measure). The diagnostic follows from two features, not from the class label.

theorem Phenomena.TenseAspect.Diagnostics.forX_semelfactive_coercion :

forXPrediction Features.VendlerClass.semelfactive = DiagnosticResult.coerced ∧ Features.VendlerClass.semelfactive.telicity = Features.Telicity.atelic ∧ Features.VendlerClass.semelfactive.duration = Features.Duration.punctual

Semelfactive coercion under "for X" derives from being atelic but punctual: atelicity licenses temporal modification, but punctuality forces iterative reinterpretation.

theorem Phenomena.TenseAspect.Diagnostics.progressive_from_features (c : Features.VendlerClass) :

progressivePrediction c = DiagnosticResult.accept ↔ c.dynamicity = Features.Dynamicity.dynamic ∧ c.duration = Features.Duration.durative

Progressive acceptance is equivalent to being durative and dynamic. States fail (not dynamic); achievements/semelfactives fail (not durative).