Re: Motion 42 (not 41): Decoration system, revised text
Jürgen
On 21 Dec 2012, at 19:26, Jürgen Wolff von Gudenberg wrote:
> some questions
> 1. newDec() makes it impossible to combine bare intervals with arbitrary decorations it even deletes them. let x = ([1,2],def) then newDec(x) ---> x = ([1,2],dac)
Yes. that is intended. To combine intervals with arbitrary decorations is a different task. Michel called it setDec(xx,dx), or it could be a 2-argument version of newDec, i.e. newDec(xx,dx). At present I'm using the name setDec.
> 2. (29) delivers the decoration def if x is unbounded, why not dac
Typo, thanks.
> 3. There is a statement in 8.8.2 that decorations tell info about the real function (level 1). I share this idea and I think that e,g, the loose common evaluation (2) shows how level 2 constraints like overflow can be treated. (Here I mean that y'= oo in formula (2) does not contradict that the function is bounded.) is that correct ?
This isn't difficult but needs care and I have got it wrong in the past...
You are evaluating an arithmetic expression at Level 2 in decorated interval mode, having correctly initialised the input intervals. If the output is decorated com, then *all* the intervals that occurred -- input, intermediate and output -- were bounded, so overflow didn't happen.
But suppose hypotheses:
H0. the implementation provides "com";
H1. the input intervals were common, hence nonempty and bounded;
H2. the output is decorated dac.
Then you know that every intermediate operation was defined and continuous on its inputs, so the whole function must be. Hence conclusions:
C1. the true range must be bounded (by compactness);
C2. but overflow must have happened at some point, else
the final output would be com.
The computed output may or may not be unbounded.
If you have H1, H2 but not H0, you can still deduce C1, but without H0 you have no way to deduce C2.
Examples using an inf-sup type:
(a) f(x) = 2*x evaluated on xx=[0,realmax].
xx is common, so initialised to [0,realmax]_com.
f(xx) = 2*[0,realmax]_com (actually [2,2]_com * [0,realmax]_com)
= [0,oo]_dac
By above, this tells us the true range is bounded.
(b) g(x) = sin(2*x) with same xx. This gives
g(xx) = [-1,1]_dac.
Bounded. But we don't get com on the output, so we know overflow happened at some stage.
(c) h(x) = 1/exp(x) evaluated on yy = [-1000,1000],
assuming exp(-1000) underflows and exp(1000) overflows.
exp([-1000,1000]_com) = [0,oo]_dac
h(yy) = 1/[0,oo]_dac = [0,oo]_trv.
This is spoiled by the underflow of course, and resulting zerodivide. If we had Rump's interval system, I think we could obtain [0,oo]_dac and deduce h is bounded on yy. But that's another story.
John Pryce