[HN Gopher] Relational Floating-Point Arithmetic [pdf]
___________________________________________________________________
Relational Floating-Point Arithmetic [pdf]
Author : 082349872349872
Score : 26 points
Date : 2023-01-30 10:44 UTC (12 hours ago)
(HTM) web link (www.cs.toronto.edu)
(TXT) w3m dump (www.cs.toronto.edu)
| hedora wrote:
| Range / interval arithmetic solves(?) these problems with a 2x
| overhead (in space + time) vs. the exponential overhead the paper
| gets:
|
| https://en.wikipedia.org/wiki/Interval_arithmetic
| klodolph wrote:
| I think you may be missing the context of what the paper is
| presenting, here. It looks like the paper is solving relations
| between floating-point numbers--for example, "3.4 + x = 3.4;
| solve for x" is of the examples from the paper.
|
| Note that there are solutions other than x = 0.
| CoastalCoder wrote:
| > A floating-point number system F (, p, L,U ) is characterized
| by a base [?] N, precision p [?] N, and lower and upper
| exponential range L,U [?] Z.
|
| IIUC, this paper describes an approach to formally modeling
| schemes such as like IEEE-754 floats.
|
| I don't work with formal systems / proof assistants, but this
| _sounds_ like step in the right direction for modeling floating-
| point computations.
|
| But I have to wonder though about their treatment of NaN:
|
| > We exclude NaN values which represent undefined arithmetic
| operations.
|
| AFAIK, IEEE-754 has very well-defined rules for how NaN values
| behave, including signaling / non-signaling options. I think
| their model will have limited applicability until they extend it
| to fully model this.
| jcranmer wrote:
| > AFAIK, IEEE-754 has very well-defined rules for how NaN
| values behave.
|
| If you model NaNs with no more specificity than there is a NaN,
| then IEEE-754 is very well-defined. If you consider NaN
| payloads, then IEEE-754 is underdefined (and hardware is
| notably divergent here).
| dbcurtis wrote:
| Notably divergent, and notably hard to get correct. (I have
| some experience validating the correctness of 754 arithmetic.
| I suspect nobody gets it perfect.)
| mncharity wrote:
| Curious - any suggested reading?
|
| I've recently been exploring how to approach collaborative
| compilation in a compiler backend. Thorough control of a
| mere numeric literal and binop spike turned out a rich in
| challenge.
| CoastalCoder wrote:
| It sounds like my understanding might be incomplete, could
| you expand on your comment?
|
| IIRC, IEEE-754 includes several _options_ for what should
| happen when various operations consume or could create NaN
| values. (As well as underflow, overflow, etc.) But that all
| of those options _are_ covered by the spec.
|
| So, e.g., a modern x86-64 processor supports various FP modes
| (NaN signalling, etc.), and all of those FP modes result in
| behavior that's well-defined by IEEE-754.
|
| Is that not the case?
|
| EDIT: TIL about "NaN payloads". Now the parent comment makes
| more sense to me.
| nerdponx wrote:
| Does this have any practical uses, or is this just an attempt to
| push the limits of relational programming? For example, can you
| use this system to derive new compile-time optimizations? Or can
| you use it to formalize compile-time floating-point arithmetic in
| languages with refinement types or dependent types? The latter is
| a well-known pain point in Idris, for example.
___________________________________________________________________
(page generated 2023-01-30 23:02 UTC)