Re: Motion 31 draft text V04.4, extra notes

[Vincent Lefevre <vincent@xxxxxxxxxx>]

On 2012-04-11 18:53:04 -0500, Nate Hayes wrote:
> Vincent Lefevre wrote:
> >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.

Do you mean that 1 / [0,1] returns [1,+OVR] based on this fact?
In such a case, [1,+OVR] is equivalent to an unbounded interval.

> >>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.

And I would add the the above does not work with families of intervals
such as [1,+OVR]. So, you are not solving anything by replacing
unbounded intervals by families of intervals.

> Well, how am I to not work with unbounded intervals at Level 1 if the
> standard requires they may be there?

Since your system works only with bounded intervals, you must have
some hypotheses that guaranty that unbounded intervals will never
occur (e.g. if you consider 1 / X, you need to know that X doesn't
contain 0). So, you can just ignore unbounded intervals globally.

> I can't ignore anything the standard mandates unless I don't follow the
> standard.

The standard mandates that unbounded intervals are supported by the
implementation, not that they will occur in the user application.

-- 
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)