No Cover Image

Journal article 94 views 25 downloads

Computing with Infinite Objects: the Gray Code Case

Dieter Spreen, Ulrich Berger Orcid Logo

Logical Methods in Computer Science, Volume: 19, Issue: 3

Swansea University Author: Ulrich Berger Orcid Logo

  • 65589.VOR.pdf

    PDF | Version of Record

    Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.

    Download (723.66KB)

Check full text

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...

Full description

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!
first_indexed 2024-04-04T13:22:34Z
last_indexed 2024-04-04T13:22:34Z
id cronfa65589
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>65589</id><entry>2024-02-08</entry><title>Computing with Infinite Objects: the Gray Code Case</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-02-08</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>19</volume><journalNumber>3</journalNumber><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic>1860-5974</issnElectronic><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.</keywords><publishedDay>6</publishedDay><publishedMonth>7</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-07-06</publishedDate><doi/><url>https://lmcs.episciences.org/11550</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><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.</funders><projectreference/><lastEdited>2024-04-04T14:26:53.4885522</lastEdited><Created>2024-02-08T00:10:50.6441334</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Dieter</firstname><surname>Spreen</surname><order>1</order></author><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>2</order></author></authors><documents><document><filename>65589__29921__876406e6992f47699ec892a47458757b.pdf</filename><originalFilename>65589.VOR.pdf</originalFilename><uploaded>2024-04-04T14:24:11.4913062</uploaded><type>Output</type><contentLength>741028</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0</licence></document></documents><OutputDurs/></rfc1807>
spelling v2 65589 2024-02-08 Computing with Infinite Objects: the Gray Code Case 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2024-02-08 SCS 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. Journal Article Logical Methods in Computer Science 19 3 1860-5974 Computing, real numbers, compact sets, signed-digit representation, Gray code representation, iterative function systems, program extraction, logic, inductive definition, co-inductive definition, constructive mathematics. 6 7 2023 2023-07-06 https://lmcs.episciences.org/11550 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University Thisproject has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 731143. 2024-04-04T14:26:53.4885522 2024-02-08T00:10:50.6441334 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Dieter Spreen 1 Ulrich Berger 0000-0002-7677-3582 2 65589__29921__876406e6992f47699ec892a47458757b.pdf 65589.VOR.pdf 2024-04-04T14:24:11.4913062 Output 741028 application/pdf Version of Record true Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license. true eng https://creativecommons.org/licenses/by/4.0
title Computing with Infinite Objects: the Gray Code Case
spellingShingle Computing with Infinite Objects: the Gray Code Case
Ulrich Berger
title_short Computing with Infinite Objects: the Gray Code Case
title_full Computing with Infinite Objects: the Gray Code Case
title_fullStr Computing with Infinite Objects: the Gray Code Case
title_full_unstemmed Computing with Infinite Objects: the Gray Code Case
title_sort Computing with Infinite Objects: the Gray Code Case
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Dieter Spreen
Ulrich Berger
format Journal article
container_title Logical Methods in Computer Science
container_volume 19
container_issue 3
publishDate 2023
institution Swansea University
issn 1860-5974
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url https://lmcs.episciences.org/11550
document_store_str 1
active_str 0
description 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.
published_date 2023-07-06T14:26:50Z
_version_ 1795410845389291520
score 11.016235

Similar Items