Relationship between `cons' and average

The `cons' operation is a primitive operation on lists and streams. Operations on exact real numbers, however, are defined in terms of mathematical operations. Fortunately the semantics of the stream of digits representation of reals leads to a useful relationship between `cons' and average which simplifies later definitions.

We define average as one would expect, using the symbol $\oplus$ so that

$$a \oplus b = \frac{a+b}{2}$$

Now, suppose we wish to compute the average $(a \oplus x)$ of the digit a and the stream x. It is useful to observe that

$$a \oplus \llbracket x \rrbracket = \llbracket a :: x \rrbracket$$

because $a \oplus \llbracket x \rrbracket = \frac{a}{2} + \frac{\llbracket x \rrbracket}{2} = \frac{a}{2} + \llbracket 0::x \rrbracket = \llbracket a::x \rrbracket$. Hence the result of averaging a digit and a stream may be performed by generating a new stream using the `cons' operation to attach the digit at the head of the original stream.