next up previous contents
Next: Limits within Up: Limits within [-1,1] Previous: A recursive definition

Recursive calls to compute the limits

Suppose we have a stream of nested intervals represented as $(x_1,z_1)::(x_2,z_2):: \dots$, whose end points are represented as signed binary streams (section 3.5), and with the following property:

\begin{displaymath}[x_1, z_1]
\supseteq [x_2, z_2] \supseteq [x_3, z_3] \supseteq \dots\end{displaymath}

We also have a function f which takes three signed binary stream x, y, and z as inputs, and outputs a signed binary stream representing $\llbracket y \rrbracket$ by examining x and z, determining common digits from them if it can using the method described above, and then using y directly to determine the rest of the output.

We can now compute the signed binary stream represented by the stream of nested intervals y as the result of $\mathrm{limit}(y)$, where the function $\mathrm{limit}$ function is defined as:

\mathrm{limit}((x, z)::y) = f(x, \mathrm{limit}(y), z)\end{displaymath}

Martin Escardo