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

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

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

I wasnâ€™t aware of Float.prec and Float.succ and this is exactly what I needed.