Journal article 214 views 48 downloads
Computing with Infinite Objects: the Gray Code Case
Dieter Spreen,
Ulrich Berger 
Logical Methods in Computer Science, Volume: 19, Issue: 3
Swansea University Author:
Ulrich Berger
-
PDF | Version of Record
Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.
Download (723.66KB)
Abstract
Infinite Gray code has been introduced by Tsuiki as a redundancy-free representation of the reals. In applications the signed digit representation is mostly used which has maximal redundancy. Tsuiki presented a functional program converting signed digit code into infinite Gray code. Moreover, he sho...
| Published in: | Logical Methods in Computer Science |
|---|---|
| ISSN: | 1860-5974 |
| Published: |
2023
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa65589 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
Infinite Gray code has been introduced by Tsuiki as a redundancy-free representation of the reals. In applications the signed digit representation is mostly used which has maximal redundancy. Tsuiki presented a functional program converting signed digit code into infinite Gray code. Moreover, he showed that infinite Gray code can effectively be converted into signed digit code, but the program needs to have some non-deterministic features (see also H. Tsuiki, K. Sugihara, "Streams with a bottom in functional languages"). Berger and Tsuiki reproved the result in a system of formal first-order intuitionistic logic extended by inductive and co-inductive definitions, as well as some new logical connectives capturing concurrent behaviour. The programs extracted from the proofs are exactly the ones given by Tsuiki. In order to do so, co-inductive predicates \bS and \bG are defined and the inclusion \bS⊆\bG is derived. For the converse inclusion the new logical connectives are used to introduce a concurrent version §2 of S and \bG⊆\bS2 is shown. What one is looking for, however, is an equivalence proof of the involved concepts. One of the main aims of the present paper is to close the gap. A concurrent version \bG∗ of \bG and a modification \bS∗of \bS2 are presented such that \bS∗=\bG∗. A crucial tool in U. Berger, H. Tsuiki, "Intuitionistic fixed point logic" is a formulation of the Archimedean property of the real numbers as an induction principle. We introduce a concurrent version of this principle which allows us to prove that \bS∗ and \bG∗ coincide. A further central contribution is the extension of the above results to the hyperspace of non-empty compact subsets of the reals. |
|---|---|
| Keywords: |
Computing, real numbers, compact sets, signed-digit representation, Gray code representation, iterative function systems, program extraction, logic, inductive definition, co-inductive definition, constructive mathematics. |
| College: |
Faculty of Science and Engineering |
| Funders: |
Thisproject has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 731143. |
| Issue: |
3 |