Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Tsuiki, Hideki
(2016):
Logic for Graycode Computation.
In: Probst, Dieter (ed.) :
Concepts of Proof in Mathematics, Philosophy, and Computer Science. Ontos Mathematical Logic, Vol. 6. Berlin: Walter De Gruyter. pp. 69110

Full text not available from 'Open Access LMU'.
Abstract
Graycode is a wellknown binary number system where neighboring values differ in one digit only. Tsuiki (2002) has introduced Gray code to the field of real number computation. He assigns to each number a unique 1 perpendicular tosequence, i.e., an infinite sequence of {1, 1, perpendicular to} containing at most one copy of perpendicular to (meaning undefinedness). In this paper we take a logical and constructive approach to study real number computation based on Graycode. Instead of Tsuiki's indeterministic multihead Type2 machine, we use preGray code, which is a representation of Graycode as a sequence of constructors, to avoid the difficulty due to perpendicular to which prevents sequential access to a stream. We extract real number algorithms from proofs in an appropriate formal theory involving inductive and coinductive definitions. Examples are algorithms transforming preGray code into signed digit code of real numbers, and conversely, the average for preGray code and a translation of finite segments of preGray code into its normal form. These examples are formalized in the proof assistant Minlog.