Degree semantics: core types and classification carriers

Foundational definitions for degree-based analyses of gradable expressions [Hei01] [Ken07] [Sch08f] [Bel25]:

• the discrete scale types Degree max / Threshold max (the finite carriers used by the RSA fragment), and
• the Kennedy-style classification enums (PositiveStandard, AdjectiveClass, …).

Positive-form semantics is in Basic.lean; Kennedy 2007's interpretive economy is in Kennedy.lean. The abstract theory works with plain measure functions μ : E → α into a linear order — there is no measure typeclass. Klein-style delineation [Kle80] has no measure function and lives in Gradability/Delineation.lean.

Main definitions

• Degree max, Threshold max — discrete bounded scale types (Fin-backed).
• DegPType — DegP compositional taxonomy.
• PositiveStandard, AdjectiveClass — Kennedy-style classification carriers.

Adjectival surface-construction types (AdjectivalConstruction) live in Gradability/Construction.lean.

Discrete bounded scales

Degree max wraps Fin (max + 1) with LinearOrder, BoundedOrder, Fintype; Threshold max wraps Fin max with a coercion to Degree max. These are the discretized carriers used by the gradable-adjective RSA fragment.

structure Degree.Degree (max : ℕ) : Type

A degree on a scale from 0 to max — a discretized continuous value (height, temperature, …).

• value : Fin (max + 1)

def Degree.instReprDegree.repr {max✝ : ℕ} : Degree max✝ → ℕ → Std.Format

Equations

• Degree.instReprDegree.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

@[implicit_reducible]

instance Degree.instReprDegree {max✝ : ℕ} : Repr (Degree max✝)

Equations

• Degree.instReprDegree = { reprPrec := Degree.instReprDegree.repr }

def Degree.instDecidableEqDegree.decEq {max✝ : ℕ} (x✝ x✝¹ : Degree max✝) : Decidable (x✝ = x✝¹)

Equations

• Degree.instDecidableEqDegree.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instDecidableEqDegree {max✝ : ℕ} : DecidableEq (Degree max✝)

Equations

• Degree.instDecidableEqDegree = Degree.instDecidableEqDegree.decEq

@[implicit_reducible]

instance Degree.instInhabitedDegree {n : ℕ} : Inhabited (Degree n)

Equations

• Degree.instInhabitedDegree = { default := { value := ⟨0, ⋯⟩ } }

@[implicit_reducible]

instance Degree.instLinearOrderDegree {max : ℕ} : LinearOrder (Degree max)

Degree max inherits a linear order from Fin (max + 1).

Equations

• Degree.instLinearOrderDegree = LinearOrder.lift' Degree.Degree.value ⋯

@[implicit_reducible]

instance Degree.instBoundedOrderDegree {max : ℕ} : BoundedOrder (Degree max)

Degree max is bounded: 0 is the minimum, max the maximum.

Equations

• Degree.instBoundedOrderDegree = { top := { value := Fin.last max }, le_top := ⋯, bot := { value := ⟨0, ⋯⟩ }, bot_le := ⋯ }

def Degree.allDegrees (max : ℕ) : List (Degree max)

All degrees from 0 to max.

Equations

• Degree.allDegrees max = List.map (fun (x : Fin (max + 1)) => { value := x }) (List.finRange (max + 1))

def Degree.Degree.ofNat (max n : ℕ) : Degree max

Degree from Nat (clamped to max).

Equations

• Degree.Degree.ofNat max n = { value := ⟨min n max, ⋯⟩ }

def Degree.Degree.toNat {max : ℕ} (d : Degree max) : ℕ

The numeric value of a degree.

Equations

• d.toNat = ↑d.value

structure Degree.Threshold (max : ℕ) : Type

A threshold for a gradable adjective: x is "tall" iff degree x > threshold.

• value : Fin max

@[implicit_reducible]

instance Degree.instReprThreshold {max✝ : ℕ} : Repr (Threshold max✝)

Equations

• Degree.instReprThreshold = { reprPrec := Degree.instReprThreshold.repr }

def Degree.instReprThreshold.repr {max✝ : ℕ} : Threshold max✝ → ℕ → Std.Format

Equations

• Degree.instReprThreshold.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

def Degree.instDecidableEqThreshold.decEq {max✝ : ℕ} (x✝ x✝¹ : Threshold max✝) : Decidable (x✝ = x✝¹)

Equations

• Degree.instDecidableEqThreshold.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instDecidableEqThreshold {max✝ : ℕ} : DecidableEq (Threshold max✝)

Equations

• Degree.instDecidableEqThreshold = Degree.instDecidableEqThreshold.decEq

@[implicit_reducible]

instance Degree.instInhabitedThresholdOfNeZeroNat {n : ℕ} [NeZero n] : Inhabited (Threshold n)

Equations

• Degree.instInhabitedThresholdOfNeZeroNat = { default := { value := ⟨0, ⋯⟩ } }

@[implicit_reducible]

instance Degree.instLinearOrderThreshold {max : ℕ} : LinearOrder (Threshold max)

Threshold max inherits a linear order from Fin max.

Equations

• Degree.instLinearOrderThreshold = LinearOrder.lift' Degree.Threshold.value ⋯

def Degree.allThresholds (max : ℕ) : autoParam (0 < max) allThresholds._auto_1 → List (Threshold max)

All thresholds from 0 to max - 1.

Equations

• Degree.allThresholds max x✝ = List.map (fun (x : Fin max) => { value := x }) (List.finRange max)

def Degree.Threshold.toNat {max : ℕ} (t : Threshold max) : ℕ

The numeric value of a threshold.

Equations

• t.toNat = ↑t.value

@[implicit_reducible]

instance Degree.instFintypeDegree {max : ℕ} : Fintype (Degree max)

Equations

• Degree.instFintypeDegree = Fintype.ofEquiv (Fin (max + 1)) { toFun := Degree.Degree.mk, invFun := Degree.Degree.value, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Degree.instFintypeThresholdOfNeZeroNat {max : ℕ} [NeZero max] : Fintype (Threshold max)

Equations

• Degree.instFintypeThresholdOfNeZeroNat = Fintype.ofEquiv (Fin max) { toFun := Degree.Threshold.mk, invFun := Degree.Threshold.value, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Degree.instCoeThresholdDegree {max : ℕ} : Coe (Threshold max) (Degree max)

Coercion: a Threshold embeds into Degree via Fin.castSucc.

Equations

• Degree.instCoeThresholdDegree = { coe := fun (t : Degree.Threshold max) => { value := t.value.castSucc } }

theorem Degree.coe_threshold_toNat {max : ℕ} (t : Threshold max) : { value := t.value.castSucc }.toNat = t.toNat

@[reducible, inline]

abbrev Degree.deg (n : ℕ) {max : ℕ} (h : n ≤ max := by omega) : Degree max

Construct a degree by literal: deg 5 : Degree 10.

Equations

• Degree.deg n h = { value := ⟨n, ⋯⟩ }

@[reducible, inline]

abbrev Degree.thr (n : ℕ) {max : ℕ} (h : n < max := by omega) : Threshold max

Construct a threshold by literal: thr 5 : Threshold 10.

Equations

• Degree.thr n h = { value := ⟨n, h⟩ }

DegP compositional taxonomy

inductive Degree.DegPType : Type

The compositional structure of a Degree Phrase (DegP).

In all degree frameworks, DegP is the syntactic locus where degree comparison happens. The internal structure varies — Kennedy posits [DegP [Deg -er/as/est] [DegComplement than-clause]], Heim posits a sentential -er operator — but the framework-independent taxonomy is captured here.

• comparative : DegPType

  -er / more.

• equative : DegPType

  as...as.

• superlative : DegPType

  -est / most.

• excessive : DegPType

  too.

• sufficiency : DegPType

  enough.

@[implicit_reducible]

instance Degree.instDecidableEqDegPType : DecidableEq DegPType

Equations

• Degree.instDecidableEqDegPType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instReprDegPType : Repr DegPType

Equations

• Degree.instReprDegPType = { reprPrec := Degree.instReprDegPType.repr }

def Degree.instReprDegPType.repr : DegPType → ℕ → Std.Format

Equations

• Degree.instReprDegPType.repr Degree.DegPType.comparative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.DegPType.comparative")).group prec✝
• Degree.instReprDegPType.repr Degree.DegPType.equative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.DegPType.equative")).group prec✝
• Degree.instReprDegPType.repr Degree.DegPType.superlative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.DegPType.superlative")).group prec✝
• Degree.instReprDegPType.repr Degree.DegPType.excessive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.DegPType.excessive")).group prec✝
• Degree.instReprDegPType.repr Degree.DegPType.sufficiency prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.DegPType.sufficiency")).group prec✝

Kennedy-style classification carriers

inductive Degree.PositiveStandard : Type

Positive form standard: how the contextual threshold is determined. For open scales, the standard is the contextual norm ([Ken07]); for closed scales, it is the relevant endpoint fixed by Interpretive Economy.

• contextual : PositiveStandard

  Open-scale: θ = norm relative to comparison class.

• minEndpoint : PositiveStandard

  Lower-bounded: θ = minimum (e.g., "bent", "wet").

• maxEndpoint : PositiveStandard

  Upper-bounded / closed: θ = maximum (e.g., "full", "dry").

• functional : PositiveStandard

  Necessity standard: θ = minimum value for pursuit ([Bel25]).

@[implicit_reducible]

instance Degree.instDecidableEqPositiveStandard : DecidableEq PositiveStandard

Equations

• Degree.instDecidableEqPositiveStandard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instReprPositiveStandard : Repr PositiveStandard

Equations

• Degree.instReprPositiveStandard = { reprPrec := Degree.instReprPositiveStandard.repr }

def Degree.instReprPositiveStandard.repr : PositiveStandard → ℕ → Std.Format

Equations

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

def Degree.PositiveStandard.RequiresComparisonClass : PositiveStandard → Prop

Whether the positive standard depends on contextual domain information.

[Ken07] argues the comparison class is not a semantic argument of pos (contra [Kle80]), replacing it with the standard-fixing function s: ⟦pos⟧ = λg.λx. g(x) ≥ s(g). For relative (open-scale) adjectives, s still requires contextual domain information; for absolute (closed-scale) adjectives the standard comes from scale endpoints via Interpretive Economy.

Equations

• Degree.PositiveStandard.contextual.RequiresComparisonClass = True
• Degree.PositiveStandard.minEndpoint.RequiresComparisonClass = False
• Degree.PositiveStandard.maxEndpoint.RequiresComparisonClass = False
• Degree.PositiveStandard.functional.RequiresComparisonClass = True

@[implicit_reducible]

instance Degree.instDecidablePredPositiveStandardRequiresComparisonClass : DecidablePred PositiveStandard.RequiresComparisonClass

Equations

• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.contextual = isTrue Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_1
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.minEndpoint = isFalse Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_2
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.maxEndpoint = isFalse Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_3
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.functional = isTrue Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_4

inductive Degree.AdjectiveClass : Type

Kennedy's adjective classification by scale structure and standard type [Ken07] [KMcN05], plus a nonGradable case for adjectives outside the degree-based fragment.

• relativeGradable : AdjectiveClass

  Standard varies with comparison class — tall, expensive, big.

• absoluteMaximum : AdjectiveClass

  Threshold fixed at scale maximum — full, straight, closed, dry.

• absoluteMinimum : AdjectiveClass

  Threshold fixed at scale minimum — wet, bent, open, dirty.

• mildlyPositive : AdjectiveClass

  Necessity-relative threshold — decent, acceptable ([Bel25]).

• nonGradable : AdjectiveClass

  Non-gradable: no degree argument, no scale — atomic, prime, deceased, pregnant. Outside the gradable (DirectedMeasure) system; consumers that classify a general adjective should map non-gradables here rather than coercing them into a gradable class.

def Degree.instReprAdjectiveClass.repr : AdjectiveClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instReprAdjectiveClass : Repr AdjectiveClass

Equations

• Degree.instReprAdjectiveClass = { reprPrec := Degree.instReprAdjectiveClass.repr }

@[implicit_reducible]

instance Degree.instDecidableEqAdjectiveClass : DecidableEq AdjectiveClass

Equations

• Degree.instDecidableEqAdjectiveClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.AdjectiveClass.IsRelative (c : AdjectiveClass) : Prop

Coarse two-way classification: relative vs absolute. Collapses absoluteMaximum and absoluteMinimum.

Equations

• c.IsRelative = (c = Degree.AdjectiveClass.relativeGradable)

@[implicit_reducible]

instance Degree.instDecidablePredAdjectiveClassIsRelative : DecidablePred AdjectiveClass.IsRelative

Equations

• Degree.instDecidablePredAdjectiveClassIsRelative c = decEq c Degree.AdjectiveClass.relativeGradable