Consider an abstract value whose type we call <b>DS</b> (Division State).
I want to draw a clear line between the internal logic of a DS and the external logic.
<p>There are two functions with access to the α and δ of a DS:<ul>
<li><b>cDS</b> takes two positive reals and returns a DS.
It also has access to the factory parameter ε.
<li><b>qb</b> (quotient bits) which takes a positive real d and a DS and returns a DS and a non-negative integer.</ul>
There is a function μ from DS to a positive real.
The axioms:<ul>
<li>For any positive real x and DS d, qb(x, d) = d', y (for some d' and y) and μ(d')*x + y = μ(d).
(In practice x will be a power of 2 greater than 1.)
<li>For positive reals x and y, μ(cDS(x, y)) = x/y.
</ul>
Note that these axioms do not refer to the internal values of the DS.
If 0 ≤ x &lt; 1 and ½ ≤ y &lt; 1 and d = cDS(x, y) then the bits b[j] of the binary fraction of x/y can be had thus:
<br>d[0] = cDS(x, y)
<br>for j > 0, d[j], b[j-1] = qb(2, d[j-1])
<br> whereupon x/y = Σ[j>0] b[j]*2<sup>−j</sup>.
N.B. that b[j] will be a non-negative integer (add to axioms) but it may be larger than 1.
<hr>
Internally a DS is composed of α and δ which are both positive reals.
α &lt; 1 and δ ≤ ε where ε is a positive real, fixed at the factory, probably less than ¼.
<ul>
<li>qb(d, n) = (let m = (d.α ÷ n) in