Degree Achievements #
@cite{kennedy-levin-2008}
@cite{kennedy-levin-2008}: the telicity of degree achievements is derived from the boundedness of the underlying adjectival scale. This bridge file verifies that the fragment annotations are consistent with that derivation.
§1 — Per-verb derived vendlerClass verification
§2 — Adjective-verb scale agreement
§3 — Telicity diagnostic predictions
§4 — Pipeline convergence
§5 — Substrate-level demonstration: K&L 2008 measure-of-change m_Δ
(eq. 25) → Beavers' affectedness typeclass chain. First production
[HasMeasureFunction] instances in linglib; validates the auto-
synthesis arrow [HasMeasureFunction] → HasScalarResult → IsXAffected end-to-end on closed-scale (straighten) and
open-scale (widen) toys.
- Kennedy, C. & Levin, B. (2007). Measure of change: The adjectival core of degree achievements. In L. McNally & C. Kennedy (eds.), Adjectives and Adverbs, 156–182. OUP.
For each degree achievement verb, the vendlerClass stipulated in the fragment matches what degreeAchievementScale.defaultVendlerClass derives.
"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).
For each adj-verb pair, the verb's degreeAchievementScale.scaleBoundedness matches the adjective's scaleType. This ensures the verb inherits the correct scale classification from 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) ↔ boil (verb, closed scale for boiling point). Note: boil reaches a closed endpoint (boiling point) even though the base adjective "hot" has an open scale. @cite{kennedy-levin-2008} notes that the verb selects the relevant portion of the scale.
Closed-scale DAs accept "in X" (telic prediction). Open-scale DAs accept "for X" (atelic prediction).
"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".
"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".
LicensingPipeline.toBoundedness applied to the verb's degreeAchievementScale matches LicensingPipeline.toBoundedness applied to the verb's vendlerClass.
"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.
K&L 2008's measure-of-change function m_Δ (eq. 25), formalised in
Theories/Semantics/Degree/MeasureFunction.lean, plugs directly
into Beavers' affectedness typeclass chain
(Theories/Semantics/Events/Scalar/Affectedness.lean).
This section provides the **first production `[HasMeasureFunction]`
instances in linglib** — toy domains for *straighten* (closed
scale, max = 1) and *widen* (open scale, no max) — and demonstrates
that the auto-synthesis arrow
`[HasMeasureFunction α δ Time] → HasScalarResult α δ (Event Time)`
fires structurally. Downstream `IsQuantizedAffected.mk'` /
`IsNonQuantizedAffected.mk'` smart constructors find the
`HasScalarResult` instance by typeclass resolution without explicit
naming.
The variable-telicity prediction (K&L §7.3.3) is realised
structurally: closed-scale DAs construct an `IsQuantizedAffected`
instance at `g_φ = scale max`; open-scale DAs only have an
`IsNonQuantizedAffected` instance available (no Quantized witness
exists because the scale lacks a maximum).
Toy types `RodToy` and `GapToy` are used (rather than fragment
`Rod`/`Gap` if those exist) to keep the substrate demonstration
self-contained. The fragment-level §1-4 results above are
independent of this substrate work.
Toy time type for the substrate demonstration.
Equations
Instances For
Toy patient type for the substrate-level straighten demonstration. The actual identity of rods is irrelevant; what matters is the measure of straightness over time.
Equations
- KennedyLevin2008.RodToy = Unit
Instances For
Toy straight measure function on a closed scale (ℚ with
max = 1, representing complete straightness per K&L footnote 8 /
eq. 20). Returns the constant 1 — every rod is fully straight at
every time, so θ_straighten_toy (defined below) is provably
Quantized at g_φ = 1 without case analysis on rod-time pairs.
A real K&L instantiation would track actual straightness as a function of rod geometry and time.
Equations
- KennedyLevin2008.straightMeasure = { measure := fun (x : KennedyLevin2008.RodToy) (x_1 : KennedyLevin2008.SubstrateTime) => 1 }
Companion HasLatentScale — straighten commits to the
straightness scale, making rods force-recipients on it
per Beavers (60c). Manual call to
HasLatentScale.ofHasMeasureFunction since auto-synthesis isn't
available (δ-inference issue documented in
Degree/MeasureFunction.lean).
straighten's θ-relation: rod x is straightened in event e
iff x has straightness 1 at the end of e. K&L eq. 20: "x
undergoes a change from non-maximal to maximal straightness".
The toy entails only the maximal-end condition.
Equations
Instances For
straighten is Quantized at g_φ = 1 (K&L's telic prediction
for closed-scale DAs): every straightening event ends with the
patient at maximum straightness.
The full IsQuantizedAffected instance for straighten. The
HasScalarResult parameter is found automatically by typeclass
synthesis from the [HasMeasureFunction] instance above — this
is the load-bearing demonstration of the K&L → Beavers
auto-synthesis arrow.
The forget argument is fun _ _ _ => trivial because the
HasLatentScale instance has trivial content (True) per the
ofHasMeasureFunction definition.
Toy patient type for substrate-level widen.
Equations
- KennedyLevin2008.GapToy = Unit
Instances For
Toy wide measure function on an open scale (ℚ with no
maximum, per K&L §7.3.3). Returns t + 1 for time t — any
monotone function works for the substrate demonstration; the
key fact is that the SCALE has no maximum, so no specific g_φ
can witness Quantized.
Equations
- KennedyLevin2008.wideMeasure = { measure := fun (x : KennedyLevin2008.GapToy) (t : KennedyLevin2008.SubstrateTime) => ↑t + 1 }
HasLatentScale companion for widen.
widen's θ-relation: gap x widens in event e iff x has
SOME width at the end of e. K&L's atelic "comparative" reading
— no specific final value entailed.
Equations
- KennedyLevin2008.θ_widen_toy x e = ∃ (g : ℚ), Semantics.Degree.MeasureFunction.HasMeasureFunction.measure x e.runtime.finish = g
Instances For
widen is NonQuantized: every widening event ends with the patient at SOME degree on the wide scale. K&L's atelic "comparative" reading.
The IsNonQuantizedAffected instance for widen.
Per K&L §7.3.3: NO IsQuantizedAffected θ_widen_toy instance is
available (or constructible) — the open scale has no maximum to
instantiate g_φ. The substrate correctly refuses to assert
Quantized affectedness for open-scale DAs, exactly as K&L
predicts.
This is the substrate's empirical bite: the typeclass hierarchy structurally distinguishes closed-scale DAs (Quantized) from open-scale DAs (NonQuantized only), matching K&L's variable telicity prediction without ad-hoc per-verb stipulation.
The K&L 2008 → Beavers 2011 telicity correspondence at the
AffectednessDegree level: closed-scale DAs (straighten)
project to .quantized (telic); open-scale DAs (widen) project
to .nonquantized (atelic). The strict ordering encodes K&L's
variable-telicity prediction structurally.