Re: Neumaier-Pryce proposed decoration system (v03.2)
Jürgen
On 10 Jun 2011, at 12:16, J. Wolff von Gudenberg wrote:
> John
> here are some comments on your position paper
> 1. The sentence
>> Note that a decoration primarily describes a property, not of the interval it is attached to, but of the function defi ned by a section of code that produced that interval.
> is very important and helpful for understanding. It should be emphasized
OK
> 2. The following sentence is also important for your position, but I dislike it:
> In the remaining case
> c' = bnd, we require instead c'' = min dec(f; y) over all bounded y \subseteq x, to match the semantics of the bnd decoration.
> - as a user of p1788, I do not understand it
> - as an implementor of p1788 I see no rules or formulas how to procede
> - as a mathematicien i miss the proof
> - as an intervaller I think, we live better without it and always propagate the min of c' and c''
I don't like it either. It wasn't in the previous version but when we split "saf" into "saf" and "bnd", Arnold reckoned it is needed to handle the "bounded" property. The ball is in Arnold's court at present while he checks the FTDIA proof and updates it to handle the new set D of decorations.
It certainly needs to be reduced to rules or formulas as you suggest.
Every time we try to handle boundedness it seems to create a mess. (Recall, in this context it means "A function f is bounded on its input box xx".) Why it does so, I'm not sure. Maybe Arnold's current work will remove the mess.
> 3. There are some typos around formula (14)
> 4.In the list (ii) d is the input shouldn't it be e
I think these points 3,4 are one point? No, I think the formula is correct. It is rather obscurely written and I'll try to say it better.
> 5-Table 5 for division is either false or I can't read it
Which entry(s) do you disagree with? Counterexample please.
> All in all I fear that p1788 will fail, if we will continue to define it by the theorem proof style.
This is an important comment. My belief is that your objections can be met by proper arrangement and signposting of the 1788 text.
More, probably, than most IEEE standards, 1788 has to satisfy disparate groups of people. Yes, implementers need rules that say clearly how to implement. This is mostly level 2 and level 3 stuff; we have some of it already, e.g. Ulrich's tables for the basic operations. For the decoration system it'll be tedious, but not especially hard, to write tables that specify the decoration delivered by each of our elementary functions in all possible cases.
But also mathematicians want to write algorithms based on P1788 primitives, and prove them correct. They need the statement of the Fundamental Theorem of Decorated Interval Arithmetic in the main text, surely. They need access to its proof to check the wool isn't being pulled over their eyes - this could be in an Annex as now, or in a different, publicly available, document. This is all level 1 stuff.
It would be useful if someone looks at the whole level 1 - especially the decoration material - aiming to extract "a minimal subset that an implementer MUST understand", which could be presented first. The rest to be signposted as optional reading for an implementer.
I can send the current complete level 1 to anyone interested. It needs some tidying before I circulate, and I prefer to wait till I have Arnold's verdict on the FTDIA and proof.
There'll probably be bugs in what we ship, but the existence of proofs should greatly increase our confidence. I read in
http://c2.com/cgi/wiki?ProofOfCorrectness
that a formal model of TcpIp discovered bugs in the protocol, even though it had been in use for years!
I'm probably being highly naive and simplistic but that how it strikes me. Please put me right.
John