Table 4 proposal version 0.4, less midpoint...
Folks,
Now that 32.01 has failed, it is time to propose the
remainder of table 4. I have taken as much of the
current discussion into account but some of you will
find that in error.
In any event, please comment on as much as you wish
BEFORE I go to the notion of making a motion about it.
Dan
------------------
A Table 4 Proposal
Version 0.4
(Less midpoint)
------------------
OK, I'd like to define the table 4 functions at level 1.
Then list some properties that live there. Then define
the level 1 to level 2 mapping in each case as is useful
for that case. Then show that the properties still hold
at level 2. All the properties are flavors of some weak
monotonicity property appropriate to each function.
That's pretty much all of it. But some things fall out
of this approach.
() All of them are defined for all X (including Empty)
except midRad which remain undefined for Empty because
midpoint is as yet undefined.
() Both the generic (result floating-point type the same
as that which underlies the operand) & formatOf functions
are explicitly defined. The properties still hold no
matter what the result format.
() None of them reference any level 2 structure at all.
() Unless I made a mistake somewhere (please check), all
the monotonicity properties still hold on coercion from
level 1 to level 2 (so long as our arithmetic does also &
we are careful how we coerce them there), all are defined
everywhere, & all do what we want them to do. All very
nice if we are going to support proofs.
Let me go through the level 1 definitions; the level 1
properties; the coercions; & the level 2 properties for
each function in table 4.
----------
Level 1: inf(X) = { greatest i such that i <= x for all x in X }
Note that inf(Empty) = +infinity. This is important.
Property: X \subset Y ==> inf(X) >= inf(Y)
Coercion: inf_F(X) = roundDown_F(inf(X))
That the level 1 property still holds follows from weak
monotonicity on the mapping of the Reals to the elements of F.
That we have inf(Empty) = +infinity is required as Empty is a
subset of all sets. Any semi-infinite on the -infinity side &
inf(Entire) = -infinity. Also, inf_F(X) may report -infinity
if F has insufficient dynamic range to express an otherwise
finite inf(X). All other non-empty sets have finite inf's.
So in any given F it would be sufficient if inf_F(Empty) >=
Fmax_F. But +infinity is the only correct level 1 answer.
----------
Level 1: sup(X) = { least s such that s >= x for all x in X }
Thus, sup(Empty) = -infinity.
Property: X \subset Y ==> sup(X) <= sup(Y)
Coercion: sup_F(X) = roundUp_F(sup(X))
Property still holds due to weak monotonicity. And sup(Empty)
= -infinity is required at level 1 although sup_F(Empty) <= -Fmax_F
is sufficient for any given F. Semi-infinites on the +infinity
side & sup(Entire) = +infinity. Also, sup_F(X) may report
+infinity if F has insufficient range to express inf(X). All
other non-emptys are finite.
----------
Note: mag takes arguments in IRbar & returns results in Rbar+.
Level 1: mag(X) = { least m>=0 such that m >= |x| for all x in X }
Property: X \subset Y ==> mag(X) <= mag(Y)
Coercion: mag_F(X) = roundUp_F(mag(X))
Property still holds although intervals of sufficient finite
magnitude may have +infinity reported if F has insufficient
dynamic range to express that magnitude. Other than Empty, [0,0]
is the only interval with a 0 magnitude. All others are strictly
positive. Both John & Vincent have argued that the m>=0 should
be removed which would render mag(Empty) = -infinity. A case can
be made for this but I, personally, prefer mag(Empty) = 0 on Least
Astonishment grounds. It was Vincent who provided me with the
level 1 definition that accomplishes this goal.
----------
Note: mig takes arguments in IRbar & returns results in R+.
Level 1: mig(X) = { greatest Real m such that m <= |x| for all x in X }
Property: X \subset Y ==> mig(X) >= mig(Y)
Coercion: mig_F(X) = roundDown_F(mig(X))
Property still holds although intervals of sufficiently small
mignitude may have 0 reported if F has insufficient dynamic
range to express such a small number (all others are finite &
positive). The property still holds & this is generally not
a problem as it is a fault of F rather than the definition of
mignitude.
----------
Note: wid takes arguments in IRbar & returns results in Rbar+.
Level 1: wid(X) = if (X==Empty) then 0
else if (X==Entire) then +inf
else sup(X) - inf(X)
Property: X \subset Y ==> wid(X) <= wid(Y)
Coercion: wid_F(X) = roundUp_F(wid(X))
Property still holds if weak monotonicity holds in your
arithmetic. Sufficiently wide finite intervals may have an
infinite width returned if F has insufficient dynamic range
to express that width. And care should be taken that the
expressions +/-inf - +/-inf either never arise or are dealt
with properly (easy to do). The "else if" clause is only
needed for systems that choke on +inf - -inf & return a NaN
(there are still such systems around). After that, there is
guaranteed to be one finite term in the "else" clause. At
least at level 1. Both John & Vincent argue that wid(Empty)
= -infinity on much the same grounds as mag(Empty) = -infinity.
I prefer 0 on Least Astonishment grounds but would have no
great objection to the change. Vincent provided me with the
definition that accomplishes that.
----------
Note: rad takes arguments in IRbar & returns results in Rbar+.
Level 1: rad(X) = if (X==Empty) then 0
else mag(X - mid(X))
Property: X \subset Y ==> rad(X) <= rad(Y)
Coercion: rad_F(X) = if (X==Empty) then 0
else mag_F(X - mid_F(X))
This one is a bit tricky. Partially due to its use of mid &
partially otherwise. Note that the coercion is subtly different
from all the others & is needed for both weak monotonicity &
(22) to hold. Given that, property still holds if (1) mid_F
returns the nearest representable finite number in F rather
than a NaN whether or not it is in the interior of X & (2) weak
monononicity holds in your arithmetic. Some finite intervals
will return an infinite result if F is unable to represent the
finite value. Care should be taken that +/-inf - +/-inf either
never arises or is dealt with properly (easy to do). Further,
Nate's (22)
X \subset [mid_F(X) - rad_F(X), mid_F(X) + rad_F(X)]
holds so long as not both mid_F(X) & rad_F(X) are infinite.
It would also hold for Empty if mid(Empty) is not a NaN. But
chances are, that's too much to ask for. Equation (22) is
going to be needed if we want to use X -> <mid_F(X),rad_F(X)>
to preserve containment on conversion to mid-rad. We already
have X -> [inf_F(X),sup_F(X)] for inf-sups. We will need both.
Note that we can have rad_F(X) > wid_F(X)/2 in some cases.
Indeed, we can have rad_F(X) = wid_F(X). I could make a good
mathematical argument for why this is so but only another
mathematician would fall for it.
In the end, it is because wid() & rad() are defined very
differently. With this definition (courtesy of Vincent), we
cannot have rad(X) > wid(X). Vincent also notes that the width
of an interval is unaffected by translation. Thus, an infinite
interval is still infinite no matter how you shift it (at least
at level 1). The real problem would come from the subtraction
of infinities at level 2. And this is avoided by clamping all
midpoints to finite values.
----------
Level 1: midRad(X) = for non-empty X only: <mid(X),rad(X)>
Property: mid property holds for mid part & rad for rad.
Coercion: midRad_F(X) = <mid_F(X),rad_F(X)>
This is a derived function, really. And dependent on mid() as
well. So its behavior is derived from its components. Kind of
by definition of midRad, we have that its version of (22) namely
X \subset midRad_F(X)
holds so long as not both mid_F(X) & rad_F(X) are infinite &
mid(X) not NaN. BTW, this suggests to me that we might define
an infSup(X) which returns [inf(X),sup(X)]. And maybe both this
& midRad belong elsewhere than table 4.
----------
My 5th bolt.
May it be my last.
Dan