Re: Neumaier-Pryce proposed decoration system (v03.2)
John Pryce wrote:
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.
If a proof is given for the wrong theory, this would be worse.
Of the two sources noted in:
http://grouper.ieee.org/groups/1788/email/msg03570.html
that caused failure of the interval algorithms, I don't see that the new
v3.02 draft addresses these issues.
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!
Yes, the bugs noted above are still present in the v3.02 draft. But they are
bugs in the theory, not the technical writing.
On a different topic:
One thing in v3.02 that puzzles me is the introduction of the decoration
"ein" as the "worst" decoration of the linear quality order (5). In my old
Nov. 14 draft paper on decorations, I had proposed this as well: that
arithmetic operations on empty input gave the worst decoration.
But this was criticized heavily by Arnold (see the "ping pong match" between
the two of us in the P1788 archives for December 2010).
So I admit it was really shocking to see this appear in v3.02.
It was in some offline discussions with the Gang of Ten a month or two later
that Dominique suggested arithmetic operations on empty input should give
the best decoration, not the worst.
After trying this in our lab and studying the behavior in various
algorithms, we found Dominique's suggestion not only addressed the
complaints raised by Arnold but also appeared to solve some other issues
involving bare decorations as well (which haven't been discussed in any
detail yet by P1788). So this is what led to Motion 25.
Just recently (on May 26) you wrote:
HOWEVER the following may help us converge.
I have been thinking about
- Dominique's and your proposal to put "X is empty" at the top of the
hierarchy (D4 in your May 20th draft).
[...]
Following discussion with Arnold we propose: do as you and Dominique say,
and put "X is empty" at the top of the hierarchy. We call this decoration
"ein" for "empty input".
But this obviously is not the case in v3.02. Is it a type-o?
Otherwise it seems in just the past few weeks you have changed your minds...
but instead of going back to v3.01 definitions, introducing "ein" as the
"worst" decoration?
Nate