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

Re: Motion P1788/M0032.01:MidpointMeaning -- discussion period begins



> AFAIK, "based on a some floating-point system F" has not been defined
> for implicit interval types (see the discussion about associated /
> compatible number formats). IMHO, we could just require that each
> non-empty interval of T must contain an element of F.
>
> > 		mid_F(X) = if ((inf(X) == -inf) && (sup(X) == +inf)) then 0
> > 			   else if (round2Nearest_F(mid(X)) == +inf)
> > 				then nextDown_F(+inf)
> > 			   else if (round2Nearest_F(mid(X)) == -inf)
> > 				then nextUp_F(-inf)
> > 			   else round2Nearest_F(mid(X))
>
> So, as a consequence, inf_F(X) <= mid_F(X) <= sup_F(X). This is
> important, because this will be assumed below.

Requirement "each non-empty interval of T must contain an element of F" is not necessary.
The failure of then cna invalidate property inf(X) <= mid_F(X) <= sup(X).
Nevertheless, property inf_F(X) <= mid_F(X) <= sup_F(X) is valid independently of the requirement.