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}7 denote the real numbers adjoined with -infty and +infty. A subset S c R* is a screen if

1. forall x e R* exist s e S: s < x /\ forall s' e S: s' < x => s' < s and
2. 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:
 Sb,l := { 0 } u { x = * m ·be | * e {+,-}, e e Z, m=SUMi=1l x[i] b-i, x[i] e {0,1, ..., b-1}, x[1] =/= 0 }
and
S(b,l,e1,e2) := { x e Sb,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 Sb,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 Sb,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.