[std-interval] More on interval computations as proofs

[Guillaume Melquiond]

Le vendredi 29 septembre 2006 à 16:58 -0700, Ron Avitzur a écrit :
> >The discussion showed that Standard functions MUST set a flag when
> >the argument interval is not completely contained in the domain of
> >the function. Otherwise (i.e without the flag) verification of the
> >result with fixed points or other assertions that need continuity is
> >not possible
> 
> For my graphics application of intervals, as well, it is also
> sometimes necessary to track both continuity of functions and
> the domain over which they are well-defined.

I'm not sure I understand. The following is what a two-flag semantic
could mean to me. The first flag would be the out-of-domain flag, with
the obvious semantic, while the second flag would be the discontinuity
flag. This second flag would be set when an out-of-domain interval would
cause a discontinuity. For example, dividing by [0,1] would set only the
first flag while dividing by [-1,1] would set both flags. Is this what
you have in mind?

> >I hope you are proposing these operations in addition to the
> >corresponding operations without the flag....
> >without two different functions, the user has no way to say either
> >"I don't care about domain errors" or "I am quite sure there is no
> >domain error here".  The result is substantial overhead in fairly
> >primitive functions.
> 
> Seconded. Requiring all usage of the library to pay for the overhead
> seems unreasonable.

Actually, there isn't much overhead, as the interval functions already
have to check the domain. The only overhead lies in passing a boolean
flag around and raising its value from time to time. As an example, the
following two functions would be reasonable implementation of the square
root with and without the discontinuity flag.

interval sqrt(interval x) {
  if (x.upper() < 0) {
    return empty();
  } else if (x.lower() < 0) {
    return interval(0, sqrt_up(x.upper()));
  } else {
    return interval(sqrt_dn(x.lower()), sqrt_up(x.upper()));
  }
}

interval sqrt(interval x, bool &edomain) {
  if (x.upper() < 0) {
    edomain = true;
    return empty();
  } else if (x.lower() < 0) {
    edomain = true;
    return interval(0, sqrt_up(x.upper()));
  } else {
    return interval(sqrt_dn(x.lower()), sqrt_up(x.upper()));
  }
}

So the only change is the addition of "edomain = true;" twice to the
usual implementation. I don't think it would be much of a burden on
implementers.

Best regards,

Guillaume