Re: Reasons (not) to vote Motion 27: NO
Nate
On 1 Aug 2011, at 17:43, Nate Hayes wrote:
> John Pryce wrote:
>> That's what the FTDIA is! Merely a justification that the method (decorations in this case) gives valid results.
>
> John, be careful. Your theorem in its present form has contradictions, so it can't be valid. The contradictions were pointed out by Vincent Lefevre, and you aknowledged them. But neither you nor Arnold ever addressed this.
Vincent, please remind me what those were. Finding the source of contradictions is one function of a proof. The shorter the proof the easier to find any contradictions. Either the proof has wrong steps (which, because of its increased simplicity, I now doubt) or the hypotheses of the theorem are in dispute (much more likely).
> Also, you have no coherent theory for intersection and union. Saying there should be no standard for these operations is less than a mathematical punt: it is simply not acceptable.
I do indeed have a coherent theory, clearly stated. It is that no coherent theory exists. More precisely:
On 1 Jul 2011, at 06:07, John Pryce wrote:
> My rationale is that ALL the various examples so far shown build to the conclusion that union/intersection are not free-standing operations in the way that, say, an interval extension of a point function is. Their decoration logic is too contingent on the environment in which they are used, to be fixed in this standard. If we do fix it, these operations will become illustrations of the proverb "If all you have is a hammer, everything looks like a nail".
Please write, and put in your library, a decorated version of intersection that fits your applications. Offer its API for general use. Let others do the same. Just ensure they all have different names. Those that are seen to be useful in several contexts will become popular. At some future date when 1788 is revised, the popular ones can become part of the standard.
Finally
> The propagation of decorations from the leafs of the DET to the root is a proof by structural induction.
NO! It is a mechanism. You are confusing two concepts of "proof". I suspect you have been doing so for a long time.
Each correctly formed piece of decorated interval code, applied to an instance of data, instantiates a proof that a specific function has certain properties over a specific box. E.g., f(x) = sqrt(1-x) applied to xx=[0.36,0.99], using decorated library functions (and exact arithmetic!), gives a sequence of computations summarised by
sqrt( [1,1]_saf - [0.36,0.99]_saf ) = sqrt( [0.01,0.64]_saf ) = [0.1,0.8]_saf (*)
thus instantiating a "proof" that sqrt(1-x) is defined and continuous on this box xx, and its range over xx is contained in [0.1,0.8]. But that "proof" only is a bona-fide proof IF THE MECHANISM IS VALID.
An FTDIA, or any similar theorem of that kind, is a proof that the mechanism is valid: that the mechanism always spews out correct instances of proofs. You could regard it as a "meta-proof".
It's much the same as a compiler. Indeed, a debugging compiler could be taught to print out stuff like (*) to help humans check what it is doing. But if there is a bug in the compiler, then the "proof"-instance described by (*) may not be a proof at all, no matter how much you argue that "it is structural induction".
To summarise: a compiler generates code. But is it correct code? Bluntly put, you only seem interested in running the code, whereas I am interested in validating the compiler.
John