×

Logic for Gray-code computation. (English) Zbl 1433.03120

Probst, Dieter (ed.) et al., Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9–13, 2013. Ontos Mathematical Logic 6. Berlin: De Gruyter. 69-110 (2016).
Summary: Gray-code is a well-known binary number system where neighboring values differ in one digit only. H. Tsuiki [Theor. Comput. Sci. 284, No. 2, 467–485 (2002; Zbl 1042.68071)] has introduced Gray code to the field of real number computation. He assigns to each number a unique 1 \(\bot\)-sequence, i.e., an infinite sequence of \(\{-1,1,\bot\}\) containing at most one copy of \(\bot\) (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 \(\bot\) 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.
For the entire collection see [Zbl 1345.03009].

MSC:

03D78 Computation over the reals, computable analysis
03F60 Constructive and recursive analysis
03B70 Logic in computer science
03B35 Mechanization of proofs and logical operations

Citations:

Zbl 1042.68071
PDFBibTeX XMLCite
Full Text: DOI Link