Book chapter 1227 views
Logic for Gray-code computation
Ulrich Berger 
,
Kenji Miyamoto,
Helmut Schwichtenberg,
Hideki Tsuiki
,
Kenji Miyamoto,
Helmut Schwichtenberg,
Hideki Tsuiki
Start page: 69
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1515/9781501502620-005
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 infinite sequence containing at most one undefined element. In this paper we take a lo...
| ISBN: | 9781501502620 |
|---|---|
| Published: |
Mouton, Oldenburg, China
de Gruyter
2016
|
| Online Access: |
http://www.cs.swan.ac.uk/~csulrich/ftp/logic_for_gray_code.pdf |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa28978 |
| 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 infinite sequence containing at most one undefined element. 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 difculty due to the undefined element which prevents sequential access to a stream.We extract real number algorithms from proofs in an appropriate formal theory involving inductive and coinductive defi€nitions. 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 fi€nite segments of pre-Gray code into its normal form. These examples are formalized in the proof assistant Minlog. |
|---|---|
| Keywords: |
Gray-code, Real number computation, Inductive and coinductive definitions, Program extraction. |
| Start Page: |
69 |