Helmut Schwichtenberg ; Franziskus Wiesnet - Logic for exact real arithmetic

lmcs:5419 - Logical Methods in Computer Science, April 20, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:7)2021
Logic for exact real arithmeticArticle

Authors: Helmut Schwichtenberg ; Franziskus Wiesnet

    Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.


    Volume: Volume 17, Issue 2
    Published on: April 20, 2021
    Accepted on: March 21, 2021
    Submitted on: May 1, 2019
    Keywords: Mathematics - Logic
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Consultation statistics

    This page has been seen 1182 times.
    This article's PDF has been downloaded 405 times.