Motion 26: V03.2 draft plus FTDIA proof

[John Pryce <j.d.pryce@xxxxxxxxxxxx>]

P1788

On behalf of myself and Arnold Neumaier, I circulate a revised v03.2 draft of the decoration system, with a proof of the Fundamental Theorem of Decorated Interval Arithmetic, in Annex D.

As with the previous circulated version:
- The basic Level 1 definitions in 5.1-5.5 are included.
- Required and recommended functions in 5.6-5.7 are omitted.
- The decoration system in 5.8 is included.

The initial subclauses of 5.8 (old 5.8.1-5.8.5 have become 5.8.1-5.8.6 I think) have been revised without changing the substance. Namely the definition of the dec(f,xx) function has been put as late as possible, just before the numerical examples where it is essential.

Chair: Since the substance is unchanged and the main change is that supporting material (FTDIA proof) has been added, I hope this does not count as an "amendment" to Motion 26 that would require re-starting the vote. I.e., let's continue the current voting period.

Voters: The crucial Motion 26 issue is that we say, far more precisely than does Motion 27, how a chunk of metal and silicon, with a finite set of states, can collaborate with humans to construct valid proofs about the infinite continuum of real numbers. When a correctly constructed program reports "This function is continuous" we can show exactly why it is telling the truth. Though the Motion 27 scheme is operationally nearly identical, its description of decorations as merely "tracking properties of the environment in which the interval has been computed" seems to me to be vague, and lack the courage of conviction.

If you vote NO, please do the group the courtesy to state *the changes that would make you vote yes*, as you would if this were a vote on the actual text. Maybe you will find a gap or error in the proof: excellent. Maybe it all looks too complicated: how would you simplify it, taking note of Einstein's dictum "Everything should be made as simple as possible, but not simpler"? 

Whichever way you vote, please note:
- How many decorations there shall be is for later discussion.
  (I would go for 6 or 5.)
- Some aspects of "bare interval arithmetic" may be open to change.
  Recall this scheme is to support very fast execution for certain
  important classes of problems.
- Arnold has flagged the decorated case(b,g,h) function as needing
  attention. Let P1788 discuss this separately from the current motion.

Regards

John Pryce

Attachment: 20110805Decs+FTDIAproof.pdf
Description: Adobe PDF document