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

Unbounded intervals



Vincent Lefevre wrote:
On 2012-04-23 08:43:50 -0500, Nate Hayes wrote:
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.

Well, this example is a bit special as it also uses a numeric function
(f(m(X_1))). But if I understand the problem correctly (I'm not a
specialist of the interval Newton algorithm), I disagree with you:
the problem is not the unbounded intervals, but the fact that the
algorithm is not well stated. Indeed I suspect that you say it is
undefined at Level 1 only because the midpoint is undefined on
unbounded intervals. But if you replace "midpoint" by "any member of
the interval" (or perhaps something more restrictive), I think it is
well-defined at Level 1. Similarly, it is well-defined at Level 2 on
an unbounded input only if some arbitrary value is chosen for the
midpoint on such an interval.

We are looking at a model that defines overflow at Level 1 as an abstract
parameterization of Level 2, not unlike how Bertrand Meyer uses Abstract
Data Types (ADT) to specify the functional definition of a class implemented
in any arbitrary programming language. This parameterization only depends on
the notion of a "largest representable number" for each would-be Level 2
format. Such a Level 1 model can allow even midpoint to be specified at
Level 1, so the algorithm given exactly as above in that case would be well
stated.

I'll present a paper with details at some point... we are still working on
this right now.

Nate