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:

- No rounding:
`q`

is exactly represented as `f`

, hence `q \in [f, f]`

- Rounded up:
`f`

is â€śjust aboveâ€ť `q`

, hence `q \in [Float.pred f, f]`

- 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

Thanks for your great answer.

I wasnâ€™t aware of `Float.prec`

and `Float.succ`

and this is exactly what I needed.

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