Converting an arbitrary precision rational number to a float interval in a sound way

Learning
1

Hi,
In the context of writing a simple arithmetic solver, I am looking for a way to soundly convert an arbitrary-precision rational number with type Zarith.Q.t to a float interval with type:

Interval_crlibm.I.t = {low: float, high: float}

Ideally, the resulting approximation should be as tight as possible. Does anyone have suggestions?

Best,
Jonathan

1 Like
2

An FP puzzle! Great!

Let q be your rational number of type Q.t. Consider the FP number f = Q.to_float q. The doc says that f is q rounded to a nearest representable FP number. So there are three cases:

  1. No rounding: q is exactly represented as f, hence q \in [f, f]
  2. Rounded up: f is “just above” q, hence q \in [Float.pred f, f]
  3. Rounded down: f is “just below” q, hence q \in [f; Float.succ f]

To keep things simple you could pick [Float.pred f, Float.succ f] as your interval. It contains q and is only 2 ulp wide.

If you want the tightest interval, you need to determine which of the three cases above holds. Just convert f back to a rational number (this is exact) and compare with q: Q.compare q (Q.of_float f). If it’s 0 you’re in case 1; if it’s negative you’re in case 2; if it’s positive you’re in case 3.

I haven’t checked all the details, but I hope the above approach makes sense and is not too wrong.

9 Likes
3

Thanks for your great answer.
I wasn’t aware of Float.prec and Float.succ and this is exactly what I needed. :slight_smile:

(Also, sorry for my late reply. I had misconfigured the notification parameters on Discourse.)