FTDIA revisited
John Pryce wrote:
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".
Yes, structural induction is a proof method, e.g..
http://en.wikipedia.org/wiki/Structural_induction
and this is tightly coupled to the implementation in code. I think this much
we agree.
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".
Yes, I understand.
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".
Yes.
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.
I agree with Jurgen, e.g., that
Given a DET f~ for an extension of f. The mechanism (1) then
calculates a decorated interval (e,d) where d<= di for all di appearing
in the DET
That gives a proof that only functions with properties described by the
decoration d have been applied
if d = saf f is everywhere defined and continuous
if d = def f is everywhere defined
etc.
This can all be done at LEvel 1 to verify a compiler, if one wishes.
However, the main purpose of IEEE 1788 is to standardize the computation of
interval expressions.
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??
Dominique once showed me a formulation that instead uses the special
comparison operator <=_DI such that for two decorated intervals:
(I1,D1) <=_DI (I2,D2) <==> I2 \subseteq I1 and D1 <=_D D2
where <=_D is the order
con <=_D def <=_D dac <=_D ein
con <=_D ndf <=_D ein
I think this is likely to be a more promising direction to try and formulate
a FTDIA.
Nate