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