Proposed M0005: JDP response about aformat and signed zero
P1788 members
Here I expand on the definition of an "aformat" in item 6 of M0005's Rationale. Arnold Neumaier makes several comments that show he has misunderstood my text, or its references to the 754 standard. I apologise again for the slowness in replying, due to my having just moved into a house that still lacks many basic amenities.
M0005:
>> 6. A floating-point "abstract format" ("aformat") F is a finite subset of R*
>> such that at least -oo and +oo are elements of F.
AN wrote on 13 May 2009:
> Note what this implies:
>
> Calling it a subset precludes
> 1. the possibility of differentiating between +0 and -0.
> 2. having NaN's.
> The Vienna Proposal takes a more liberal view,allowing F to be a
> finite set, together with a partial value map into R^*.
Yes, I intend indeed to preclude this. This is already implied by the commutative diagram in eqn (3) on p.5 of Motion 2's position paper P1788/PP008, and the surrounding discussion, but the implication may not have been obvious.
Both "signed zero" and "NaN" at this point are meaningless concepts, and I have deliberately constructed the theory so that this is the case. Arnold, I believe you are -- as the Vienna proposal occasionally does -- confusing an object with its representation. If you had attended to what is written, instead of what you think I wrote, or maybe what you think I should have written, you would have seen this.
> (The wording in the Vienna Proposal is optimized in many places for
> maximal conceptual clarity...
Conceptual clarity is in the eye of the beholder. My words are simple and precise.
> One should also require 0 to be in F; otherwise one gets into
> trouble with interval extensions of abs(x)...
Of course any sensible F will have 0 in it but it is not logically required for the present discussion so I do not assume it. Some F might cause
abs([-1,1]) to return [-12.3, +45.6].
That would be silly, but does not cause a contradiction in my subsequent theory.
A few lines lower down:
M0005:
>> <754>A format in the 754 sense shall be identified with the aformat comprising
>> those extended-real numbers that are exactly representable in that format,
>> where -0 and +0 both represent 0.
AN:
> The 754 format does not conform to your definition of an abstract
> format a few lines above, since the set of IEEE floats are not a
> subset of R^*.
It is not explicitly stated in 754, but clear from 754 Definitions 2.1.24 and 2.1.25, from 754¤3.2, and the definition of the arithmetic operations, that a "floating-point number" (that is, any floating-point datum that is not NaN) *is* a member of R^*. (How else to read statements like "the floating-point number nearest to the infinitely precise result shall be delivered" in 754¤4.3.1?)
*Except* for one special case, namely that the point 0 in R^* is given a sign, which splits it into two datums -0 and +0, that are treated the same by most operations, but not by all.
Therefore my definition is correct. Take all the datums [I prefer to use "datums" as the plural since "data", though correct, is usually regarded as a singular noun these days] that comprise a given 754 format. Discard NaN. Strip the sign from the zeros. The result is a subset of R^*, which is the associated aformat.
Recapitulation of what level 2 is.
==================================
Floating-point (FP) level 2 as 754 does it
------------------------------------------
For a given format, the FP datums form a finite set of abstract objects. This abstract set (754 Table 3.1) is where one should, and 754 does, define the FP computational operations, independent of representation issues for the most part. The abstract set, and the operations on it, form FP level 2 (for a particular format).
In 754, the set of FP numbers (= all FP datums except NaN) is *nearly* but not quite a subset of the mathematical (level 1) number system R^*. The exceptions, -0 and +0, cause no end of trouble:
- It's hard to remember whether, for instance, (-0) - (-0) is -0 or +0, and
whether this depends on the rounding mode.
- Worse, 754's "equals" predicate is *not* the "equals" of set theory. -0 and
+0 compare equal, but 1/(-0) and 1/(+0) compare unequal, which elsewhere in
mathematics would be called a contradiction in terms for any predicate
deserving the name "equals".
That 754 should cause this situation, by creating -0 and +0, was probably inevitable given the underlying sign-exponent-significand representation. P1788 doesn't have to make a similar mess!
Interval level 2 as I propose it
---------------------------------
I have constructed the theory so that the following are true.
For a given aformat F, the interval datums form a finite set IR_F of abstract objects. This abstract set is where one should, and I do, define the interval computational operations, *entirely* independently of representation issues -- except for accuracy (tightness) issues, which can and should be handled independently. The abstract set, and the operations on it, form interval level 2 (for a particular aformat).
In my system, the set IR_F -- after discarding NaI, should we decide to have this -- is *entirely* a subset of the mathematical interval system IR. (Namely those mathematical intervals whose endpoints are in F, together with the empty set.)
By Motion 2, P1788's mathematical intervals are exactly
the closed connected subsets of R,
same as Vienna proposal's textbook intervals.
A level 2 interval datum is either a textbook interval
whose endpoints belong to a particular set, or NaI.
No exceptions.
To my mind this counts as "conceptual clarity".
Consequences
------------
Let me point out some things that are at stake here.
- By defining level 2 in this way (for each implemented format)
- to comprise a set of abstract objects
- that form an "algebraically closed system", cf. 754 Table 3.1
- and that, apart from NaI, *are* textbook intervals
- we make Moore's Basic Theorem of Interval Arithmetic true
- for mixed-format arithmetic expressions
- with a simple, undergraduate-level proof
- independent of anything we may subsequently decide about
- representation,
- implementation,
- contents of elementary function libraries,
- tightness requirements for elementary functions,
- set of supported formats,
- etc.
- Furthermore, we make equality of intervals mean exactly the same
at level 2 as at level 1, namely set-equality.
Such a level 2 offers a rock-solid foundation for P1788.
If we do not define such a level 2, I am not saying Moore's Theorem will be false. But it may be (which would be a catastrophe!) and a proof is likely to be far more messy than the one I have outlined in the Rationale.
It is obvious that I have nailed the colours of the "set paradigm" firmly to my mast. Intervals are sets. Arnold: they are not ordered pairs of numbers at this level; only at the level of representation do questions about -0, +0 and NaN become meaningful.
Does this stance mean I regard collaboration with the modal interval folk as impossible? By no means. As soon as I can I will comment on that. Also on the "flags & tags" thread that Dan, Vincent, Nate & others have been discussing.
Sorry again to be so behind-hand. With luck, today I shall have a phone line and broadband installed at home. Up till then I have had to go to the town's new library to communicate.
Oh dear... it is the official opening of the library by Princess Anne! So I have had to go elsewhere to access the internet...
Best wishes
John Pryce