Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0016 — Numeric tower: exact by default

  • State: committed
  • Opened: 2026-06-05
  • Decides: the runtime representation and arithmetic semantics of the numeric tower — specifically that Real is exact (arbitrary-precision rational), Decimal/Money are exact, and machine floats (f32/f64) are the explicit opt-in inexact types; how the reasoner’s value domain represents numbers; and that aggregate folds (sum/avg/min/max) are exact. Resolves the “finer breakdown of the tower … deferred to a follow-up RFD” note in §17.1.

Question

§17.1 lists Real as “real number; runtime-chosen representation (defaults to IEEE 754 f64)” and defers the finer tower (rationals, fixed-point) to a follow-up RFD. But the substrate is already ahead of the book: the slice-4 mutation semantics (Argon/Runtime/MutationSemantics.lean:85) models Value.real : Rat — an exact rational — with exact parseDecimal, toRat, and evalRatBinary. Meanwhile the reasoner’s catalog value domain has no numeric beyond Int (a Real/Decimal/Money literal round-trips as opaque CBOR), so an aggregate like sum(r.value for r in …) where value: Real cannot fold at all.

What is Real’s representation, what does the reasoner store, and is avg exact? And which wins — the book’s “f64” or the Lean’s exact rational?

Context

  • Domain. Argon’s flagship workloads are finance and legal (the residential-lease / accounting overlay). For that domain IEEE-754 f64 is a bug generator: 0.1 + 0.2 ≠ 0.3, summed payments drift, and cumulative-satisfaction checks (e.value <= sum(r.value …)) become subtly wrong at the boundary. Exactness is a correctness requirement, not a nicety.
  • The Lean already chose exact. MutationSemantics.lean models Real as Rat deliberately (“the spec’s arithmetic is exact”). Per the project’s own rule — where the book disagrees with the Lean on something the Lean covers, the Lean wins; the book is a bug — §17.1’s “f64 default” is the bug.
  • avg wants a field. avg over a Real collection is Σ / n. Over rationals this stays exact (rationals are closed under division); over fixed-precision decimals or floats it rounds. Exact Real is what makes avg mathematically clean.
  • The reasoner gap. oxc-reasoning’s Value has Int(i64) but no exact Real/Decimal; the fold is Int-only. This blocks the overlay’s Met rule (the motivating case) and any Real/Money aggregate.

Decision

  1. Real = exact, arbitrary-precision rational. Numerator/denominator big integers; no precision ceiling; no implicit rounding. This is the canonical Real for the data/ontology substrate.
  2. Decimal and Money are exact. Decimal is arbitrary-precision base-10; Money is a currency-tagged Decimal. Both share the exact-rational carrier in the reasoner (a Decimal is a rational whose denominator is a power of ten); the currency tag and display scale are metadata on top. Money arithmetic (§17.1, D-069) is unchanged in typing; only its representation becomes exact.
  3. Floats are the explicit opt-in inexact tier. f32/f64 live in std::math::primitive (already the case) and are the only inexact numerics. Real never silently becomes a float. The implicit-widening chain keeps Int → Real (exact ⊆ exact) but the f32 → f64 → Real step is removed — a float reaches Real only via an explicit, lossy to_real-style conversion (a float is not exact, so widening it into the exact tier must be a visible choice).
  4. The reasoner value domain carries exact numerics. oxc-reasoning’s Value gains an exact-rational variant; Real/Decimal/Money literals materialize to it (replacing the opaque-CBOR/f64 path). Mirrors MutationSemantics.Value.real : Rat.
  5. Aggregate folds are exact. sum/min/max/avg fold over the exact domain: integer-exact when all operands are Int, else promoted to exact rational; avg stays exact (Σ/n as a rational). This mirrors MutationSemantics.foldAggregate.
  6. §17.1 is corrected to describe Real as exact arbitrary-precision rational (not f64), and the deferral note is resolved by this RFD.

Rationale

  • Correctness-first for the domain. A financial/legal substrate that silently rounds is unfit for purpose; exact-by-default makes “the numbers are right” the default, with floats available when a modeler explicitly wants approximate/scientific compute.
  • The Lean is the source of truth. Adopting exact rationals aligns the reference and the implementation to the already-mechanized MutationSemantics; it is reconciliation, not invention.
  • avg exactness is a concrete, checkable win unavailable under float or fixed decimal.
  • Implementation. The Rust reasoner uses num-rational::BigRational over num-bigint (MIT/Apache-2.0, on the workspace allow-list) — arbitrary precision, exact division, deterministic Ord/Hash over normalized components. Not rust_decimal (96-bit fixed; would diverge from the Lean Rat carrier and cap precision).

Alternatives considered

  • Real = f64 default (status quo §17.1). Rejected: float drift is a correctness bug for the domain; contradicts the Lean.
  • Real = fixed-precision Decimal (e.g. rust_decimal, 96-bit). Rejected: caps precision, rounds division (so avg is inexact), and diverges from the Lean’s Rat carrier.
  • Defer (keep folding Int-only). Rejected: blocks the motivating Met rule and every Real/Money aggregate; the deferral was already taken once in §17.1 and this RFD is its resolution.

Follow-ups

  • L5 — exact avg + a Reasoning/Aggregate.lean fold theorem (the interval/fold characterization; closes the Lean item of issue #52).
  • R4 — oxc-reasoning exact Value variant + exact encode_tuple + exact sum/min/max/avg fold mirroring MutationSemantics.foldAggregate; oxc-runtime literals → exact value (replace the opaque-CBOR path).
  • A future RFD may add custom-precision fixed-point / refinement-driven width selection (the remaining tail of §17.1’s deferral); not needed for exact-by-default.