Re: Unbounded intervals
Vincent Lefevre wrote:
On 2012-04-25 09:05:19 -0500, Nate Hayes wrote:
A few points:
-- No computer (that I'm aware of) can numerically prove hardly
anything
useful about the domain of a function beyond the underlying numeric
limits
of the system; so for this reason alone, truly unbounded intervals are
never
necessary in numeric models or computations (you have never answered my
original question from long ago to show a counter-example of this).
I disagree. If the user asks for the range of 1/[0,1], the math result
is [1,+inf]. This is useful information, at least much more than an
error.
You've avoided the question again. The question is, what is an example of an
interval algorithm, for example, that proves all the zeros of a function on
the domain [MAXREAL,+Inf].
-- An overflown interval [1,+OVR] := { [1,a] | a >= H_f }, where H_f
is
As an unknown bounded interval with an arbitrary bound, the result
for 1/[0,1] would be incorrect, because the computed result must
contain the mathematical result.
I already corrected you on this in my 4/11/2012 e-mail:
Nate Hayes wrote:
In my recent e-mails I've said that the interval [1,+OVR] should be
considered as a family of intervals: the number of elements in the family
is
inifinite, but each element is closed and bounded.
Vincent Lefevre wrote (cont.):
You may build a theory where the computed result as a *family* of
intervals, but then you should stop calling that an interval. This
is obviously more complex (as a specification) than unbounded
intervals and I don't see what it would bring.
During the course of this discussion, it appears your position changed from
unbounded intervals are "essential" to "they make algorithms more easy to
define at Level 1." But my observations are that both these statements are
not true.
Overflow brings to the table an alternative to consider that, to the extent
we've studied this so far here at Sunfish, closes what we see are some
inconsistencies in the current 1788 model. For example, the midpoint
Interval Newton cannot be defined as an algorithm at Level 1 with unbounded
intervals.
a parameterization of any would-be Level 2 format, is functionally
equivalent to an unbounded interval but retains a notion of the "largest
representable number";
I don't see how this notion of the "largest representable number" is
retained.
If [1,+OVR] := { [1,a] | a >= H_f }, then the smallest element of the family
is [1,H_f], which at Level 2 is equivalent to [1,REALMAX].
for this reason it is possible to define
midpoint([1,+OVR]) at Level 1 in the same way P1788 is currently
considering to do so at Level 2.
How would you define it at Level 1, as a *real number*?
At Level 2 P1788 has considered to define midpoint([1,+Inf]) = (1+REALMAX)/2
or something similar. At Level 1, midpoint([1,OVR]) could for the same
reasons be similarly be defined (1+H_f)/2.
-- Replacing "midpoint" with "any member of the interval" gives a
valid
mathematical definition of the Interval Newton, but such a definition is
also then no longer an algorithm because the exact method of choosing
"any
member of the interval" is left undefined.
Well, once the one who writes the algorithm choose the member in
question, he has an algorithm. This member can potentially be a
parameter, and it will still be an algorithm. I don't see any problem
with that!
The problem is one cannot choose midpoint as this parameter at Level 1
without causing the Interval Newton to be undefined when unbounded interval
is provided as input.
You are the one who said unbounded intervals are important to ensure
algorithms are easy to define at Level 1. But this is clearly not always the
case.
Nate