next up previous contents
Next: Output zero case: Up: Division Previous: Division

Modification of mantissas

We first need to modify the mantissas x and y' of the numerator and denominator in such a way as to allow us to perform division on the streams. Using the naïve approach of simply using the mantissas directly this would be impossible:

\begin{displaymath}
x \in [-1,1] \ \textrm{and }y' \in [-1,1] - \{0\} \ \Rightarrow \ \frac{x}{y} \in (-\infty,\infty)\end{displaymath}

However we can use shift operations and the identities from section 3.3.1 to find an exponent $e \in \mathbb{Z}$and a numeral y' such that:

\begin{displaymath}
\llbracket y \rrbracket = \llbracket y' \rrbracket \times 2^...
 ...\textrm{ such that } \ \vert y\vert \in \Big[\frac{1}{4},1\Big]\end{displaymath}

Essentially we insist that the stream y starts with a non-zero digit, and that the first two digits are not $(1::\overline{1})$ or $(\overline{1}::1)$. Now we can say:

\begin{displaymath}
x \in [-1,1] \ \textrm{and }\vert y\vert \in \Big[ \frac{1}{4},1 \Big] \Rightarrow \frac{x}{y} \in [-4,4]\end{displaymath}

The algorithm will now compute $x/4y = (x/y') \times 2^{e-2}$. For simplicity we now assume that y always starts with the digit one. In order to compute division by a negative y, it is sufficient to negate y to make it positive, and then negate either the numerator x or the result of the whole division. Hence from now on:

\begin{displaymath}
y \in \Big[\frac{1}{4},1\Big]\end{displaymath}

We describe the algorithm and prove its correctness by examining cases. We look at all possible combinations of digits at the head of the input streams, and for each case show how we can find a dyadic digit which we can output, and express the remainder of the result as a recursive call to the division algorithm.

The algorithm is broken up into the cases which produce the digit zero as output, those which produce a positive digit, and those which produce a negative digit.


next up previous contents
Next: Output zero case: Up: Division Previous: Division
Martin Escardo
5/11/2000