OM Floats

[David Carlisle]

> If you want to represent IEEE infinities and NaNs, then you may wish
> to revisit this. It may be a mistake to use floats in decimal or hex at all. 

I don't, particularly, and the core CDs do contain symbols that
represent NaN and various notions of infinite number.

However it is (I presume) useful for the OM Float type to be able to
accept any value that is allowed by IEEE double precision floats,
as you either have to allow them, or to mandate that every phrasebook
picks these up and substitutes these values with the appropriate
OpenMath Symbol.

> Exactly not the case.  As Bruce Miller points out,
> To have the precision of a number depend on the number of
> decimal digits you happen to write down is a terrrrrible rule.

But that isn't the rule.
Currently OMF has a fixed precision (double).

There are some systems that need _exact_ reals, rather than reals to
some specifiable precision.
If I asked a theorem proving system whether

> 2.0
was equal to
> 1.99999999999999999999999999999999999999999999999999

I would be shocked if it said true no matter how many 9s were there.
Obviously input/output of exact real values, e, sqrt(2), ...
requires more than decimal expansions, but that is not the point
here: a finite decimal expansion does have an exact value in |R
and it makes sense to have some OpenMath symbols that allow such values
to be encoded, even though the OMF primitive type is not suitable for
this use, being of fixed precision.

There is also a need for numbers of a specified (but not fixed by the
system) precision.

In fact as this thread is showing there are many different possible
requirements for `floating point numbers' which is why I think that
using a mechanism of constructing them from a constructor symbol in a CD
gives much more flexibility, and the current OMF should be kept as
currently specified, solely for double precision values.

> At the substantial risk of belaboring this
> point, I disagree with Gaston on the feasibility
> of leaving out floats: it is feasible for OM to convey numeric
> rationals only. 

True, and rationals are a good example, OpenMath does not have a
primitive notion of rationals, but the core set of CDs contain a
rational constructor symbol that takes two integers with the obvious
semantics. All I am arguing is that we should treat floats similarly
(by the way, this is _me_ arguing: this thread is not arguing any
`agreed position' of the esprit consortium, I just started it myself
as we've been working through the draft standard trying to bring it in
to line with the discussions at Eindhoven, and got to this point...)

I agree with Bruce that if we do this then the core set of CDs should
have a CD that gives suitable symbols.

One could then have symbols that more or less directly encoded your

> (float-type=:IEEE-double, values= signed hex-pairs)
or
> You could also use rational number specifications..

David