Re: Motion 31 draft text V04.4, extra notes
Vincent Lefevre wrote:
On 2012-04-11 10:33:41 -0500, Nate Hayes wrote:
Vincent Lefevre wrote:
>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.)
atan([1,+OVR]) = [atan(1),+pi/2]
pi/2 is not a Level 2 number. I assume you mean the hull of this
interval.
Yes. pi/2 is the exact result of the operation. However, any Level 2
interpretation of this exact result will need to be rounded, no differently
than, say, atan([1,+Inf])=[atan(1),roundUp(+pi/2)] at Level 2.
How do you determine pi/2?
>>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.
I don't see you've given any reason or convincing proof to this claim.
How can you consider 1 / [0,1] without unbounded intervals?
You've already agreed [1,+OVR] as a family of intervals is not the same
thing as an unbounded interval but contains all possible solutions.
>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).
I can't think of any.
If there isn't any, this would mean that your model is equivalent
to the one using unbounded intervals (basically you're using
unbounded intervals without saying it, a bit like one can manipulate
real numbers just by using sequences of rational numbers).
No. You've already agreed [1,+OVR] is not an unbounded interval, it is an
infinite family of bounded intervals.
>>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.
What does that matter?
Motion 5 is a practical consequence of the underlying set-based
definitions.
It hides the more interesting (generic) definitions (i.e. the ones
that used for other operations). Anyway since this doesn't change
anything in Motion 5, I agree that this doesn't really matter (I
wonder why you mentioned this motion in the first place).
Because Baker (and perhaps others) is worried, for example, that my point of
view just represents so much useless "churn". But I'm actually trying to
demonstrate that such a change has relatively little impact on anything,
especially from a practical point of view.
>>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].
Who cares if I can do 1/[0,1]=[1,+Inf] at Level 1 if I can't assume
A + X = B + X
means A = B!!
That is not an arithmetic I want to work with.
If you do not work with unbounded intervals, you still have
A + X = B + X ==> A = B
I don't see any problem.
Well, how am I to not work with unbounded intervals at Level 1 if the
standard requires they may be there?
I'd rather reason about at Level 1 like Ramon Moore (no division by
interval containing zero).
If you never divide by intervals containing zero (and never use
other functions like tan that can lead to unbounded intervals),
then you can just ignore anything related to unbounded intervals.
I can't ignore anything the standard mandates unless I don't follow the
standard.
Other users who may need such intervals can still use them with
P1788.
Well, I'm still waiting for you to show me why they are necessary. All I
take away from our conversation to this point is you have a very strong
personal preference and opinion for unbounded intervals in the Level 1
model. But I've not seen any proof or evidence they are *necessary*.
Nate
--
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)