Pragmatic Halo and Precision Modes

@cite{krifka-2007} @cite{lasersohn-1999} @cite{woodin-etal-2023} @cite{kao-etal-2014-hyperbole}

Rounding semantics for numeral imprecision. Round numbers (100, 1000) are interpreted imprecisely; sharp numbers (103, 1001) are interpreted precisely. This is the "pragmatic halo" effect.

inductive Semantics.Lexical.Numeral.Precision.PrecisionMode : Type

Precision mode for numeral interpretation.

• exact : PrecisionMode
• approximate : PrecisionMode

instance Semantics.Lexical.Numeral.Precision.instReprPrecisionMode : Repr PrecisionMode

Equations

• Semantics.Lexical.Numeral.Precision.instReprPrecisionMode = { reprPrec := Semantics.Lexical.Numeral.Precision.instReprPrecisionMode.repr }

def Semantics.Lexical.Numeral.Precision.instReprPrecisionMode.repr : PrecisionMode → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Numeral.Precision.instDecidableEqPrecisionMode : DecidableEq PrecisionMode

Equations

• Semantics.Lexical.Numeral.Precision.instDecidableEqPrecisionMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Numeral.Precision.instBEqPrecisionMode.beq : PrecisionMode → PrecisionMode → Bool

Equations

• Semantics.Lexical.Numeral.Precision.instBEqPrecisionMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Numeral.Precision.instBEqPrecisionMode : BEq PrecisionMode

Equations

• Semantics.Lexical.Numeral.Precision.instBEqPrecisionMode = { beq := Semantics.Lexical.Numeral.Precision.instBEqPrecisionMode.beq }

def Semantics.Lexical.Numeral.Precision.roundToNearest (n : ℚ) (base : ℚ := 10) : ℚ

Round a rational number to the nearest multiple of base.

Equations

• Semantics.Lexical.Numeral.Precision.roundToNearest n base = if (base == 0) = true then n else have scaled := n / base; have rounded := (scaled + 1 / 2).floor; ↑rounded * base

def Semantics.Lexical.Numeral.Precision.isRoundNumber (n : ℚ) (base : ℚ := 10) : Bool

Check if a number is "round" (divisible by base).

Equations

• Semantics.Lexical.Numeral.Precision.isRoundNumber n base = (Semantics.Lexical.Numeral.Precision.roundToNearest n base == n)

def Semantics.Lexical.Numeral.Precision.roundingEquiv (n₁ n₂ : ℚ) (base : ℚ := 10) : Bool

Rounding equivalence: two values are equivalent if they round to the same number.

Equations

• Semantics.Lexical.Numeral.Precision.roundingEquiv n₁ n₂ base = (Semantics.Lexical.Numeral.Precision.roundToNearest n₁ base == Semantics.Lexical.Numeral.Precision.roundToNearest n₂ base)

def Semantics.Lexical.Numeral.Precision.projectPrecision (mode : PrecisionMode) (n : ℚ) (base : ℚ := 10) : ℚ

Project a value according to precision mode.

Equations

• Semantics.Lexical.Numeral.Precision.projectPrecision Semantics.Lexical.Numeral.Precision.PrecisionMode.exact n base = n
• Semantics.Lexical.Numeral.Precision.projectPrecision Semantics.Lexical.Numeral.Precision.PrecisionMode.approximate n base = Semantics.Lexical.Numeral.Precision.roundToNearest n base

def Semantics.Lexical.Numeral.Precision.matchesPrecision (mode : PrecisionMode) (stated actual : ℚ) (base : ℚ := 10) : Bool

Check if stated and actual values match under a given precision mode.

Equations

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

def Semantics.Lexical.Numeral.Precision.adaptiveBase (n : ℕ) : ℚ

Adaptive rounding base: rounder numbers get a coarser base. Uses RoundnessGrade to avoid duplicating score-binning logic.

Equations

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

def Semantics.Lexical.Numeral.Precision.adaptiveTolerance (n : ℕ) (baseTol : ℚ) : ℚ

Adaptive tolerance: scales a base tolerance by the roundness score.

Equations

• Semantics.Lexical.Numeral.Precision.adaptiveTolerance n baseTol = baseTol * (1 + ↑(Core.Roundness.roundnessScore n) / 6)

def Semantics.Lexical.Numeral.Precision.haloWidth (n : ℕ) : ℚ

Pragmatic halo width as a function of roundness score.

Equations

• Semantics.Lexical.Numeral.Precision.haloWidth n = (if n ≥ 1000 then 50 else if n ≥ 100 then 10 else if n ≥ 10 then 5 else 1) * ↑(Core.Roundness.roundnessScore n) / 6

def Semantics.Lexical.Numeral.Precision.inferPrecisionMode (n : ℕ) : PrecisionMode

Infer precision mode from k-ness score. roundnessScore ≥ 2 → .approximate; roundnessScore < 2 → .exact.

Equations

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

theorem Semantics.Lexical.Numeral.Precision.adaptive_base_ge_five_of_div10 (n : ℕ) (h10 : n % 10 = 0) : adaptiveBase n ≥ 5

Multiples of 10 have adaptive base ≥ 5.