M-7 -- 6.1 Screens and Roundings

Go up to 6 Towards a Datatype REAL
Go forward to 6.2 Proposal of an Abstract Datatype REAL

6.1 Screens and Roundings

Let R^*:= R u {-infty, +infty}⁷ denote the real numbers adjoined with -infty and +infty. A subset S c R^* is a screen if

forall x e R^* exist s e S: s < x /\ forall s' e S: s' < x => s' < s and
forall x e R^* exist s e S: s > x /\ forall s' e S: s' > x => s' > s,

i.e. the set of the lower (upper) bounds of an element x e R^* in S has a greatest (least) element. For example, the following (normalized) floating point systems can be extended to screens:

S_b,l := { 0 } u { x = * m ·b^e | * e {+,-}, e e Z,

m=SUM_i=1^l x[i] b^-i,

x[i] e {0,1, ..., b-1}, x[1] =/= 0 }

and

S(b,l,e1,e2) := { x e S_b,l | e1 < e < e2 },

where

b e N, b > 1, the base,
l e N, the length of the mantissa,
e1, e2 e Z, the bounds of the exponent.

In order to have a unique representation of zero available in S(b,l,e1,e2), we assume additionally that sign(0)= +, mant(0)=0.00...0 (l zeros after the b-ary point), and exp(0)=e1. The set S_b,l is countable, while the set S(b,l,e1,e2) is finite. They both have the properties: 0,1 e S, forall x e S: -x e S, where S is either S_b,l or S(b,l,e1,e2). Adjoining the elements -infty and +infty we obtain screens on R^*:

S(b,l)^* := S(b,l) u {-infty, +infty}, and

S(b,l,e1,e2)^* := S(b,l,e1,e2) u {-infty, +infty}.

A rounding is a map r: R^* -> S to a screen S such that

forall s e S: r(s) =s.

We call it monotone if furthermore

forall x,y e R^*: x < y => r(x) < r(y).

For example the mappings

phi: {
R^* -> S

x ^_|-> |_| { s e S | s < x }

and psi: {
R^* -> S

x ^_|-> |¯| { s e S | s > x },

where |_| denotes the greatest upper and |¯| the least upper bound of a set in S, are monotone roundings.

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to till@informatik.uni-bremen.de

S_b,l := { 0 } u { x = * m ·b^e \|	* e {+,-}, e e Z,
	m=SUM_i=1^l x[i] b^-i,
	x[i] e {0,1, ..., b-1}, x[1] =/= 0 }