Re: Motion33 - an ambiguity in draft Level 2 text
P1788
I wish to clarify a point that came up in the discussion on Motion 33.
On 17 Apr 2012, at 13:04, Vincent Lefevre wrote:
> On 2012-04-17 01:12:19 -0700, Dmitry Nadezhin wrote:
>> 2) Do your (A1)-(A5) definitions define "number format" F as a finite
>> set of extended reals or F is a set of pairs (x, f) with x - extended
>> real (as in draft level 2) ?
>
> I don't think a difference between both views will appear in the
> standard. Even the current definition is a bit ambiguous and needs
> to be documented at the language level. For instance, in ISO C, if
> you write
>
> typedef t2 t1;
>
> then t1 and t2 designate the same type.
Vincent is right about the ambiguity.
First, IMO it's OK to regard a number format, informally, as just a finite subset F of Rbar. But don't forget, when it's relevant, that each member of a number format F "knows" what format it belongs to; I formalized this in the draft Level 2 text by defining F as a set of pairs (x, f) with x an extended real and f a name for the format. Similarly for an interval type T.
The ambiguity I was trying to evade to keep things simple, but which Vincent uncovers, is: Is it OK for F or T to have more than one name? I would say definitely Yes. That is, the name uniquely identifies the format or type, but not necessarily vice versa. E.g. it is handy to refer to an IEEE 754 format by either a long or a short name such as binary64 or b64. Though 1788 is below the language level, Vincent's ISO C example expresses what I mean. After binary64 has been defined, 1788 needs a way to say something equivalent to
typedef binary64 b64;
after which binary64 and b64 designate the same format. Reconciling this with the "F is a set of pairs (x, f)" machinery seems a bit tedious: does anyone have a concise way to express it?
John Pryce