From 4db025593814654c3f805c5f35745255d2af10b5 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 3 Jun 2026 18:57:35 -0700 Subject: [PATCH] feat(Semantics/Aspect): scalar telicity from order mixins --- Linglib.lean | 1 + Linglib/Core/Scales/Bounds.lean | 27 ++ .../Semantics/Aspect/DegreeAchievement.lean | 8 +- Linglib/Semantics/Aspect/ScalarTelicity.lean | 144 ++++++++ Linglib/Studies/KennedyLevin2008.lean | 331 ++++++------------ blog/references.bib | 15 + 6 files changed, 301 insertions(+), 225 deletions(-) create mode 100644 Linglib/Semantics/Aspect/ScalarTelicity.lean diff --git a/Linglib.lean b/Linglib.lean index e01bc6e50..c41f178b5 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -2424,6 +2424,7 @@ import Linglib.Semantics.Aspect.Basic import Linglib.Semantics.Aspect.Composition import Linglib.Semantics.Aspect.SubintervalProperty import Linglib.Semantics.Aspect.DegreeAchievement +import Linglib.Semantics.Aspect.ScalarTelicity import Linglib.Semantics.Aspect.ChangeOfState -- Theories: Semantics.Iconic (Iconological Semantics for sign language) import Linglib.Semantics.Iconic.Basic diff --git a/Linglib/Core/Scales/Bounds.lean b/Linglib/Core/Scales/Bounds.lean index 3130ff348..d0839c377 100644 --- a/Linglib/Core/Scales/Bounds.lean +++ b/Linglib/Core/Scales/Bounds.lean @@ -89,6 +89,33 @@ theorem open_scale_unlicensable [NoMaxOrder α] [NoMinOrder α] · obtain ⟨y, hy⟩ := NoMaxOrder.exists_gt x exact ⟨y, hy, le_trans hx (le_of_lt hy)⟩ +/-! ### Order-theoretic boundedness primitives + +Whether a scale has a greatest degree, stated *structurally* via mathlib's +`OrderTop` / `NoMaxOrder` mixins rather than as stored data — the order-theoretic +facts that telicity and licensing derive from (see `Semantics/Aspect/ScalarTelicity.lean`). -/ + +/-- "Has a greatest element", as a proposition — usable when an `OrderTop` + instance is not in hand (e.g. under a quantifier). -/ +def HasGreatest (β : Type*) [LE β] : Prop := ∃ m : β, ∀ x : β, x ≤ m + +theorem hasGreatest_of_orderTop {β : Type*} [LE β] [OrderTop β] : HasGreatest β := + ⟨⊤, fun _ => le_top⟩ + +theorem not_hasGreatest_of_noMaxOrder {β : Type*} [Preorder β] [NoMaxOrder β] : + ¬ HasGreatest β := by + rintro ⟨m, hm⟩ + obtain ⟨c, hc⟩ := exists_gt m + exact absurd (hm c) (not_le_of_gt hc) + +/-- `OrderTop` and `NoMaxOrder` are mutually exclusive — the rigorous sense in + which a scale either has a greatest degree or does not. (Not in Mathlib.) -/ +theorem not_noMaxOrder_of_orderTop {β : Type*} [Preorder β] [OrderTop β] : + ¬ NoMaxOrder β := by + intro h + obtain ⟨c, hc⟩ := h.exists_gt ⊤ + exact absurd (lt_of_lt_of_le hc le_top) (lt_irrefl ⊤) + -- ════════════════════════════════════════════════════ -- § 6b. Order-Sensitive MAX ([rett-2026]) -- ════════════════════════════════════════════════════ diff --git a/Linglib/Semantics/Aspect/DegreeAchievement.lean b/Linglib/Semantics/Aspect/DegreeAchievement.lean index 883c9991a..3b85f2052 100644 --- a/Linglib/Semantics/Aspect/DegreeAchievement.lean +++ b/Linglib/Semantics/Aspect/DegreeAchievement.lean @@ -19,10 +19,6 @@ open, mΔ is unbounded → atelic (activity). This module derives `VendlerClass` from `Boundedness`, connecting to the existing `LicensingPipeline` infrastructure in `Core/Scales/Scale.lean`. - -- 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. -/ namespace Features.DegreeAchievement @@ -49,8 +45,8 @@ structure DegreeAchievementScale where instance : Inhabited DegreeAchievementScale where default := { scaleBoundedness := .open_, dimension := "" } -/-- Derive default telicity from scale boundedness ([kennedy-levin-2008] Thm 1). - Scales with a maximum → telic; scales without → atelic. +/-- Derive default telicity from scale boundedness — the central claim of + [kennedy-levin-2008]. Scales with a maximum → telic; scales without → atelic. The mapping follows `Boundedness.hasMax`: - `.closed` (has max) → `.telic` diff --git a/Linglib/Semantics/Aspect/ScalarTelicity.lean b/Linglib/Semantics/Aspect/ScalarTelicity.lean new file mode 100644 index 000000000..cb9fe8d7e --- /dev/null +++ b/Linglib/Semantics/Aspect/ScalarTelicity.lean @@ -0,0 +1,144 @@ +import Linglib.Semantics.Degree.MeasureFunction +import Linglib.Semantics.ArgumentStructure.Affectedness.Hierarchy +import Mathlib.Order.BoundedOrder.Basic +import Mathlib.Order.Max +import Mathlib.Order.WithBot + +/-! +# Scalar telicity: telicity from the order structure of a scale + +[kennedy-levin-2008]'s thesis — a degree achievement's telicity is fixed by the +boundedness of its adjectival scale — realised *order-theoretically* and connected +to [beavers-2011]'s affectedness hierarchy. "The scale has a greatest degree" is +mathlib's `OrderTop` mixin; "the scale is unbounded above" is `NoMaxOrder`; over a +degree type `δ`. A degree achievement is telic (admits a Quantized witness) **iff** +its scale has a greatest element — the witness is the maximum `g_φ = ⊤`, *derived* +from the mixin, not stipulated from a stored flag. + +The measure is the patient's degree at the event's end (its temporal trace); +[beavers-2011]'s `HasScalarResult` is synthesised by `ofHasMeasureFunction`. + +## Main results + +* `telic_of_orderTop` — `[OrderTop δ]` ⇒ a Quantized witness exists (at `⊤`). +* `atelic_of_noMaxOrder` — `[NoMaxOrder δ]` ⇒ no Quantized witness exists. +* `Dimension` / `Dimension.degree` — a scalar dimension is the categorical + primitive (what the adjective measures); its boundedness is the order-mixin + profile of its degree type, not a stored flag. + +## Implementation notes + +Degree carriers are computable order-shapes (`WithTop ℕ` for closed, `ℕ` for +unbounded-above), so `decide` stays available; what matters is the +presence/absence of the `OrderTop` / `NoMaxOrder` mixin, not the carrier. +-/ + +namespace ScalarTelicity + +open Semantics.ArgumentStructure.Affectedness +open Semantics.ArgumentStructure.Affectedness.Hierarchy +open Semantics.Degree.MeasureFunction + +/-- Trivial patient: the measure of change ignores the patient's identity, so a + single one-constructor type serves for every degree type `δ`. -/ +inductive Patient + | mk + +section +variable {δ : Type*} [LinearOrder δ] + +/-- The patient's degree at a time is that time — the temporal trace — so the + final degree of an event is its end-time. The instance lives on the file-local + `Patient`, so it cannot pollute resolution elsewhere. -/ +instance traceMeasure : HasMeasureFunction Patient δ δ where + measure _ t := t + +/-- Companion `HasLatentScale` ([beavers-2011] eq. (60c)). -/ +instance : HasLatentScale Patient (Event δ) := + HasLatentScale.ofHasMeasureFunction (δ := δ) + +/-- Telic reading: the patient reaches the maximal degree `⊤` by the event's end. + Available only when the scale has a greatest element (`OrderTop`). -/ +def reachesTop [OrderTop δ] : Patient → Event δ → Prop := + fun _ e => e.runtime.finish = (⊤ : δ) + +/-- Atelic ('comparative') reading: the patient reaches *some* degree by the end — + always satisfiable, hence `NonQuantized` for any scale. -/ +def reachesSome : Patient → Event δ → Prop := + fun _ e => ∃ g : δ, e.runtime.finish = g + +theorem reachesSome_nonQuantized : NonQuantized (δ := δ) (reachesSome (δ := δ)) := + fun _ _ h => h + +/-- With a greatest degree, the telic reading is Quantized at `⊤`: every event + entails the patient reaches the maximum. -/ +theorem reachesTop_quantized [OrderTop δ] : + Quantized (reachesTop (δ := δ)) (⊤ : δ) := + fun _ _ h => h + +/-- **Telic ⇐ a greatest degree.** `OrderTop` supplies the Quantized witness + `g_φ = ⊤` — the order-theoretic content of [kennedy-levin-2008]'s closed-scale + telicity. -/ +theorem telic_of_orderTop [OrderTop δ] : + ∃ g : δ, Quantized (reachesTop (δ := δ)) g := + ⟨⊤, reachesTop_quantized⟩ + +/-- **Telic ⇒ a greatest degree (contrapositive).** With no greatest degree + (`NoMaxOrder`), *no* final degree is entailed: for any candidate `g`, + `exists_gt` yields a strictly larger degree, realised by an event whose final + degree is not `g`. This is [kennedy-levin-2008]'s open-scale obligatory + atelicity, derived from the order structure. -/ +theorem atelic_of_noMaxOrder [NoMaxOrder δ] : + ¬ ∃ g : δ, Quantized (reachesSome (δ := δ)) g := by + rintro ⟨g, hg⟩ + obtain ⟨b, hb⟩ := exists_gt g + have hbg : b = g := hg Patient.mk ⟨⟨b, b, le_refl b⟩, .dynamic⟩ ⟨_, rfl⟩ + exact absurd hbg hb.ne' + +/-- Synthesis: with a greatest degree, the telic reading builds the full Beavers + `IsQuantizedAffected` instance — the `HasScalarResult` premise is found from + `traceMeasure`, and the weaker hierarchy levels follow by the `extends` chain + ([beavers-2011] eq. (62)). -/ +instance reachesTop_isQuantizedAffected [OrderTop δ] : + IsQuantizedAffected (δ := δ) (reachesTop (δ := δ)) := + IsQuantizedAffected.mk' (fun _ _ _ => trivial) ⊤ reachesTop_quantized + +example [OrderTop δ] : IsNonQuantizedAffected (δ := δ) (reachesTop (δ := δ)) := inferInstance +example [OrderTop δ] : IsPotentialAffected (β := Event δ) (reachesTop (δ := δ)) := inferInstance + +end + +/-! ### Dimensions: boundedness as the order structure of the degree type + +A *dimension* (what the adjective measures) is the categorical primitive; its +boundedness is the order-mixin profile of its degree type, read off structurally +rather than stored. -/ + +/-- Scalar dimensions a degree-achievement verb's base adjective can measure. -/ +inductive Dimension + | straightness | fullness | cleanliness + | width | length | height + | temperature + deriving DecidableEq, Repr + +/-- The degree type for each dimension. Boundedness is structural: closed + dimensions carry `OrderTop` (`WithTop ℕ`), unbounded-above ones `NoMaxOrder` + (`ℕ`). The carrier is a computable order-shape, not a real magnitude — only the + mixin matters. -/ +abbrev Dimension.degree : Dimension → Type + | .straightness | .fullness | .cleanliness => WithTop ℕ + | .width | .length | .height | .temperature => ℕ + +/-- A closed dimension yields a telic reading (a Quantized witness at `⊤`). -/ +theorem straightness_telic : + ∃ g : Dimension.straightness.degree, + Quantized (reachesTop (δ := Dimension.straightness.degree)) g := + telic_of_orderTop + +/-- An unbounded-above dimension yields an atelic reading (no Quantized witness). -/ +theorem width_atelic : + ¬ ∃ g : Dimension.width.degree, + Quantized (reachesSome (δ := Dimension.width.degree)) g := + atelic_of_noMaxOrder + +end ScalarTelicity diff --git a/Linglib/Studies/KennedyLevin2008.lean b/Linglib/Studies/KennedyLevin2008.lean index ed453e2de..e3fd92878 100644 --- a/Linglib/Studies/KennedyLevin2008.lean +++ b/Linglib/Studies/KennedyLevin2008.lean @@ -1,41 +1,51 @@ import Linglib.Semantics.Aspect.DegreeAchievement -import Linglib.Semantics.Degree.MeasureFunction +import Linglib.Semantics.Aspect.ScalarTelicity import Linglib.Semantics.ArgumentStructure.Affectedness.Hierarchy import Linglib.Fragments.English.Predicates.Verbal import Linglib.Fragments.English.Predicates.Adjectival import Linglib.Phenomena.TenseAspect.Diagnostics -import Mathlib.Data.Rat.Defs /-! -# Degree Achievements -[kennedy-levin-2008] - -[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. +# Degree achievements: the adjectival core of telicity + +Formalisation of [kennedy-levin-2008], 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 its `degreeAchievementScale`. +* `*_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 lives in `Semantics/Aspect/ScalarTelicity.lean` + (`telic_of_orderTop` / `atelic_of_noMaxOrder`): a degree achievement admits a + Quantized (telic) witness iff its scale has a greatest degree, via mathlib's + `OrderTop` / `NoMaxOrder` mixins (witness `g_φ = ⊤`), feeding [beavers-2011]'s + affectedness hierarchy. Here it is instantiated at the dimensions the verbs + measure — `straighten_telic` (straightness, closed), `widen_atelic` (width, + open) — matched to the fragment tags by `straighten_scale_hasMax` / + `widen_scale_no_max`. The variable-telicity contrast of [kennedy-levin-2008] §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/Hierarchy.lean`. -/ namespace KennedyLevin2008 open English.Predicates.Verbal hiding clean cool warm open_ open Features.DegreeAchievement (DegreeAchievementScale) -open Semantics.Lexical -open Core.Scale (Boundedness LicensingPipeline MereoTag) +open Core.Scale (LicensingPipeline) open Phenomena.TenseAspect.Diagnostics (forXPrediction inXPrediction) -- Fully qualified aliases for names shared between Verbal and Adjectival @@ -48,12 +58,11 @@ private def aCool := English.Predicates.Adjectival.cool private def aWarm := English.Predicates.Adjectival.warm private def aOpen := English.Predicates.Adjectival.open_ --- ════════════════════════════════════════════════════ --- § 1. Per-Verb Derived VendlerClass Verification --- ════════════════════════════════════════════════════ +/-! ### Per-verb derived Vendler class -/-! For each degree achievement verb, the vendlerClass stipulated in the - fragment matches what degreeAchievementScale.defaultVendlerClass derives. -/ +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). -/ theorem bend_derived_vendler : @@ -115,13 +124,26 @@ theorem warm_derived_vendler : vWarm.toVerb.degreeAchievementScale.get!.defaultVendlerClass = vWarm.toVerb.vendlerClass.get! := rfl --- ════════════════════════════════════════════════════ --- § 2. Adjective-Verb Scale Agreement --- ════════════════════════════════════════════════════ +/-- The degree-achievement verbs whose telicity this file derives from scale + boundedness. -/ +def daVerbs : List Verb := + [bend.toVerb, boil.toVerb, rust.toVerb, increase.toVerb, vClean.toVerb, + straighten.toVerb, flatten.toVerb, vOpen.toVerb, lengthen.toVerb, + widen.toVerb, vCool.toVerb, vWarm.toVerb] -/-! 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. -/ +/-- 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. -/ +theorem da_vendler_classes_agree : + ∀ v ∈ daVerbs, v.vendlerClass = v.degreeAchievementScale.map (·.defaultVendlerClass) := by + decide + +/-! ### 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). -/ theorem clean_adj_verb_scale : @@ -163,22 +185,22 @@ theorem warm_adj_verb_scale : aWarm.scaleType = (vWarm.toVerb.degreeAchievementScale.get!).scaleBoundedness := rfl -/-- 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. [kennedy-levin-2008] notes that the verb - selects the relevant portion of the 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 + [kennedy-levin-2008]'s treatment of *cool*, whose conventionalised + 'room-temperature' standard licenses a telic reading from an open-scale base + (§3.3); [kennedy-levin-2008] do not themselves discuss *boil*. -/ theorem hot_boil_scale_diverges : English.Predicates.Adjectival.hot.scaleType = .open_ ∧ (boil.toVerb.degreeAchievementScale.get!).scaleBoundedness = .closed := ⟨rfl, rfl⟩ --- ════════════════════════════════════════════════════ --- § 3. Telicity Diagnostic Predictions --- ════════════════════════════════════════════════════ +/-! ### Telicity-diagnostic predictions -/-! Closed-scale DAs accept "in X" (telic prediction). - Open-scale DAs accept "for X" (atelic prediction). -/ +Closed-scale degree achievements accept *in X* (telic); open-scale ones accept +*for X* (atelic). -/ --- Closed-scale: "in X" ✓ +/-! #### Closed-scale verbs accept *in X* -/ /-- "bent the wire in 5 seconds" — closed-scale DA accepts "in X". -/ theorem bend_inX : @@ -204,7 +226,7 @@ theorem flatten_inX : theorem open_inX : inXPrediction vOpen.toVerb.vendlerClass.get! = .accept := rfl --- Open-scale: "for X" ✓ +/-! #### Open-scale verbs accept *for X* -/ /-- "rusted for years" — open-scale DA accepts "for X". -/ theorem rust_forX : @@ -230,13 +252,11 @@ theorem cool_forX : theorem warm_forX : forXPrediction vWarm.toVerb.vendlerClass.get! = .accept := rfl --- ════════════════════════════════════════════════════ --- § 4. Pipeline Convergence --- ════════════════════════════════════════════════════ +/-! ### Pipeline convergence -/-! LicensingPipeline.toBoundedness applied to the verb's - degreeAchievementScale matches LicensingPipeline.toBoundedness - applied to the verb's vendlerClass. -/ +`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. -/ theorem bend_pipeline_converge : @@ -298,175 +318,48 @@ theorem warm_pipeline_converge : LicensingPipeline.toBoundedness vWarm.toVerb.degreeAchievementScale.get! = LicensingPipeline.toBoundedness vWarm.toVerb.vendlerClass.get! := rfl --- ════════════════════════════════════════════════════ --- § 5. Substrate-Level Demonstration: K&L → Beavers --- ════════════════════════════════════════════════════ - -/-! K&L 2008's measure-of-change function `m_Δ` (eq. 25), formalised in - `Semantics/Degree/MeasureFunction.lean`, plugs directly - into Beavers' affectedness typeclass chain - (`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. -/ +/-! ### Substrate demonstration: telicity from scale order + +The order-theoretic account of [kennedy-levin-2008]'s thesis lives in +`Semantics/Aspect/ScalarTelicity.lean`: a degree achievement is telic iff its +scale has a greatest degree (`OrderTop`), with the Quantized witness `g_φ = ⊤`, +feeding [beavers-2011]'s affectedness hierarchy. Here it is instantiated at the +dimensions the K&L verbs measure. -/ open Semantics.ArgumentStructure.Affectedness open Semantics.ArgumentStructure.Affectedness.Hierarchy -open Semantics.Degree.MeasureFunction - -/-- Toy time type for the substrate demonstration. -/ -abbrev SubstrateTime : Type := Nat - --- ──────────────────────────────────────────────────── --- §5.1 Closed-scale: *straighten* (K&L eq. 20) --- ──────────────────────────────────────────────────── - -/-- 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. -/ -abbrev RodToy : Type := Unit - -/-- 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. -/ -instance straightMeasure : HasMeasureFunction RodToy ℚ SubstrateTime where - measure _ _ := 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`). -/ -instance : HasLatentScale RodToy (Event SubstrateTime) := - HasLatentScale.ofHasMeasureFunction (δ := ℚ) - -/-- *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. -/ -def θ_straighten_toy : RodToy → Event SubstrateTime → Prop := - fun x e => HasMeasureFunction.measure - (α := RodToy) (δ := ℚ) (Time := SubstrateTime) - x e.runtime.finish = (1 : ℚ) - -/-- *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. -/ -theorem straighten_quantized_toy : - Quantized θ_straighten_toy (1 : ℚ) := - fun _ _ h => h - -/-- 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. -/ -instance straighten_isQuantizedAffected_toy : - IsQuantizedAffected (δ := ℚ) θ_straighten_toy := - IsQuantizedAffected.mk' (fun _ _ _ => trivial) (1 : ℚ) straighten_quantized_toy - -/-- `IsQuantizedAffected.finalDegree` is accessible as data - (preserves K&L's lexical `g_φ` commitment). -/ -example : IsQuantizedAffected.finalDegree (θ := θ_straighten_toy) = (1 : ℚ) := rfl - -/-- Synthesis test: extends-chain gives `IsNonQuantizedAffected` from - the Quantized instance (Beavers eq. 62 leftmost arrow). -/ -example : IsNonQuantizedAffected (δ := ℚ) θ_straighten_toy := inferInstance - -/-- Synthesis test: extends-chain gives `IsPotentialAffected` (bottom). -/ -example : IsPotentialAffected (β := Event SubstrateTime) θ_straighten_toy := - inferInstance - --- ──────────────────────────────────────────────────── --- §5.2 Open-scale: *widen* (K&L §7.3.3) --- ──────────────────────────────────────────────────── - -/-- Toy patient type for substrate-level *widen*. -/ -abbrev GapToy : Type := Unit - -/-- 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`. -/ -instance wideMeasure : HasMeasureFunction GapToy ℚ SubstrateTime where - measure _ t := (t : ℚ) + 1 - -/-- HasLatentScale companion for *widen*. -/ -instance : HasLatentScale GapToy (Event SubstrateTime) := - HasLatentScale.ofHasMeasureFunction (δ := ℚ) - -/-- *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. -/ -def θ_widen_toy : GapToy → Event SubstrateTime → Prop := - fun x e => ∃ g : ℚ, HasMeasureFunction.measure - (α := GapToy) (δ := ℚ) (Time := SubstrateTime) - x e.runtime.finish = g - -/-- *widen* is NonQuantized: every widening event ends with the - patient at SOME degree on the wide scale. K&L's atelic - "comparative" reading. -/ -theorem widen_nonQuantized_toy : - NonQuantized (δ := ℚ) θ_widen_toy := - fun _ _ h => h - -/-- 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. -/ -instance widen_isNonQuantizedAffected_toy : - IsNonQuantizedAffected (δ := ℚ) θ_widen_toy := - IsNonQuantizedAffected.mk' (fun _ _ _ => trivial) widen_nonQuantized_toy - -/-- Extends-chain still gives Potential. -/ -example : IsPotentialAffected (β := Event SubstrateTime) θ_widen_toy := inferInstance - --- ──────────────────────────────────────────────────── --- §5.3 Telicity Bridge to AffectednessDegree --- ──────────────────────────────────────────────────── - -/-- 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. -/ +open ScalarTelicity + +/-- *straighten* measures straightness — a closed scale — so a telic reading is + available, derived from the dimension's `OrderTop` (not a stored `hasMax`). -/ +theorem straighten_telic : + ∃ g : Dimension.straightness.degree, + Quantized (reachesTop (δ := Dimension.straightness.degree)) g := + straightness_telic + +/-- *widen* measures width — unbounded above — so no telic reading exists. -/ +theorem widen_atelic : + ¬ ∃ g : Dimension.width.degree, + Quantized (reachesSome (δ := Dimension.width.degree)) g := + width_atelic + +/-- The dimension assignments match the fragment's current scale tags: + *straighten* closed (`hasMax`), *widen* open (no max). (Phase 3 of the + boundedness→mixin migration replaces the tag with the dimension itself.) -/ +theorem straighten_scale_hasMax : + straighten.toVerb.degreeAchievementScale.get!.scaleBoundedness.hasMax = true := by + decide + +theorem widen_scale_no_max : + widen.toVerb.degreeAchievementScale.get!.scaleBoundedness.hasMax = false := by + decide + +/-! #### Telicity at the `AffectednessDegree` level -/ + +/-- The [kennedy-levin-2008] to [beavers-2011] 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. -/ theorem widen_lt_straighten_at_affectedness_level : AffectednessDegree.nonquantized < AffectednessDegree.quantized := by decide diff --git a/blog/references.bib b/blog/references.bib index 693259dfa..b82a73cf6 100644 --- a/blog/references.bib +++ b/blog/references.bib @@ -9858,6 +9858,21 @@ @article{beavers-2010 validated = {true}, sources = {Phenomena/ArgumentStructure/Studies/Beavers2010.lean} } + +@article{beavers-2011, + author = {Beavers, John}, + year = {2011}, + title = {On Affectedness}, + journal = {Natural Language \& Linguistic Theory}, + volume = {29}, + number = {2}, + pages = {335--370}, + publisher = {Springer}, + subfield = {semantics/argument-structure}, + role = {formalized}, + validated = {true}, + sources = {Semantics/ArgumentStructure/Affectedness/Hierarchy.lean} +} @book{sneddon-1996, author = {Sneddon, James Neil}, year = {1996},