@cite{hay-kennedy-levin-1999}: Scalar Structure Underlies Telicity in DAs

@cite{hay-kennedy-levin-1999}

HKL 1999's central claim (p.3): "when the scalar structure associated with the base adjective has a natural bound, the derived verb is telic; when the adjective's scalar structure has no such bound, the verb is atelic."

The thesis applies specifically to degree achievements (verbs derived from gradable adjectives — lengthen, cool, straighten). The mechanism is the INCREASE function (eq 16), whose difference value drives telicity: bounded difference → telic; unbounded difference → atelic.

Sections

• §1 — HKL's INCREASE operator (eq 16) + bridge note to K&L 2008's measureOfChange substrate (Theories/Semantics/Degree/MeasureFunction.lean).
• §2 — Central matrix prediction (HKL §3.2): closed-range adjective → telic DA verb; open-range adjective → atelic DA verb. Verified against fragment degreeAchievementScale annotations on straighten (closed → accomplishment) vs lengthen, widen, cool, warm (open → activity).
• §3 — Specifying the difference value (HKL §3.1): measure phrases, completely, significantly/slightly data.
• §4 — Context-dependent telicity (HKL §3.3): defeasibility-via-implicature data.
• §5 — Beyond DAs (HKL §4.1): brief connection to consumption / motion / creation that the analysis extends to.

Relation to KennedyLevin2008.lean

K&L 2008 is the mature successor of HKL 1999. The K&L measureOfChange function (eq 25, in MeasureFunction.lean) refines HKL's INCREASE with explicit clamping at the initial degree (differenceFunction, K&L eq 23). Per-verb derivation of vendlerClass from degreeAchievementScale.scaleBoundedness is in Phenomena/TenseAspect/Studies/KennedyLevin2008.lean. This file focuses on what's specific to HKL 1999: the original INCREASE operator, the §3 data, and the closed/open-range vocabulary HKL introduced (the same distinction Kennedy & McNally 2005 later canonicalized as "closed scale"/"open scale").

Anchoring discipline

§7 of Phenomena/TenseAspect/Studies/Krifka1989.lean (added in 0.230.429) explicitly cites HKL 1999 as the source of the defeasible closed-scale → telic-verb bridge for degree achievements specifically. This file makes that bridge a Lean-checkable matrix on fragment data rather than docstring prose.

@[reducible, inline]

abbrev HayKennedyLevin1999.TimedAdjective (α : Type u_1) (δ : Type u_2) (Time : Type u_3) : Type (max (max u_1 u_2) u_3)

HKL eq 11: [long(x)(t)] = the degree to which x is long at time t. A gradable adjective denotes a time-indexed measure function — the same shape as K&L 2008's MeasureFunction α δ Time in Theories/Semantics/Degree/MeasureFunction.lean.

Equations

• HayKennedyLevin1999.TimedAdjective α δ Time = (α → Time → δ)

def HayKennedyLevin1999.INCREASE {α : Type u_1} {δ : Type u_2} {Time : Type u_3} [Add δ] (φ : TimedAdjective α δ Time) (x : α) (d : δ) (startT finT : Time) : Prop

HKL eq 16, the INCREASE function: INCREASE(φ)(x)(d)(e) = 1 iff φ(x)(SPO(e)) + d = φ(x)(EPO(e)).

True iff x's degree at the end of an event equals its degree at the start plus d. The "difference value" d is HKL's central object; its boundedness drives telicity (HKL §3 thesis).

K&L 2008 reformulates this as a measure-valued function measureOfChange m x initT finT : δ with explicit differenceFunction clamping at the initial degree (K&L eq 23). The two coincide on monotone-increase events with d ≥ 0; HKL's Prop-valued INCREASE is sufficient for the §3 data and avoids the clamping bookkeeping.

Equations

• HayKennedyLevin1999.INCREASE φ x d startT finT = (φ x startT + d = φ x finT)

theorem HayKennedyLevin1999.increase_self {α : Type u_1} {δ : Type u_2} {Time : Type u_3} [AddZeroClass δ] (φ : TimedAdjective α δ Time) (x : α) (t : Time) : INCREASE φ x 0 t t

Zero-duration events (start = end) carry zero difference value.

theorem HayKennedyLevin1999.increase_unique_end {α : Type u_1} {δ : Type u_2} {Time : Type u_3} [Add δ] (φ : TimedAdjective α δ Time) (x : α) (d : δ) (startT finT₁ finT₂ : Time) (h₁ : INCREASE φ x d startT finT₁) (h₂ : INCREASE φ x d startT finT₂) : φ x finT₁ = φ x finT₂

HKL §3 thesis at the type level: when the difference value d is given, the end degree is uniquely determined by the start degree — the structural source of telic interpretations.

HKL §3.2 (p. 135): closed-range adjectives (full, empty, straight, dry) map to bounded scales; open-range adjectives (long, wide, short) map to unbounded scales. The DA verbs derived from each class default to telic vs atelic respectively (HKL eqs 26-27).

Linglib's fragment encodes this directly via `degreeAchievementScale`
annotations on each DA verb:

| Verb        | Base adjective | scaleBoundedness | vendlerClass     |
|-------------|----------------|------------------|------------------|
| straighten  | straight       | `.closed`        | `.accomplishment`|
| lengthen    | long           | `.open_`         | `.activity`      |
| widen       | wide           | `.open_`         | `.activity`      |
| cool        | cool           | `.open_`         | `.activity`      |
| warm        | warm           | `.open_`         | `.activity`      |

The theorems below verify HKL's matrix prediction on each fragment
entry. K&L 2008's `KennedyLevin2008.lean` study file proves the
per-verb derivation of `vendlerClass` from `scaleBoundedness`
structurally; this file checks HKL's specific predictions on the
central exemplars. 

theorem HayKennedyLevin1999.straighten_closed_accomplishment : Option.map (fun (x : Features.DegreeAchievement.DegreeAchievementScale) => x.scaleBoundedness) Fragments.English.Predicates.Verbal.straighten.degreeAchievementScale = some Core.Scale.Boundedness.closed ∧ Fragments.English.Predicates.Verbal.straighten.vendlerClass = some Features.VendlerClass.accomplishment

HKL eq 26 (closed-range default): "straighten" — closed scale, accomplishment (telic).

theorem HayKennedyLevin1999.lengthen_open_activity : Option.map (fun (x : Features.DegreeAchievement.DegreeAchievementScale) => x.scaleBoundedness) Fragments.English.Predicates.Verbal.lengthen.degreeAchievementScale = some Core.Scale.Boundedness.open_ ∧ Fragments.English.Predicates.Verbal.lengthen.vendlerClass = some Features.VendlerClass.activity

HKL eq 27 (open-range default): "lengthen" — open scale, activity (atelic).

theorem HayKennedyLevin1999.widen_open_activity : Option.map (fun (x : Features.DegreeAchievement.DegreeAchievementScale) => x.scaleBoundedness) Fragments.English.Predicates.Verbal.widen.degreeAchievementScale = some Core.Scale.Boundedness.open_ ∧ Fragments.English.Predicates.Verbal.widen.vendlerClass = some Features.VendlerClass.activity

HKL §3.1 default: "widen" — open scale, activity (made telic only by overt measure phrase, see §3 below).

theorem HayKennedyLevin1999.cool_open_activity : Option.map (fun (x : Features.DegreeAchievement.DegreeAchievementScale) => x.scaleBoundedness) Fragments.English.Predicates.Verbal.cool.degreeAchievementScale = some Core.Scale.Boundedness.open_ ∧ Fragments.English.Predicates.Verbal.cool.vendlerClass = some Features.VendlerClass.activity

HKL §3.1 default: "cool" — open scale, activity (made telic only by overt measure phrase or contextual bound).

theorem HayKennedyLevin1999.warm_open_activity : Option.map (fun (x : Features.DegreeAchievement.DegreeAchievementScale) => x.scaleBoundedness) Fragments.English.Predicates.Verbal.warm.degreeAchievementScale = some Core.Scale.Boundedness.open_ ∧ Fragments.English.Predicates.Verbal.warm.vendlerClass = some Features.VendlerClass.activity

HKL §3.1 default: "warm" — open scale, activity.

HKL §3.1: when the difference value is bounded by overt linguistic material, the predicate is telic regardless of the base adjective's scalar structure. Three modifier classes:

1. **Measure phrases** (HKL eqs 18-20): *widened the road 5 m*,
   *cooled 4 degrees* — telic.
2. **Completely** (HKL eqs 21-22): *straightened completely*,
   *dried completely* — telic. Forces `d` to a maximum.
3. **Significantly** (HKL eq 23) — telic (lower bound from
   monotone-increasing modifier); contrasts with **slightly**
   (HKL eq 24) — atelic (no lower bound). 

structure HayKennedyLevin1999.HKLModifierDatum : Type

An HKL §3.1 modifier-class datum: a sentence + its modifier-class + HKL's predicted telicity + the paper-equation tag.

• sentence : String
• modifier : String
• expectedTelic : Bool
• paperEq : String

def HayKennedyLevin1999.instReprHKLModifierDatum.repr : HKLModifierDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HayKennedyLevin1999.instReprHKLModifierDatum : Repr HKLModifierDatum

Equations

• HayKennedyLevin1999.instReprHKLModifierDatum = { reprPrec := HayKennedyLevin1999.instReprHKLModifierDatum.repr }

def HayKennedyLevin1999.widenedRoad5m : HKLModifierDatum

Equations

• HayKennedyLevin1999.widenedRoad5m = { sentence := "They widened the road 5 m.", modifier := "5 m", expectedTelic := true, paperEq := "HKL eq 18a (telic per eq 19a)" }

def HayKennedyLevin1999.lakeCooled4Deg : HKLModifierDatum

Equations

• HayKennedyLevin1999.lakeCooled4Deg = { sentence := "The lake cooled 4 degrees.", modifier := "4 degrees", expectedTelic := true, paperEq := "HKL eq 18b (telic per eq 19b)" }

def HayKennedyLevin1999.straightenedCompletely : HKLModifierDatum

Equations

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

def HayKennedyLevin1999.driedCompletely : HKLModifierDatum

Equations

• HayKennedyLevin1999.driedCompletely = { sentence := "The clothes dried completely.", modifier := "completely", expectedTelic := true, paperEq := "HKL eq 21b (telic per eq 22b)" }

def HayKennedyLevin1999.broadenedSignificantly : HKLModifierDatum

Equations

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

def HayKennedyLevin1999.broadenedSlightly : HKLModifierDatum

Equations

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

def HayKennedyLevin1999.hklSection3_1Data : List HKLModifierDatum

Equations

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

def HayKennedyLevin1999.modifierLicensesTelic : String → Bool

Modifier-class licensing prediction (HKL §3.1): measure phrases, completely, and significantly each induce telicity by bounding the difference value below; slightly does not. Cf. K&M 2005's later modifier-class matrix at scale-structure level.

Equations

• HayKennedyLevin1999.modifierLicensesTelic "completely" = true
• HayKennedyLevin1999.modifierLicensesTelic "significantly" = true
• HayKennedyLevin1999.modifierLicensesTelic "slightly" = false
• HayKennedyLevin1999.modifierLicensesTelic x✝ = true

theorem HayKennedyLevin1999.hklSection3_1Data_consistent : (hklSection3_1Data.all fun (d : HKLModifierDatum) => modifierLicensesTelic d.modifier == d.expectedTelic) = true

HKL §3.1 matrix: all six §3.1 data points agree with the modifier-class prediction.

HKL §3.3: when no overt linguistic material specifies the difference value, real-world knowledge can supply a bound, producing a defeasible telic interpretation that is cancellable because it arises through conversational implicature.

The contrast (HKL eqs 28 vs 30): pants/blinds have a conventional
maximum → telic (eq 28); commute/heat have no conventional bound →
atelic (eq 30). Eq 32 confirms the eq-28 telicity is cancellable
(*lengthened my pants, but not completely* is felicitous). Eq 33
confirms linguistically-supplied bounds (eq 21's *completely*) are
NOT cancellable (*#straightened completely, but not completely*). 

structure HayKennedyLevin1999.HKLContextDatum : Type

An HKL §3.3 context-dependent telicity datum.

• sentence : String
• contextProvidesBound : Bool
• expectedTelic : Bool
• cancellable : Bool
• paperEq : String

def HayKennedyLevin1999.instReprHKLContextDatum.repr : HKLContextDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HayKennedyLevin1999.instReprHKLContextDatum : Repr HKLContextDatum

Equations

• HayKennedyLevin1999.instReprHKLContextDatum = { reprPrec := HayKennedyLevin1999.instReprHKLContextDatum.repr }

def HayKennedyLevin1999.tailorLengthened : HKLContextDatum

Equations

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

def HayKennedyLevin1999.kimLowered : HKLContextDatum

Equations

• HayKennedyLevin1999.kimLowered = { sentence := "Kim lowered the blind.", contextProvidesBound := true, expectedTelic := true, cancellable := true, paperEq := "HKL eq 28b (telic per 29b)" }

def HayKennedyLevin1999.trafficLengthened : HKLContextDatum

Equations

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

def HayKennedyLevin1999.kimLoweredHeat : HKLContextDatum

Equations

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

def HayKennedyLevin1999.hklSection3_3Data : List HKLContextDatum

Equations

• HayKennedyLevin1999.hklSection3_3Data = [HayKennedyLevin1999.tailorLengthened, HayKennedyLevin1999.kimLowered, HayKennedyLevin1999.trafficLengthened, HayKennedyLevin1999.kimLoweredHeat]

theorem HayKennedyLevin1999.hklSection3_3Data_matrix : (hklSection3_3Data.all fun (d : HKLContextDatum) => d.contextProvidesBound == d.expectedTelic && d.contextProvidesBound == d.cancellable) = true

HKL §3.3 matrix prediction: contextual bound ⟺ (defeasible) telicity; when telic via context, the inference is cancellable; when no context-bound, the interpretation is robustly atelic.

HKL §4.1 extends the analysis to consumption (eat the sandwich, eqs 36-37), motion (run a mile, descend 1000m, eqs 38-42), and creation (draw a house, eq 39) — the "classically telic" verbs of @cite{krifka-1989}'s incremental-theme tradition. Their telicity ALSO depends on the boundedness of a difference value: bounded → telic, unbounded → atelic. The difference value is "the measure of change along a path of motion, in spatial extent, or in some other scalar property" (HKL §4.2).

HKL uses this generalization to argue against Dowty 1991's
"incremental theme as argument" view: the incremental theme is
properly construed as a *property of an argument*, not the
argument itself (HKL §4.2). That argument is recorded as data here
but not further formalized — the K89 quantization framework
(`Theories/Semantics/Events/Krifka1989.lean`) is the substrate for
the consumption/creation cases, and `Phenomena/TenseAspect/Studies/Krifka1989.lean`
§1-§4 cover the same ground via Krifka's QUA/CUM apparatus. 

structure HayKennedyLevin1999.HKLBeyondDADatum : Type

A datum from HKL §4.1's beyond-DA generalization.

• sentence : String
• verbClass : String
• bounded : Bool
• expectedTelic : Bool
• paperEq : String

def HayKennedyLevin1999.instReprHKLBeyondDADatum.repr : HKLBeyondDADatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HayKennedyLevin1999.instReprHKLBeyondDADatum : Repr HKLBeyondDADatum

Equations

• HayKennedyLevin1999.instReprHKLBeyondDADatum = { reprPrec := HayKennedyLevin1999.instReprHKLBeyondDADatum.repr }

def HayKennedyLevin1999.ateSandwich5min : HKLBeyondDADatum

Equations

• HayKennedyLevin1999.ateSandwich5min = { sentence := "She ate the sandwich in 5 minutes.", verbClass := "consumption", bounded := true, expectedTelic := true, paperEq := "HKL eq 36 / 37a" }

def HayKennedyLevin1999.ranMile : HKLBeyondDADatum

Equations

• HayKennedyLevin1999.ranMile = { sentence := "She ran a mile.", verbClass := "motion", bounded := true, expectedTelic := true, paperEq := "HKL eq 38a (negation infelicitous)" }

def HayKennedyLevin1999.ranRace : HKLBeyondDADatum

Equations

• HayKennedyLevin1999.ranRace = { sentence := "She ran a race.", verbClass := "motion", bounded := true, expectedTelic := true, paperEq := "HKL eq 38b" }

def HayKennedyLevin1999.planeDescended20min : HKLBeyondDADatum

Equations

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

def HayKennedyLevin1999.hklSection4Data : List HKLBeyondDADatum

Equations

• HayKennedyLevin1999.hklSection4Data = [HayKennedyLevin1999.ateSandwich5min, HayKennedyLevin1999.ranMile, HayKennedyLevin1999.ranRace, HayKennedyLevin1999.planeDescended20min]

theorem HayKennedyLevin1999.hklSection4Data_bounded_iff_telic : (hklSection4Data.all fun (d : HKLBeyondDADatum) => d.bounded == d.expectedTelic) = true

HKL §4.1 generalization: across consumption, motion, and directed motion, bounded difference value ⟺ telic interpretation.