Degree achievements: the adjectival core of telicity #
Formalisation of [KL08], which derives the telicity of degree achievement verbs (widen, cool, straighten, ...) from the boundedness of the scale lexicalised by their adjectival base: a closed-scale base yields a telic (accomplishment) verb, an open-scale base an atelic (activity) verb.
Main results #
*_derived_vendler/da_vendler_classes_agree— each verb's stipulated Vendler class agrees with the class derived from itsdegreeAchievementScale.*_scale— each degree-achievement verb shares its adjectival base's scale boundedness, including the boil case where the verb selects a bounded portion of an otherwise open scale.*_inX/*_forX— telicity-diagnostic predictions: closed-scale verbs accept in X, open-scale verbs accept for X.*_pipeline_converge— the scale-based and Vendler-based licensing pipelines agree on boundedness.- The order-theoretic core (
telic_of_orderTop/atelic_of_noMaxOrder, below): a degree achievement admits a Quantized (telic) witness iff its scale has a greatest degree, via mathlib'sOrderTop/NoMaxOrdermixins (witnessg_φ = ⊤), feeding [Bea11]'s affectedness hierarchy. Here it is instantiated at the dimensions the verbs measure —straighten_telic(straightness, closed),widen_atelic(width, open) — grounded to the verbs' stored dimensions bystraighten_dimension/widen_dimension. The variable-telicity contrast of [KL08] §3.3.
Implementation notes #
The scale annotations and Vendler classes consumed here live on the English
verbal/adjectival fragment entries; the derivations they are checked against
live in Semantics/Aspect/DegreeAchievement.lean, and the affectedness
typeclass chain in Semantics/ArgumentStructure/Affectedness.lean.
Per-verb derived Vendler class #
For each degree achievement verb, the Vendler class stipulated in the fragment
matches the class DegreeAchievementScale.defaultVendlerClass derives from the
verb's scale boundedness.
"bend": closed scale → accomplishment (derived = stipulated).
"boil": closed scale → accomplishment (derived = stipulated).
"rust": open scale → activity (derived = stipulated).
"increase": open scale → activity (derived = stipulated).
"clean": closed scale → accomplishment (derived = stipulated).
"straighten": closed scale → accomplishment (derived = stipulated).
"flatten": closed scale → accomplishment (derived = stipulated).
"open": closed scale → accomplishment (derived = stipulated).
"lengthen": open scale → activity (derived = stipulated).
"widen": open scale → activity (derived = stipulated).
"cool": open scale → activity (derived = stipulated).
"warm": open scale → activity (derived = stipulated).
The degree-achievement verbs whose telicity this file derives from scale boundedness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The invariant the per-verb *_derived_vendler lemmas witness, stated once:
every degree-achievement verb's stipulated Vendler class equals the class
derived from its scale boundedness. A drift sentry — adding a verb whose
annotations disagree breaks this.
Adjective–verb scale agreement #
For each adjective–verb pair, the verb's degreeAchievementScale.scaleBoundedness
matches the adjective's scaleType: the verb inherits the scale classification
of its adjectival base.
clean (adj, closed) ↔ clean (verb, closed scale).
straight (adj, closed) ↔ straighten (verb, closed scale).
flat (adj, closed) ↔ flatten (verb, closed scale).
open (adj, closed) ↔ open (verb, closed scale).
long (adj, open) ↔ lengthen (verb, open scale).
wide (adj, open) ↔ widen (verb, open scale).
cool (adj, open) ↔ cool (verb, open scale).
warm (adj, open) ↔ warm (verb, open scale).
hot (adj, open) vs boil (verb, closed at the boiling point). boil selects a conventionalised endpoint (the boiling point) despite the open scale of its base adjective hot. This fragment annotation extends [KL08]'s treatment of cool, whose conventionalised 'room-temperature' standard licenses a telic reading from an open-scale base (§3.3); [KL08] do not themselves discuss boil.
Telicity-diagnostic predictions #
Closed-scale degree achievements accept in X (telic); open-scale ones accept for X (atelic).
Closed-scale verbs accept in X #
"bent the wire in 5 seconds" — closed-scale DA accepts "in X".
"boiled the water in 3 minutes" — closed-scale DA accepts "in X".
"cleaned the table in 5 minutes" — closed-scale DA accepts "in X".
"straightened the wire in 10 seconds" — closed-scale DA accepts "in X".
"flattened the dough in 2 minutes" — closed-scale DA accepts "in X".
"opened the door in 3 seconds" — closed-scale DA accepts "in X".
Open-scale verbs accept for X #
"rusted for years" — open-scale DA accepts "for X".
"increased for months" — open-scale DA accepts "for X".
"lengthened the rope for hours" — open-scale DA accepts "for X".
"widened the road for months" — open-scale DA accepts "for X".
"cooled for an hour" — open-scale DA accepts "for X".
"warmed for an hour" — open-scale DA accepts "for X".
Pipeline convergence #
LicensingPipeline.toBoundedness agrees whether applied to the verb's
degreeAchievementScale or to its vendlerClass — the scale-based and
Vendler-based routes to boundedness converge.
"bend": DA pipeline → closed = VendlerClass pipeline → closed.
"boil": DA pipeline → closed = VendlerClass pipeline → closed.
"rust": DA pipeline → open = VendlerClass pipeline → open.
"increase": DA pipeline → open = VendlerClass pipeline → open.
"clean": DA pipeline → closed = VendlerClass pipeline → closed.
"straighten": DA pipeline → closed = VendlerClass pipeline → closed.
"flatten": DA pipeline → closed = VendlerClass pipeline → closed.
"open": DA pipeline → closed = VendlerClass pipeline → closed.
"lengthen": DA pipeline → open = VendlerClass pipeline → open.
"widen": DA pipeline → open = VendlerClass pipeline → open.
"cool": DA pipeline → open = VendlerClass pipeline → open.
"warm": DA pipeline → open = VendlerClass pipeline → open.
Substrate demonstration: telicity from scale order #
The order-theoretic account of [KL08]'s thesis (formalized below):
a degree achievement is telic iff its scale has a greatest degree (OrderTop),
with the Quantized witness g_φ = ⊤,
feeding [Bea11]'s affectedness hierarchy. Here it is instantiated at the
dimensions the K&L verbs measure.
Telicity from the scale's order structure (order-theoretic K&L thesis) #
The telic reading is "the patient reaches the maximal degree ⊤", available only
on a scale with a greatest element (OrderTop); the atelic reading is "reaches
some degree", always satisfiable. So telicity is a Quantized-witness existence
fact over the dimension's degree fiber, derived from the order mixin — not a
stored flag. The Dimension carrier lives in Semantics/Gradability/Dimension.lean;
the event machinery below is specific to this paper's degree-achievement analysis.
Trivial patient: the measure of change ignores the patient's identity, so a
single one-constructor type serves for every degree type δ.
- mk : Patient
Instances For
The patient's degree at a time is that time — the temporal trace — so the final degree of an event is its end-time.
Equations
- KennedyLevin2008.traceMeasure = { measure := fun (x : KennedyLevin2008.Patient) (t : δ) => t }
Companion HasLatentScale ([Bea11] eq. (60c)).
The forgetful link holds in this model: latentScale is True.
Telic reading: the patient reaches the maximal degree ⊤ by the event's end.
Equations
- KennedyLevin2008.reachesTop x✝ e = (e.runtime.toProd.2 = ⊤)
Instances For
Atelic ('comparative') reading: the patient reaches some degree by the end.
Equations
- KennedyLevin2008.reachesSome x✝ e = ∃ (g : δ), e.runtime.toProd.2 = g
Instances For
Telic ⇐ a greatest degree. OrderTop supplies the Quantized witness
g_φ = ⊤ — the order-theoretic content of [KL08]'s closed-scale
telicity.
Telic ⇒ a greatest degree (contrapositive). With no greatest degree
(NoMaxOrder), no final degree is entailed — [KL08]'s open-scale
obligatory atelicity, derived from the order structure.
Synthesis: with a greatest degree, the telic reading builds the Beavers
IsQuantizedAffected instance ([Bea11] eq. (62)); the weaker
mixins follow by derivation.
Equations
- KennedyLevin2008.reachesTop_isQuantizedAffected = { finalDegree := ⊤, isQuantized := ⋯ }
straighten measures straightness — a closed scale — so a telic reading is
available, derived from the dimension's OrderTop (not a stored HasMax).
widen measures width — unbounded above — so no telic reading exists.
The fragment stores each verb's dimension directly (boundedness is derived):
straighten measures straightness, widen width — so straighten_telic /
widen_atelic above apply to the actual lexical entries.
Telicity at the AffectednessDegree level #
The [KL08] to [Bea11] telicity correspondence at the
AffectednessDegree level: a closed-scale base (straighten) projects to
.quantized (telic), an open-scale base (widen) to .nonquantized
(atelic). The strict ordering encodes the variable-telicity contrast.