[std-interval] More on interval computations as proofs

Wed Oct 4 20:22:06 PDT 2006

Dear all

I respond to some recent points in this discussion thread.

At 18:37 30/09/06, Guillaume Melquiond wrote:
>Le vendredi 29 septembre 2006 Ã 22:21 +0200, Gabriel Dos Reis a Ã©crit :
> > | An alternative implementation is to have a global flag like errno,
> >
> > I would not support that. Global variables pose significant problems,
> > both for users and implementers -- these days errno really is a
> > function. Specially in multi-threaded environment (C++ is seriously
> > considering concurency).
> >
> > Another alternative design could throw an exception.
>
>This would make the library a bit painful to use. Indeed, when the flag
>is set, it only means that the computations do not satisfy the
>hypotheses of "fixpoint" theorems. The computed range, however, is still
>valid and the program may have a use for it. So, if an exception is
>thrown, the only way to obtain the range will be to start the whole
>computation anew with no-exception functions.

Guillaume, I think you have summarized things nicely here, thanks.

Here is my view of the *context* for the discussion:

1. There is a physical problem that, 
mathematically, is modelled as a differential 
equation (i.e. almost any such problem) and for 
which verified answers are valuable. The 
consequences of getting them wrong could involve 
litigation (e.g. do the resonant frequencies of 
this turbine blade lie in a given region of the 
spectrum?) or conceivably the future of life (asteroids hitting us).

2. The interval algorithms to solve it rely on fixed-point theorems or similar.

This to my mind is what makes intervals a 
mind-blowing area: by just messing about with 
discrete stuff (bits), we can rigorously verify 
the pre-conditions for applying deep "continuous 
stuff" like Brouwer's Theorem, and get useful numerical facts as a result.

3. Programs that solve such problems are layered:

- At the bottom is an interval arithmetic library IA. We wish it
   to conform to the standard we are now building. It is probably written
   by C++ experts.

- Above it is a library code, say DESOLVE, for solving differential
   equations, written by an interval analysis expert, say Ned
   Nedialkov.

- Above that is a program APP written by an application expert, the
   "Engineer". Characteristic of differential equation problems is that

- DESOLVE calls a function APPFCN, also written by the Engineer, which
   defines the differential equation being solved. For an ordinary
   differential equation (ODE)
                 y' = f(t,y)
   APPFCN implements the function f. Given t,y it returns the value of y'
   to the caller, DESOLVE.

If we have done our job well, the Engineer 
regards IA and DESOLVE as Trusted Code.

Ned however must regard APPFCN as Untrusted Code 
- no fault of the Engineer, but there is no 
control over what APPFCN may produce, and DESOLVE 
must act robustly no matter what.

In particular DESOLVE must know for certain that 
when f has been evaluated over a box, it is 
defined and continuous on it, if the intention is to apply Brouwer's Theorem.

4. Hence the typical pattern of use is
- The DESOLVE manual tells the Engineer how to implement APPFCN, including
   to do so without clearing the DISCONT flag.

At run time
- Trusted Code DESOLVE clears the DISCONT flag.
- DESOLVE calls Untrusted Code APPFCN.
- On return DESOLVE inspects the flag. If it remains un-set, and APPFCN is
   written correctly, the Brouwer conditions have been rigorously verified.

5. If this is the typical pattern, I believe some 
of the difficulties raised are not as insuperable 
as they may seem, and I have misgivings about some offered solutions. E.g.
At 19:01 29/09/06, Lawrence Crowl wrote:
>Prof.Dr.J.Wolff von Gudenberg wrote:
>>We propose (together with G. Melquiond) That this flag can be
>>managed by the user himself. The elementary functions (at least
>>those with bounded domain) have to set this flag in the case when
>>the argument interval is not completely contained in the domain of
>>the function.
>>   interval<T> sqrt ( interval<T> x, bool& flag)
>>will be a proper interface... [as well as]
>>   interval<T> divide ( interval<T> x, interval<T> y, bool& flag)
>>  ...[etc.]
>
>I hope you are proposing these operations in addition to the
>corresponding operations without the flag.
>
>On 9/29/06, Sylvain Pion <Sylvain.Pion at sophia.inria.fr> wrote:
>>An alternative implementation is to have a global flag like errno,
>>which allows to check the flag without modifying all function calls.
>>What is the motivation behind your choice ?
>
>Please, no. Functions that modify global state are nightmares for
>multithreaded code. We could use thread-local storage, but that
>still means the function has a side effect, and compilers cannot
>optimize well around functions with side effects.

Wolff, I would hate to be the Engineer, who has 
successfully tested his APPFCN in floating-point 
and now has to re-write some possibly lengthy 
code putting in all these flags. We want to 
encourage people to join the interval fraternity: is this the way to do it?

Lawrence, some queries.
We want to make it user-friendly to write APPFCN 
functions a few hundreds of lines long, but in 
practice their length is a tiny fraction of the surrounding main program code.
First Q: does the fact that setting the flag is 
localized to a procedure, APPFCN, reduce your own 
misgivings? Our view in Sect 5.3 of the Pryce-Corliss paper is
>   For applications that need it, the value of the information [given
>   by the flag] should far outweigh any speed penalty. There should be
>   a way to remove [the flag], and its overhead, entirely for those
>   applications that do not require it.
Including the flag, or not, is surely best done 
by a compiler option at the file level, or a 
directive at the level of an individual function? 
However, the calling code DESOLVE must have 
access to clear and query the flag. Any problem 
with this from a compiler viewpoint?
Second, if this is done, is not the speed penalty 
also localized to the function?
Third, the IEEE 754 flags OVERFLOW, etc., are 
global in the way that is being criticized by 
yourself and others. Why is this considered 
acceptable for them, but not for other flags? 
Several people have said to me "that's because 
they are in hardware". (a) Can you explain why 
this is so? (b) If it is so, the ultimate 
solution is to include the DISCONT flag in 
hardware. In which case one should not force the 
current standard to adopt bad design on account 
of temporary hardware deficiencies.

Fourth, I entirely concur that an ideal DISCONT 
flag would be local to each thread. That applies 
equally to the IEEE flags. How is it proposed to 
achieve it for those? How is it done at present for, say, Java threads?

Regards

John
Dr John and Mrs Kate Pryce
142 Kingshill Rd
Swindon, Wiltshire SN1 4LW
UK
Tel (+44)1793-331062