Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Re: Motion P1788/M0034.01:Notation-- discussion period begins



Michel Hack wrote:
P.S.  I also had an objection to Nate's Level 1 use of MAXREAL (which one,
     as Level 2 may well support several formats?)
We're still looking at a the details of supporting multiple formats.

-- but that discussion
     has mercifully been put to rest...
Hmm. I'd point out you and Vincent had basically argued the reason for
unbounded intervals is they supposedly make developing computer algorithms
(and proofs) at Level 1 much easier. But one doesn't need to look very hard
to see this isn't the case. Interval Newton is arguably one of the most
fundamental or important algorithms. At each step we have:
   X_2 := (m(X_1)-f(m(X_1))/F'(X_1)) \intersect X_1
where m(X_1) is the midpoint of X_1. If the user provides an unbounded
interval as input, the algorithm is undefined at Level 1 despite the fact it
may operate well at Level 2.
Nate