On 2012-04-17 13:26:25 -0500, Nate Hayes wrote:
Vincent Lefevre wrote:
>On 2012-04-17 08:42:02 -0500, Nate Hayes wrote:
>>Vincent Lefevre wrote:
>>>Since there is no practical difference, between Inf and OVR, I don't
>>>see why you are complaining about unbounded intervals.
>>I may ask the same question of you about OVR.
>
>No, because:
> * OVR isn't defined at Level 1 (as you said).
It depends on the notion of a largest Level 2 number (REALMAX), e.g.,
[1,+OVR] := { [1,a] | a >= REALMAX }
as opposed to, say
[1,+Inf] := { x | x >=1 }
but both otherwise have a concrete Level 1 definition.
Still, I don't see why you want to consider a family of intervals
instead of unbounded intervals. Perhaps because this isn't clear
yet. You should give a full specification. For instance, I still
don't know how [0,1] + [1,+OVR] is defined (and why).
And what would be the difference between
{ [1,a] | a >= REALMAX1 }
and
{ [1,a] | a >= REALMAX2 }
in practice? Basically, what is the semantic of this family of
intervals?
> This would mean
> that Level 2 functions would get arbitrary choices that you
> need to justify in the standard
Why? What is so arbitrary about the definition of [1,+OVR] above that
would
make this statement true?
Level 2 is currently based on Level 1. Any Level 2 choice not made
from Level 1 is arbitrary (unless you have a generic set of rules
explaining why/how the choice has been made, but that should still
be related to Level 1, because this is where everything is defined
in the first place).
For instance, if you have a real function f (thus at Level 1) and
associated interval function (also denoted f), f(X) is defined at
Level 1, then one has a Level 2 requirement: the containment
f(X) ⊂ f2(X2) where X ⊂ X2 (possibly with additional accuracy
requirements); the definitions are the same, whether the intervals
are bounded or not. The question is: if you don't have a Level 1
definition, how is Level 2 defined?
>(currently the Level 2 results
> directly come from Level 1 properties: if a Level 1 result is
> X, then a Level 2 result is an interval containing X).
The interval [1,+OVR] has a Level 1 definition that depends on a Level 2
constant (REALMAX).
I personally think that making Level 1 depend on Level 2 is a bad
design. Level 2 should depend on Level 1, not the opposite.
That is the only reason it must be defined at Level 2.
> * Manipulating intervals is much easier than manipulating families
> of intervals.
In terms of practical implementation you just said at the top of the
e-mail
"there is no practical difference". So why is this statement not a
contradiction to that?
Because one needs to *prove* that there is no practical difference
(taking a few examples is not sufficient). I know what an interval
is, what "is in" and "is included in" means for intervals (there
is a full well-known theory about that). But what does a family of
intervals mean in practice? What are the corresponding theorems?
And so on...
Also, if I want to express the fact that some interval is unbounded
(because it occurs in the problem), it is much more natural to see
it as an unbounded interval (no changes in the concept) than to see
it as a family of intervals.
--
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)