**
**

**Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut and Tsuiki, Hideki (2016): Logic for Gray-code Computation. In: Probst, Dieter (ed.) : Concepts of Proof in Mathematics, Philosophy, and Computer Science.**

*Ontos Mathematical Logic*, Vol. 6. Berlin: Walter De Gruyter. pp. 69-110**Full text not available from 'Open Access LMU'.**

## Abstract

Gray-code is a well-known 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 to-sequence, 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 Gray-code. Instead of Tsuiki's indeterministic multihead Type-2 machine, we use pre-Gray code, which is a representation of Gray-code 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 pre-Gray code into signed digit code of real numbers, and conversely, the average for pre-Gray code and a translation of finite segments of pre-Gray code into its normal form. These examples are formalized in the proof assistant Minlog.

Item Type: | Book Section |
---|---|

Faculties: | Mathematics, Computer Science and Statistics > Mathematics |

Subjects: | 500 Science > 510 Mathematics |

ISBN: | 9781501502620 |

Place of Publication: | Berlin |

Language: | English |

Item ID: | 47308 |

Date Deposited: | 27. Apr 2018, 08:12 |

Last Modified: | 04. Nov 2020, 13:24 |