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

Re: Midpoint paper (2012-02-08 version)



> > I desired such a property:
> > (*) midrad([u,v]) is finite floating-point number for finite [u,v] interval=
> > s (explicit or implicit).
> > The definition (15) may return infinite midpoint for some finite implicit i=
> > ntervals.
>
>	Alas, while this may be true in one direction for
>	some specific pair of explicit & implicit types,
>	I believe it is true that finite intervals of one
>	flavor may be required to become infinite or
>	semi-infinite in another if only to preserve
>	containment.

I had a mistake in formulation (*).
I want to say
(*) midpoint([u,v]) is finite floating-point number for any finite [u,v] interval from IR .

The midpoint([u,v]) is not mapping from one interval type to other interval type.
It's a mapping from interval type T to number format F.
I will put the name of result number format F into subscribe: midpoint_F([u,v]).
And I want that this operation considers only bounds of the argument [u,v], not its format T.

It is similar to the way how interval arithmetic operation are defined:
add_T([u1,v1],[u2,v2])=hull_T([u1+u2,v1_v2])
add_T may map any pair of intervals (T',T'') to the interval format T .
It considers only bounds of arguments, not their formats.

I would like to tell a little about my background.

<<<<<<<<<<
Our JInteral project develops a JVM (Java/Scala/Jython etc) interval library.
The bounds of our intervals are represented by values of our class ExtendedRational .

ExtendedRational = Rational + {NegativeInfinity, PositiveInfinity} .
The mathematical value of our Rational objects are rational numbers.
However, it is adaptive. It's internal representation depends on value.
There are a few internal subclasses of Rational:
* RationalImpl(n: BigInt, d: BigInt, e: Int) . Its value is (n/d) * 2^e. d > 1 .
* BinaryImpl(n: BigInt, e: Int). Its value is n * 2^e . n != 0 and (n * 2^e) is not a normal value of Binary64 .
* NormalDoubleImpl(d: Double). Its value is d . d is a normal value of Binary64 .
* Zero. Its value is 0 .
There are exact operations like add(x: Rational, y: Rational): Rational
And there are operations like add(F: BinaryFormat, rm: RoundingMode)(x: Rational, y: Rational): Rational = F.round(rm, add(x,y))
They are indexed by IEEE 754-2008 binary number format F=(precision,emax,emin) and by IEEE 754-2008 rounding direction.
Each call of these operations adaptively uses algorithm according to actual subclasses of x and y values.

The class Interval of our library has two public subclasses
* Nonempty(inf: ExtendedRational, sup: ExtendedRational) . inf <= sup, inf < PositiveInfinity, NegativeInfinity < sup .
* Empty.
There are exact operations
add(x: Interval, y: Interval): Interval = {
  (x, y) match {
    case (Nonempty(xi,xs), Nonempty(yi,ys) => Nonempty(xi + yi, xs + ys)
    case (Nomempty, Empty) => Empty
    case (Empty, Nonempty) => Empty
    case (Empty, Empty) => Empty
  }
}
And there are operations indexed by IEEE 754-2008 binary number format F .
add(F: BinaryFormat)(x: Interval, y: Interval): Interval = {
  add(x,y) match {
     case Nonempty(i,s) => Nonempty(F.roundFloor(i), F.roundCeiling(s))
     case Nonempty => Nonempty 
  }
}

There are exact number operations 
exactMid(x: Interval): Rational = {
  x case {
    case Nonempty(i,s) => (x + y)/2
    case Empty => throw new DomainException
  }
}
And there are operations
doubleMid(x: Interval): Double
floatMid(x: Interval): Float
There specification is stil uncertain for us.
>>>>>>>>>>

I know that our library could be out of scope of P1788
because its Intervals are not tagged by any interval datatype.
However, I search opportunity to be as close as possible to the coming P1788 standard.
And sometimes I try to influence the P1788 development, so that our library becomes closer to it.

>	So, in its full generality, I believe seeking (*)
>	is a forlorn hope.  I'll have to think about
>	whether or not there is less restrictive but still
>	useful form of (*) that is always true.

It's a pity that (*) can't be accepted.
I will be glad to explore your suggestions about alternative of (*).  

> > Then I read the Michel's post. It was about semi-finite interval of wider f=
> > ormat,
> > but it came to me the same may happen
> > with midpoint_F([u,v]) Level 2 operation that maps infsup intervals [u,v] o=
> > f wider IEEE-754 format Fw to
> > narrower IEEE-754 format F.
> > 
> > So the question that bothers me is:
> > What properties do we expect from width(X)/midpoint(X)/radius(X) when
> > X is of implicit interval type or X is of explicit interval type of wider n=
> > umber format ?
>
>	I presume the question is asking: if X is in format F
>	& X' = convertFromF2F'(X) is in format F', what can be
>	said about width(X)/midpoint(X)/radius(X) in relation
>	to width(X')/etc.?

No, this is not my question. My question is about properties of operation
midpoint_F(X) where F is some number format, and X belongs
to some explicit or implicit interval datatype T .
I don't compare midpoint_F and midpoint_F' operations now
and I don't convert X from T to other interval datatype T' .

>	As for the infinite & semi-infinite cases, I believe
>	that the fact that explicit & implicit types actually
>	represent quite different classes of intervals will
>	mess thing up.  As will Michel's observation about
>	different precisions.  Other than weak monotonicity
>	within a format & Nate's equation (22), I'm not sure
>	what other properties remain that might contribute
>	to some formal proof.
>
>	Is it properties needed for formal proofs you seek
>	or something else?

I would like to make specification of number functions simpler.
And then formal proofs will be easier. One way to do it is to define
them in such a way that they are indexed by number format, but they are
independent ot interval datatype of argument.

>	Nate & I are proposing width/midpoint/radius that
>	return floating-point answers in the same format
>	as the interval inputs.  (If that is not in the
>	text somewhere it should be.)

Yes. And I like how your definition works in this case.

>	One could have a format specific (like 754's
>	formatOf) form of midpoint, for example, that
>	returns a specific format no matter what the
>	format of its input.  Indeed, some ways that John
>	might write up this proposal would have them
>	lying around.

Yes. I'd like such definition of midpoint.

>	But how (beyond a single extra rounding error)
>	would such a function differ from
>	convert2F(midpoint(X'))?  All the finite &
>	semi-infinite inputs would convert with or
>	without over/underflow as a function of the
>	relative exponent ranges of the two formats WRT
>	their floating-point behavior not WRT their
>	interval behavior.  At least I think so.

I understand this in such a way. Can Level 2 definition of midpoint_F(X) be decomposed
in midpoint_F(X)=convert2F(midpoint(X)) where convert2F is F-dependent and midpoint is F-independent.
I'd say that yes.

midpoint([u,v]) = if (u == -oo && v == +oo) then 0
else if (u == -oo) then -oo
else uf (v == +oo) then +oo
else (u + v)/2

convert2F(t) = let t' = roundNear_F(t) in
  if (t' == -oo) then -Fmax
  else if (t' == +oo) then +Fmax
  else t'

>	Indeed, while the issues you raise are valid
>	& may be important in some contexts, they are
>	really issues of the incompatibility of the
>	various formats more than issues of the nature
>	of these particular functions.
>
>	In other words, how do they differ from the
>	same issues WRT add, subtract, multiply, &
>	divide?

It seems that the issues don't differ from the same issues of arithmetic interval operations.
And I suggest the approach that is similar to hull_T(x op y) approach. 

>	Let me know if you can think of some explicit
>	change to width/midpoint/radius that would
>	help with any of these concerns.

I suggested the change to midpoint_F .
I would like to explore your variants of midpoint too.

For now, I don't see any need to change width/radius.

  -Dima