🚀 go-pugleaf

In article <19228@brunix.UUCP>, mj@brunix (Mark Johnson) writes:
  [I wrote]
> > It is simply a MISTAKE to think of floating-point numbers as
> > denoting real numbers.  It is indeed the case that
> >         1.0 + scalb(1.0, -60) =:= 1.0
> > must be true in IEEE 754 arithmetic and must be false in the reals, but
> > all this tells us is that floating-point arithmetic is not the same
> > algebra as real arithmetic, which we already knew.
 
> But just because this is the way it is in IEEE 754 doesn't mean that
> this is the way it should be in Prolog.  Maybe floats aren't the most
> appropriate approximation to real numbers in a logic-programming 
> (inspired) language?

Why do you think they were left out of DEC-10 Prolog?
If we wanted to provide some form of 'real' arithmetic in Prolog,
then that's what we should do.  But the unpleasant brute practical
fact is that there are lots of Prolog systems offering FLOATS and
none that I know of offering REALS.  The question is, given that
there are Prologs which offer floating-point arithmetic, what should
they do?

> I found Richard's response to my point about the incompleteness of
> floating-point arithmetic (when expressions are interpreted in the
> reals) a little confusing: I thought that the only reason why floating
> point numbers are used is because they are an approximation to the
> reals.

Sigh.  Yes floating-point numbers approximate (some) reals.  But the
closeness of the approximation doesn't percolate through a computation
in any straightforward manner.  Each separate operation may be a very
good approximation, yet the final result may have the wrong sign or be
wildly out in other ways.  For example, it is possible to find three
floating-point numbers X, Y, Z such that
	X+(Y+Z) = 0.0 but (X+Y)+Z = 1000.0
[To be fair, IEEE 754 demands that INEXACT would be signalled in such a case.]
To establish that the final result of your computation is an acceptable
approximation to the real number you want requires careful reasoning
that takes account of the algebraic properties that the floats actually
possess; you _cannot_ do it by pretending that the floats are reals.

> Isn't the question really just what properties of the reals
> we want our approximation to capture, and whether completeness is one of
> these properties?

No, that is another question.  Prolog implementors don't have much choice:
customers are demanding floats, and what they want is floats that are the
same as floats or doubles in C or Fortran or Pascal or Lisp.  If you have
a Prolog-to-C interface as Quintus, BIM, IF, SICStus, NU, ALS, Arity, LPA,
and many other Prologs have, even if you did put in a splendid logically
defensible approximation of 'real' arithmetic, people would still demand
that the floating-point numbers they had in C should be made available in
Prolog, and you would be left with the question of what to do with them.
We don't have the luxury of designing floating-point arithmetic; that has
already been perpetrated.

> Nevertheless, in such a system  X =:= (X * 16.0) / 16.0, since the intervals
> on either side of the =:= have a non-empty intersection so I think my
> original claim about the completeness of interval arithmetic still stands.

If you are going to allow intervals to be regarded as equal whenever they
intersect, in order to get "completeness", then you are going to lose
soundness.  Let Y be a floating point number which happens to be precisely
equal to 1.0, let X be 2.0, and let Eps be a suitably tiny number.  It is
clear that no matter what the true value of Y really is, (X*Y)/Y should be
exactly the same as X, but in fact the interval will be wider by about
3ULPs.  So mathematically X+Eps =:= (X*Y)/Y should fail, but the two
intervals will overlap, so "equal if intersecting" would report equality
here, which would be unsound.

I would *much* rather have soundness than completeness!
> round-off errors will
> make expressions like 1.0 + scalb(1.0, -60) =:= 1.0 true in both interval
> and floating point arithmetic
No, that condition would _not_ be true in interval arithmetic.  The
left hand side would evaluate to [1.0,1.0+eps] and the right hand side
to [1.0,1.0].  The two intervals are different.