Re: Neumaier-Pryce proposed decoration system (v03.2)
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 dened by a section of code that produced that interval.
is very important and helpful for understanding. It should be emphazied
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''
3. There are some typos around formula (14)
4.In the list (ii) d is the input shouldn't it be e
5-Table 5 for division is either false or I can't read it
All in all I fear that p1788 will fail, if we will continue to define it
by the theorem proof style.
Like 754 we should define our datatype : Decorated Floating point
interval and its operations given by detailed tables or rules. Then we
can and we should present our assertions and proofs.
Marco and me will provide some material very soon
Jürgen
P.S:
John
I do like decorated intervals and appreciate your work very much, but
I am afraid that it will lead into the wrong direction.
Am 09.06.2011 11:03, schrieb John Pryce:
P1788
Herewith, as a position paper, is the current version of the Neumaier-Pryce proposed decoration system, §4.8 of the current draft standard text v03.2.
It is part of §4, the Level 1 specification. Subclauses 4.1-4.7, on intervals, functions, expressions, required and recommended operations (elementary functions) have been extensively revised also; but Arnold and I wished to get the decoration part out for discussion alongside Nate's current position paper.
I think we and Nate have converged in many respects, though there are still differences. Points to note:
(1) We've added 2 decoration values ein and bnd.
- "ein" means "empty input box xx" as suggested by Dominique.
- Also the old "saf" is renamed "bnd" = "defined, continuous and bounded on xx" while "saf" just means "defined and continuous on xx".
This change is recent, and Arnold has taken on the task of verifying and revising the correctness proof for this new scheme.
(2) I have omitted a few parts of the decoration system, notably decorated intersection and union on which Arnold and I do not currently agree.
(3) I have included 4.8.6. "Bare object arithmetic with a threshold" which is an important concept originated by Nate. I haven't yet updated it to handle the new scheme with ein and bnd added.
Baker, would it be possible to have a discussion of Nate's and our papers alongside? What about voting on both simultaneously?
John
--
- Prof. Dr. Juergen Wolff von Gudenberg
o Lehrstuhl fuer Informatik II
/ \ Universitaet Wuerzburg, Am Hubland, D-97074 Wuerzburg
InfoII o Tel.: +49 931 / 31 86602 Fax ../31 86603
/ \ Uni E-Mail:wolff@xxxxxxxxxxxxxxxxxxxxxxxxxxx
o o Wuerzburg