[std-interval] More on interval computations as proofs
Dr John Pryce
j.d.pryce at ntlworld.com
Wed Oct 4 20:22:06 PDT 2006
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
- 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
>> 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)
>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?
Dr John and Mrs Kate Pryce
142 Kingshill Rd
Swindon, Wiltshire SN1 4LW
More information about the Std-interval