Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

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

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.


  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?


(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). 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?





But instead, let me point out you have agreed (several times) unbounded
intervals are unnecessary.


No, I haven't... unless you come with a model that is more powerful
(at Level 1 and Level 2) than the current one, with all the details
and the proofs. If it is just equivalent and more complex to explain,
I'm not interested.

Fair enough. I had already told you previously we weren't done with all
that.




>Level 1 will never occur in the implementation of the standard. On your
>side, you can use whatever you like for math equations.
This applies to you, as well.


??? You haven't understood. Level 1 is there to specify Level 2.
If things like OVR are specified at Level 2 only, there's something
missing.
I understood. There must be a connection between Level 1 and Level 2, no doubt. OVR still provides that connection. I will work on it some more. 
Nate