unbounded intervals and Level 1 vs Level 2 vs Level 3
On 2010-05-03 07:00:20 +0100, John Pryce wrote:
> The ones that involve < rather than <= are more doubtful:
> > aa interior bb <==> b1 < a1 && a2 < b2
> This is more subtle because "interior" is a topology concept,
> using the "natural order topology" on any linearly ordered set.
> The level 3 definition differs from the topological one, for
> infinite endpoints. E.g. (Entire interior Entire) is true
> topologically but not with the level 3 definition.
> Query: Which do practitioners want or is the behaviour at infinite
> endpoints immaterial?
>
> > aa strictLess bb <==> a1 < b1 && a2 < b2
> I shall use the analogue of "lessEqual":
> for all b in bb, there exists a in aa such that a < b
> and
> for all a in aa, there exists b in bb such that a < b.
> This agrees with the level 3 definition for bounded intervals, I
> think. But not for unbounded ones, e.g.
> ([-oo,0] strictLess [-oo,1]), and (Entire strictLess Entire)
> are true in my definition but not in the level 3 one.
> Comments please.
The reason is that -oo and +oo are not really bounds, in the sense
they are not numbers that are part of the interval. I think that
definitions based on set theory are better, since closer to the
mathematical point of view (rather than the implementation point
of view).
For instance, one may want the following property at Level 1:
If X and Y are sets such that X lessEqual Y and z is a positive
real number, then X strictLess Y + z.
Note: Y + z is defined as { y + z | y in Y }.
So, for X = Y = [-oo,0] and z = 1, one would have:
[-oo,0] strictLess [-oo,1].
However X strictLess Y wouldn't imply X != Y, due to Entire. But
I don't think this is really important.
And strictLess at Level 1 doesn't imply strictLess at Level 2, but
this is independent from the infinity. And the implication becomes
true when the precision is large enough.
--
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 / Arénaire project (LIP, ENS-Lyon)