A Stream Calculus of Bottomed Sequences for Real Number Computation

A calculus XPCF of 1⊥-sequences, which are infinite sequences of {0,1,⊥} with at most one copy of bottom, is proposed and investigated. It has applications in real number computation in that the unit interval I is topologically embedded in the set of 1⊥-sequences and a real function on I can be written as a program which inputs and outputs 1⊥-sequences. In XPCF, one defines a function on only by specifying its behaviors for the cases that the first digit is 0 and 1. Then, its value for a sequence starting with a bottom is calculated by taking the meet of the values for the sequences obtained by filling the bottom with 0 and 1. The validity of the reduction rule of this calculus is justified by the adequacy theorem to a domain-theoretic semantics. Some example programs including addition and multiplication are shown. Expressive powers of XPCF and related languages are also investigated.