exact #

Exact rational reference answers for checking floating-point computations.

A reference answer computed in floating point carries the same rounding errors as the code it is meant to check. exact computes its answers with Zarith rationals instead, and rounds to binary64 only when asked.

Exact.Ieee does IEEE-754 binary64 rounding and arithmetic on rationals. Exact.Decimal reads a decimal literal exactly and names the binary64 a parser should return; Exact.Witness lists the literals where that answer is hardest to get right. Exact.Discrete gives binomial and hypergeometric probabilities, tails included, as ratios of integers. Exact.Interval puts a transcendental value between two rational endpoints, with the series tail bounded explicitly.

It belongs in tests, audits and reference computations. Hardware floating point stays on the production hot path.

Installation #

opam install exact

Usage #

Fisher's exact test takes as its p-value the two-sided tail, the summed probability of every outcome no more likely than the observed one. With 3 draws from 10 items of which 4 are successes, P(X = 0) to P(3) are 20/120, 60/120, 36/120 and 4/120. Nothing else is as rare as X = 3, so for an observed 3 the tail is 4/120 = 1/30. The comparison is between rationals, so two equally likely outcomes always compare equal:

let law =
  Exact.Discrete.hypergeometric ~population:10 ~successes:4 ~draws:3

let tail = Exact.Discrete.two_sided law 3
let () = assert (Q.equal tail (Q.make Z.one (Z.of_int 30)))

Rounding 1/10 to binary64, nearest with ties to even, gives the bits of 0.1:

let one_tenth = Q.make (Z.of_int 1) (Z.of_int 10)

let bits =
  Exact.Ieee.of_rational Exact.Ieee.Nearest_even one_tenth

let () = assert (Int64.equal bits (Int64.bits_of_float 0.1))

The JSON literal 0.1 is exactly 1/10, and a correct parser returns the same bits:

let literal = Option.get (Exact.Decimal.v Exact.Decimal.Json "0.1")

let () =
  assert (Q.equal (Exact.Decimal.value literal) (Q.make Z.one (Z.of_int 10)));
  assert (
    Int64.equal
      (Exact.Decimal.bits Exact.Ieee.Nearest_even literal)
      (Int64.bits_of_float 0.1))

Exact.Interval.pi () encloses π strictly inside 333/106 and 355/113:

let pi = Exact.Interval.pi ()

let () =
  assert (Q.lt (Q.make (Z.of_int 333) (Z.of_int 106)) (Exact.Interval.lo pi));
  assert (Q.lt (Exact.Interval.hi pi) (Q.make (Z.of_int 355) (Z.of_int 113)))

API #

• Exact.Decimal: decimal literals under the C, C++ from_chars and JSON grammars, and the binary64 each of three parser routes should return.
• Exact.Discrete: finite probability laws and their tails.
• Exact.Ieee: classification, conversion and arithmetic for binary64.
• Exact.Interval: rational enclosures of transcendental functions.
• Exact.Witness: decimals on binary64 rounding boundaries, each with the bits a correct parser must return.

The module interfaces carry the full documentation.

Related work #

• stats computes descriptive statistics and regressions over floating-point samples; exact is what you check such code against.
• interval is a general OCaml interval-arithmetic library. Exact.Interval is much narrower: rational enclosures with explicit tail bounds, for use as test oracles.
• mlmpfr binds MPFR's arbitrary-precision floating-point arithmetic. exact needs only Zarith.
• zar provides formally verified sampling from discrete distributions. Exact.Discrete never samples; it computes the probabilities.

Licence #

ISC. See LICENSE.md.