Understanding Bankers' Rounding for Posits

[CrashAndSideburns]

Hello,

I am currently working on a formalised implementation of posits and posit arithmetic in the Coq programming language. My hope is that this will make it possible to write computer-checkable proofs of the correctness of some numerical algorithms making use of posits.

As part of this, I need to formally specify the rounding behaviour of posits, which has proven a bit tricky. For various reasons related to Coq, it is desirable to speak of rounding as a relation, so we might say that "x ~ f" if the real number x rounds to the posit f. The difficulty, then, is how this relation ought to be specified. For the usual bankers' rounding, this isn't too bad. x rounds to f if f is the unique closest float to x, or else if it is the closest float to x with even fractional part. The issue for the variant of bankers' rounding which posits demand is precisely what "closest" means. The algorithm given for posit rounding in the standard does not always round a real number to the (Euclidean) closest posit. For instance, in the posit-8 format, the number 144179.2 is contained between the posits 65536 and 262144, but is greater than 131072, the posit-9 obtained by suffixing a 1 bit to the 8-posit 65536. As such, 144179.2 will round to 262144, in spite of the fact that this is a greater (Euclidean) distance than that to 65536. As such, it's not quite clear to me what is meant by the "closest" posit.

I could certainly just implement the rounding algorithm, but this has some undesirable properties in the context of proving theorems about posits in Coq. As such, I was hoping that there was some sense in which the rounding rules for posits could be phrased in terms of a simple mathematical property relating real numbers to posits, rather than as an algorithm for performing rounding.

Best regards,

Morgan Arnold

[Angelo Bulfone]

When there is no mantissa, then the rounding happens logarithmically rather than linearly. It's less that 144179.2 > 131072 so much as log₂(144179.2) ≈ 17.14, which is closer to 18 than to 16. The point at which this will start happening could probably be calculated depending on the bit width. I'm not sure how to describe it for cases where rounding would happen right at the boundary of two different fields, where you're rounding the mantissa value into the exponent, or the exponent value into the regime, though.

[Morgan Arnold]

Thanks for the clarification! I suspect that the algorithm described might be definable by some property like "if one of the two adjacent posits surrounding x has two exponent bits, then perform linear bankers' rounding, otherwise perform logarithmic bankers' rounding," but I also agree that it's not immediately obvious to me if this rule applies where rounding happens at the boundary of two different bit fields. Maybe it is the case that there's a nice-ish way to break the real line up into a few different "rounding régimes," so to speak? It's just not obvious to me precisely how to make that separation.

- Morgan
-------- Original Message --------

--
You received this message because you are subscribed to a topic in the Google Groups "Unum Computing" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/unum-computing/6qsygf69i1M/unsubscribe.
To unsubscribe from this group and all its topics, send an email to unum-computin...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/unum-computing/208ba14f-c059-4a20-ad28-d9f9a6947678n%40googlegroups.com.

[John Gustafson]

This is a common misconception about "closest" that affects both float rounding and posit rounding.

The idea is to think of what the bit string would look like if you had infinitely many bits, and round that as a binary fraction would round. Do not think about what the closest real number is, just look at the binary. In practice, all you actually need is one additional bit of precision. If working in n bit precision, find the value to n+1 bits and then notice if that expresses the value exactly (all bits after n+1 are zero bits) or if there is at least 1 bit after that. If it is exact, choose the flanking binary n-bit fraction that is even. Otherwise, the presence of trailing bits (sometimes summarized as the "sticky bit", or for unum arithmetic, the ubit) indicates the need to round upward when the n+1 bit is a 1.

As I said, this works for both floats (default rounding) and for posits.

John

--
You received this message because you are subscribed to the Google Groups "Unum Computing" group.
To unsubscribe from this group and stop receiving emails from it, send an email to unum-computin...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/unum-computing/5e7baa53-9c06-4f3d-bb7d-0998c79561f7n%40googlegroups.com.

[John Gustafson]

Yes, the rounded bit can belong to the exponent, in which case the midpoint is the geometric mean of the two points instead of the arithmetic mean. If logarithmic binades are used instead of linear binades, every rounding is to the logarithmically nearest value.

We discovered early on that this is a major source of bugs in posit implementations (like in software emulators) so we nicknamed it the "Twilight Zone."

John

--
You received this message because you are subscribed to the Google Groups "Unum Computing" group.
To unsubscribe from this group and stop receiving emails from it, send an email to unum-computin...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/unum-computing/208ba14f-c059-4a20-ad28-d9f9a6947678n%40googlegroups.com.

[Nathan Waivio]

I think an important thing to formally prove in Coq would be that there is an isomorphism between a Rational Cauchy Sequence and the infinite bit Posit that John described above.  That would build a pretty solid foundation where the infinite stream of Posit bits would be a construction of Real numbers in the same sense that the Rational Cauchy Sequence is a construction of real numbers.  Then the rounding to a finite representation would give the closest posit finite approximation of the real number.

After reading "Every Bit Counts" and my experience implementing elementary functions in my Haskell soft posit implementation, I believe it to be true but don't have real mathematical proof.

Nathan.

To view this discussion visit https://groups.google.com/d/msgid/unum-computing/26784A61-0D89-4C94-8C21-8FC09F1A6484%40earthlink.net.

[Morgan Arnold]

Hi Nathan,

I'm quite sure that this is false, but only mildly so. All posits (including "infinite bit length" ones) are computable numbers, but the limit of a rational Cauchy sequence is not in general computable (indeed, this limit could be any real number, and almost all real numbers are uncomputable. If you restrict only to the set of Cauchy sequences with some prescribed modulus of convergence, however, you get the computable real numbers, and it is true. Posits are isomorphic to the computable real field, certainly, but are not a model of the reals.

Best,

Morgan
-------- Original Message --------

You received this message because you are subscribed to a topic in the Google Groups "Unum Computing" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/unum-computing/6qsygf69i1M/unsubscribe.
To unsubscribe from this group and all its topics, send an email to unum-computin...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/unum-computing/CACprBhbnjU-03PmN7qkQ1mgSzA90smPXWwoOH8L9TtDhnvyhfA%40mail.gmail.com.

[Nathan Waivio]

Thanks for the clarification.  It never occurred to me that a rational Cauchy sequence would not be computable.  I was assuming that it would be an infinite convergent process, that would be terminated by rounding to a finite posit number of bits.  The Table Maker's Dilemma probably also throws a wrench into things as well.

Thanks for the corrections.

[John Gustafson]

Morgan,

If you use Dedekind cuts to define the reals, but restrict the rational numbers to those with integer powers of 2 in the denominator, then Dedekind cuts still work. Which means posits of unlimited precision do model the reals.

Best,

John

To view this discussion visit https://groups.google.com/d/msgid/unum-computing/8gqi27kAu4mnDxdTvtu5ggkQXs0EIZabycegADaUdch9ocddGqneB5IkFoAqI9_8WzD_LE5lJ3bMiUvfLHRVuJxv04CaCpED2ebREoRPfyA%3D%40proton.me.