Re: Motion 31 draft text V04.4, extra notes
On 2012-04-08 16:45:26 -0500, Nate Hayes wrote:
> In my mind, a similarly informal definition of an "overflown" interval is a
> Level 2 interval with +OVR at one or both endpoints. For example, at Level 2
> the interval [0,+OVR] represents the input domain
> x >= 0
> to any practical extent a computer in the real world can prove anything
> meaningful about the domain of a function within the numerical limits of the
> underlying system, even though [0,+OVR] is not truly unbounded.
What if the user wants the range of atan(1/x) over [0,1] (as an
interval of real numbers)?
How would atan([1,+OVR]) be defined? (I'm not asking for an
implementation, I'm asking for a specification.)
> For example, I see the more formal definition of the "overflown" interval
> [0,+OVR] as a family of intervals. One can think of the number of intervals
> in the family as being infinite, but each member of the family is a closed
> and bounded (compact) interval. This means unbounded intervals are not
> required at Level 1 in order for "overflown" intervals to exist at Level 2.
The user is interested in math results. Unbounded intervals exist
there and can be produced from bounded intervals. So, in any case,
unbounded intervals need to exist at Level 1 for this reason. And
at Level 2, probably too, unless you can get rid of them in a correct
theory, but I don't see how.
> As illustrated earlier, [0,+OVR] is suitable input, under this
> intepretation, for a branch-and-bound or global optimization algorithm, say.
> It is also suitable as the result for arithmetic operations. For example, in
> the current P1788 model
> 1/[0,2] = [1/2,+Inf]
> whereas in the new model
> 1/[0,2] = [1/2,+OVR].
Do you have an example where a sequence of operations will differ
when you change the model (except by replacing Inf by OVR).
> From a practical perspective: for any and all inverval arithmetic operations
> and applications, if you simply replace +Inf from the current P1788 model
> with +OVR, then the interval arithmetic formulas in Motion 5 are still
> completely accurate and unchanged.
Motion 5 is highly complex compared to the simple set-based
definitions.
> The main difference is in the formality of the underlying
> mathematical definitions about how such results are obtained. In the
> new model, all Level 1 intervals are closed and bounded (compact).
> IMO this leads to a cleaner, simpler Level 1 model with stronger
> algebraic properties than the current P1788 model; and I don't see
> in terms of actual meaning and practical functionality that anything
> is lost by removing unbounded intervals from the Level 1 model in
> this way.
I don't see why it is cleaner (you haven't provided any example).
And it is not stronger. On the contrary, it is less powerful, because
without unbounded intervals, you can't do things like 1 / [0,1].
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)