(long) A new proposal for midpoint et al...
Folks,
Both Nate & I have decided that the width/midpoint/radius
proposal needs some change.
And, Vincent's example of a mixed midrad+infsup type got
me to thinking about things like: the contents of John's
table 4; possible level 1 definitions; the properties
(& faults) of coercions to level 2; & on & on.
So I have thought about how to pin things down in a manner
that answers (or explains away) all the format problems by
defining things above them.
I have to admit that Nate is not on board with this approach
but he has graciously allowed me to write it up & show it to
you.
BTW, so long as I was in the neighborhood, I ended up pinning
things down for all the table 4 entries as well. Nate thinks
it is unwise to generalize things in this manner but I thought
it better to define all of them consistently.
So, without further ado, here it is.
------------------
A Table 4 Proposal
------------------
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 midpoint & midRad which remain undefined for Empty.
A 754 case could be made for midpoint(Empty) = NaN. But
it is my firm belief that NaN is a bad answer for (the
otherwise error free) 1788. Still, I have no good answer
for midpoint(Empty).
() 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. But the midpoint will
not return an element of the interior unless there ARE
such elements in the result type. So it has to be taken
into consideration that "interiorness" is a derived property
rather than a fundamental one. Further, I assert that this
is a problem with the coercion not a problem with the
definition of midpoint.
() None of them reference any level 2 structure except
midpoint which clamps results to finite values. It does
so by referencing Fmax_F for the result type F. It could
be cased out & have that reference removed. Still in this
case, I think the way it is written is more natural.
() 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 (except mid at Empty), & all do what we want them
to do. All very nice if we are going to support proofs.
() It is true that mid is defined pretty much as Michel
would have us do & has the effect of stripping off the
infinity every time you run into a semi-infinite interval.
But I'm beginning to be willing to live with that.
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) = +inf. 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) = +inf
is required as Empty is a subset of all sets. Any
semi-infinite on the -inf side & inf(Entire) = -inf.
Also, inf_F(X) may report -inf 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 +inf 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) = -inf.
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) = -inf is required at level 1
although sup_F(Empty) <= -Fmax_F is sufficient
for any given F. Semi-infinites on the +inf
side & sup(Entire) = +inf. Also, sup_F(X) may
report +inf if F has insufficient range to
express inf(X). All other non-emptys are finite.
----------
Level 1: mid(X) = for non-empty X only: if (X==Entire) then 0
else (inf(X) + sup(X))/2
Property: X \subset Y ==> if (inf(X)==inf(Y)) then mid(X) <= mid(Y) &
if (sup(X)==sup(Y)) then mid(X) >= mid(Y)
Coercion: mid_F(X) = min(max(round2Nearest_F(mid(X)),-Fmax_F),Fmax_F)
Property still holds so long as weak monotonicity
holds for your arithmetic. That is true for 754
& all other arithmetics extant (that I am aware of).
But it was false for some sloppy arithmetics in the
past. One must take care that the arithmetic is
carried out in a fashion that does not overflow.
This includes making sure that (-inf + +inf)/2 does
not happen as an intermediate result. But both can
be accomplished in more than one way. Property is
trivially true for semi-infinite intervals in that
all have the same midpoint which is to the correct
"side" of all finite subsets. Further, the midpoint
is an interior point so long as X HAS points in its
interior that are representable in F. Otherwise,
the midpoint might be an endpoint or even exterior
to X altogether. Note that this is a problem with
F not a problem with the definition of midpoint.
Applying the Principle of Least Astonishment, it is
my firm belief that a finite element of F should
always be returned rather than a NaN on the grounds
that "interiorness" is a derived rather than
fundamental property of midpoint & is violated only
when the user insists on it. That is, either by
trying to split an unsplitable interval or by
insisting on representing the midpoint in a
floating-point type inadequate to the task.
(Aside: this is mostly equivalent to Michel's
midpoint.) The midpoint of Entire is arbitrary.
Any finite value would do. But 0 is as good as
any other & splits Entire right down the middle.
Someday we may need to make a similar argument
concerning midpoint(Empty). Can we choose 0?
----------
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 +inf 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. John
has argued that the m>=0 should be removed which would
render mag(Empty) = -inf. A case can be made for this
but I, personally, prefer mag(Empty) = 0 on Least
Astonishment grounds. Still, I would have no great
objection to the change.
----------
Level 1: mig(X) = { greatest 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.
----------
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. John
also argues that wid(Empty) = -inf on much the
same grounds as mag(Empty) = -inf. I prefer 0
on Least Astonishment grounds but would have no
great objection to the change.
----------
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. 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 & (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. For the moment, we cannot have
rad(X) > wid(X) but if John's arguments about Empty
hold sway we will have rad(Empty)=0 > wid(Empty)=-inf.
Perhaps an argument against it. Perhaps not. Note
that we cannot have rad(Empty)=-inf & still preserve
containment on conversion to mid-rad. That is, IF we
can settle on an answer for mid(Empty). :-)
----------
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. 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)]. But maybe both
this & midRad belong elsewhere than table 4.
----------
Well, I've shot my bolt.
Is it any where near the target?
Dan