Next: The `p' function
Up: Auxiliary operations
Previous: Multiplication of a stream
It is possible to define two simple functions to add or subtract the number one from the number represented by a from a stream of signed binary digits (provided the stream represents a number in a suitable interval). Let us define these functions as follows:
These functions may be implemented as follows:
Figure 3.1:
The range of streams starting with different digits
|
= |
f(0::x') |
= |
f(1::x') |
= |
g(0::x') |
= |
g(1::x') |
= |
The proof of correctness for such definitions is as follows. Let us
consider the function f applied to a numeral x. The proof for the
function g is similar. We use to denote the number
represented by the numeral x. We examine the three cases in turn:
- Input x starts with the digit 1:
- If the input x starts with a one we know that . Hence we can output an infinite stream of ones () by the function definition.
- Input x starts with the digit :
- If the input is x is of the form (0::x'), we know that x represents the value . Now, using the properties described in section 3.6.2:
- Input x starts with the digit :
- If the input x is of the form , we can simply add the number one at the first digit and return (1::x'):
Next: The `p' function
Up: Auxiliary operations
Previous: Multiplication of a stream
Martin Escardo
5/11/2000