Re: KISS-decorations
Juergen, Marco and all
Thanks for the updated version
On 30 Jun 2011, at 11:42, Dominique Lohez wrote:
> BTW Your second statement of theorem 1 is again wrong
> Since f(x)=x is continuous the John's counterexample is again working.
> f(x) is a function defined by an expression in the John's wording.
> F(X) is THE extension calculated by a interval transcription of the expression.
> Then for F(X) the isotonicity holds.
(a) I was about to point out the same two things. It's what I'm calling the "natural interval extension" (Arnold asserts this is standard terminology), aka what you call "straightforward interval computation" that is isotonic.
And even that is only conditionally true.
IF the interval version of each elementary function is isotonic
THEN any function constructed from them by "straightforward interval computation" is isotonic.
But if we define the interval version of EVERY elementary function stupidly as in my counterexample (e.g. Entire if 0 not in xx, something sensible otherwise) then obviously this applies to functions defined by "straightforward interval computation" too, so isotonicity fails spectacularly.
I seem to recall discussion by elementary-function experts that isotonicity can fail "at the margins", i.e. by an ULP (unit in last place) or two, if a point elementary function e(x), used in coding its interval version, is "wobbly". E.g. if it is <1 ULP away from correct value at one FP number, and >2 ULPs away at the next FP number. So there's a nontrivial risk of isotonicity failing thanks to defects in library functions.
(b) You say "the decoration systems of motions 25-26 are too sophisticated...". I rather agree. However I think your, and Dominique's, desire to remove the "containment order" is more about presentation than substance.
Like death and taxes, the "containment" order is a fact of life. It simply expresses the fact that, because of interval widening due to dependence, the computed decoration fact may not be the sharpest one that actually holds. E.g. in your current scheme
saf may be true but you actually compute def (which is valid but weaker).
saf may be true but you actually compute enc ...
def may be true but you actually compute enc ...
ndf may be true but you actually compute enc ...
Would you prefer it if the standard says something like the following?
> The computed decoration always makes a true statement about the continuity, definedness, etc., of the function f over the box xx. However it may not be the strongest one available [give example] ... By introducing a *containment order* and the notion of the *exact decoration of f over xx *, one may express this in the form of a *FTDIA*, which says that the computed interval yy and decoration d, resulting from evaluating f(xx), _jointly_ enclose the exact range and exact decoration, respectively, of f over xx. [followed by fuller explanation]...
(* meaning bold introducing a new concept, _ meaning italic for emphasis.)
This presents the FTDIA as an optional interpretation that one may find enlightening, and the containment order as symbolically expressing an unfortunate fact of life in the same way as
(take-home pay T) < (gross pay G)
symbolically expresses another unfortunate fact.
John