Dieter Spreen ; Ulrich Berger - Computing with Infinite Objects: the Gray Code Case

lmcs:7529 - Logical Methods in Computer Science, July 6, 2023, Volume 19, Issue 3 - https://doi.org/10.46298/lmcs-19(3:1)2023
Computing with Infinite Objects: the Gray Code CaseArticle

Authors: Dieter Spreen ; Ulrich Berger

    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 \subseteq \bG$ is derived. For the converse inclusion the new logical connectives are used to introduce a concurrent version $\S_{2}$ of $S$ and $\bG \subseteq \bS_{2}$ 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 $\bS_{2}$ 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.


    Volume: Volume 19, Issue 3
    Published on: July 6, 2023
    Accepted on: May 21, 2023
    Submitted on: June 1, 2021
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Classifications

    Mathematics Subject Classification 20201

    Consultation statistics

    This page has been seen 1193 times.
    This article's PDF has been downloaded 470 times.