Nate, P1788
On 5 Aug 2011, at 10:02, Nate Hayes wrote:
Note, in Motion 27 Definition 1, you have chosen to make the different
p_d
predicates of its scheme *logically disjoint* ...
Precisely. This is exactly where Dominique gets the order <=_D that I
mentioned earlier:
con <=_D def <=_D dac <=_D ein
con <=_D ndf <=_D ein
If (I1,D1) is the true decorated range of some function f and (I2,D2) is
the
decorated interval computed by Motion 27, then:
(I1,D1) <=_DI (I2,D2) <==> I2 \subseteq I1 and D1 <=_D D2 (*)
This is the FTDIA that verifies the results computed by motion 27.
Dominique
has shown me a proof for this, as well.
Maybe I am an unobservant idiot, but I really hadn't seen before that you
regard this as part of Motion 27, especially as the latter says clearly on
p8 "We do NOT need a version of the FTIA concerning decorations".
And maybe I'm overcome by enthusiasm, but it seems to me (*) is wonderful!
At a stroke the debate has transmuted (for me at least) from
a dispute between supporters of solidly grounded algorithms on one side,
and supporters of unsubstantiated ones on the other
to
a rational design choice between two or more reasonable alternatives.
... (Nate wrote)
NO! It could be ndf, as numerous worked examples have illustrated.
No John, you continue to be wrong... Theorem 3 is not the FTDIA (*)
above, which you continue to confuse it to be.
Yes, I was wrong. I took "the decoration" in Theorem 3 to mean "the true
decoration of the function over the box", which I now accept is not the
intended meaning, because that seemed the only place in Motion 27's text
that could possibly be stating a crucial relation between "computed" and
"true" values.
Dominique's order is surely related to Motion 26's containment order,
though not identical. I have no reason to doubt her theorem is true, and
hope she will circulate a proof shortly.
Best wishes
John Pryce
<silly analogy>
In the UK we have a group of eccentrics called trainspotters, one of whose
pastimes is to spend all day by a railway line with a notebook, and record
the serial number of every locomotive that goes past. (Maybe the aim is to
see every locomotive on the network by the time they die?)
If a trainspotter uses this algorithm each time a locomotive goes past:
if (number of just seen locomotive) < (number in my book) {
erase number in book and replace by number just seen
}
then at the end of the day he can be sure the number in the book records
the lowest serial number of any locomotive seen that day. And maybe boast
about this to other trainspotters, but does it MEAN anything?
I was thinking the proponents of Motion 27 are merely trainspotters. But
now you state (*), that is changed. The trainspotter is an undercover cop,
who goes home saying "now I have the evidence to crack this case".
</silly analogy>