Logic for real number computation

                       Helmut Schwichtenberg1

           Mathematisches Institut der Universität München
                 Theresienstr. 39 D-80333 München



Abstract. Gray code (also called reflected binary code) is widely known
in digital communication, due to its property that the Hamming distance
between adjacent Gray codes is always 1. Based on Gray code, Tsuiki has
studied an expansion of real numbers as streams of 0,1,undefined each of
which contains at most one undefined, and called it the modified Gray
expansion. We consider a representation of modified Gray expansion as
ordinary streams, called pre-Gray code. Through the realizability inter-
pretation we extract programs from proofs in a theory with inductive
and coinductive definitions; the realizers involve (higher type) recursion
and corecursion operators. As case studies we extract real number algo-
rithms in our setting of pre-Gray code. The correctness of the extracted
programs is automatically ensured by the soundness theorem. (j.w.w. Ul-
rich Berger, Kenji Miyamoto and Hideki Tsuiki)