Re: FTDIA revisited
John Pryce wrote:
On 2 Aug 2011, at 11:03, Nate Hayes wrote:
BTW:
I don't object to the idea of FTDIA, but I am rather convinced the
"containment order" formulation in Motion 26 is not valid. For example,
def is set of all (f,xx) pairs with nonempty xx and ein is set of all
(f,xx) pairs with empty xx. But ein is a subset of def??
I think that was an error once, but corrected some time ago, certainly in
the current version (I hope), which says
p_ein(f,xx) : xx is empty (i.e., has some empty component);
p_bnd(f,xx) : xx is a subset of Domain f, and the restriction of f
to xx is continuous and bounded;
p_dac(f,xx) : xx is a subset of Domain f, and the restriction of f
to xx is continuous;
p_def(f,xx) : xx is a subset of Domain f;
p_con(f,xx) : always true;
p_emp(f,xx) : xx is nonempty and disjoint from Domain f;
p_ill(f,xx) : xx is nonempty and Domain f is empty.
Note, in Motion 27 Definition 1, you have chosen to make the different p_d
predicates of its scheme *logically disjoint* (exclusive), while ours get
logically narrower as one goes away from con. So
your "def" is our "def and not dac"
your "con" is our "con and not def and not emp"
and so on.
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.
As you raise technicalities ... I raise a corresponding issue about Motion
27.
Theorem 3 is FALSE as regards ndf, and I'm still waiting for your revision
that will correct it.
It is not false. Jeurgen has already pointed this out several times and
clarified in the past few days. Are you reading the e-mails?
Suppose you do an evaluation as described in Motion 27, with the
4-decoration system.
- If you get the result saf, then certainly Theorem 3's
"the decoration" (which I take to mean the unique d in
{saf,def,con,ndf} such that p_d(f,xx) is true) equals saf.
- If you get def then "the decoration" can be either def or saf.
- But if you get con? Ah, there's the rub of Motion 27.
Theorem 3's "lower bound" implies "the decoration" can be
any of con, def or saf.
NO! It could be ndf, as numerous worked examples have illustrated.
No John, you continue to be wrong. By theorem 3 the result will be ndf iff
at least one operation in the DET is ndf; it will be con iff at least one
operation in the DET was somehere defined, somewhere undefined and all other
operations were better.
Theorem 3 is not the FTDIA (*) above, which you continue to confuse it to
be.
- And if you get ndf? Theorem 3 implies "the decoration" can be
any of ndf, con, def or saf.
NO! again. If you get ndf, then the result is CERTAINLY ndf.
Nate knows this perfectly well, and knows his B&B algorithm
would not work if this were not the case.
No John, you are wrong again.
As noted above by theorem 3 the result is ndf iff at least one operation in
the DET was ndf. The problem is you continue to compare apples and pears,
i.e., Motion 26 to Motion 27. Theorem 3 is not the FTDIA, and is not
comparing the computed decoration to the true decoration. The lower bound
computed is that of all operations in the DET. This is where you keep going
astray.
So, Motion 26 guys, get your act together and produce a Theorem 3 that is
both understandable and true.
It is already true. And (*) above verifies the results.
Nate