Up Next
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 }
S(b,l,e1,e2) := { x e Sb,l | e1 < e < e2 },
where 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.
Comments to till@informatik.uni-bremen.de

Up Next