Pragmatic halo and precision modes #
Rounding semantics for numeral imprecision: round numbers (100, 1000) admit imprecise construals; sharp numbers (103, 1001) do not — [Las99]'s pragmatic halo, [Kri07a]'s approximate interpretation.
Main definitions #
PrecisionMode,projectPrecision,roundToNearest: the two meaning projectionsf_e(s) = sandf_a(s) = Round(s)of [KWBG14], withRound= round-to-nearest-multiple.Studies/KaoEtAl2014PMFHyperbole.leangrounds its goal projections in these.haloWidth,inferPrecisionMode: halo width and precision mode as functions of the k-ness score (Roundness.roundnessScore). Only the monotone relationship — rounder numerals carry wider halos and favour approximate construal — is motivated by the cited papers ([WWL+23]'s corpus finding); the magnitude constants and the score threshold are stipulations of this formalisation.
Precision mode for numeral interpretation: which of [KWBG14]'s two meaning projections applies.
- exact : PrecisionMode
Exact interpretation,
f_e(s) = s. - approximate : PrecisionMode
Approximate interpretation,
f_a(s) = Round(s).
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- Semantics.Numerals.Precision.instDecidableEqPrecisionMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Round a rational to the nearest multiple of base —
[KWBG14]'s Round at the default base = 10, the
nearest-representative map of the width-base bucket partition
(Core/Algebra/Order/ToIntervalMod.lean).
Equations
- Semantics.Numerals.Precision.roundToNearest n base = ↑(round (n / base)) * base
Instances For
Rounding moves a value by at most half the grain: the imprecision
introduced by f_a at base 10 is bounded by 5
(abs_sub_round_div_zsmul_le).
Project a value according to precision mode: f_e is the identity,
f_a rounds to the nearest multiple of base.
Equations
Instances For
Halo width and precision-mode inference #
Stipulated operationalisations over the k-ness score. Making the mode a
function of the numeral alone idealises away the contextual choice of
granularity ([Kri07a]) and joint probabilistic inference
([KWBG14]); see the caveat on inferPrecisionMode.
Pragmatic halo width, increasing in the roundness score. The magnitude factors are stipulated, not paper-derived.
Equations
- Semantics.Numerals.Precision.haloWidth n = (if n ≥ 1000 then 50 else if n ≥ 100 then 10 else if n ≥ 10 then 5 else 1) * ↑(Semantics.Numerals.Roundness.roundnessScore n) / 6
Instances For
Infer precision mode from the k-ness score: roundnessScore ≥ 2 yields
.approximate. Known idealisation: score-1 numerals (5, 15, 45, …) come out
.exact even though imprecise uses of them are attested.
Equations
- One or more equations did not get rendered due to their size.
Instances For
PrecisionMode is the two-point instance of the QUD-layer
PrecisionProjection family: f_e is PrecisionProjection.exact; f_a
at grain g rounds within the width-g grain (the lower representative
on the ℕ scale — [KWBG14]'s Round picks the nearest;
same partition, different canonical representative).