From coinductive proofs to exact real arithmetic: theory and applications

Ulrich Berger

doi:10.2168/LMCS-7(1:8)2011

Ulrich Berger - From coinductive proofs to exact real arithmetic: theory and applications

lmcs:1109 - Logical Methods in Computer Science, March 24, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:8)2011

From coinductive proofs to exact real arithmetic: theory and applicationsArticle

Authors: Ulrich Berger

Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.

https://doi.org/10.2168/LMCS-7(1:8)2011

Source: arXiv.org:1101.2162

Volume: Volume 7, Issue 1

Secondary volumes: Selected Papers of the 23rd International Workshop on Computer Science Logic and the 18th Annual Conference of the EACSL (CSL 2009)

Published on: March 24, 2011

Imported on: June 11, 2010

Keywords: Computer Science - Logic in Computer Science, 03F60

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

14 Documents citing this article

Nils Köpp;Helmut Schwichtenberg, 2022, Lookahead analysis in exact real arithmetic with logical methods, Theoretical Computer Science, 943, pp. 171-186, 10.1016/j.tcs.2022.10.003.

Ulrich Berger;Hideki Tsuiki, 2022, Extracting total Amb programs from proofs, Lecture notes in computer science, pp. 85-113, 10.1007/978-3-030-99336-8_4, https://doi.org/10.1007/978-3-030-99336-8_4.

Dieter Spreen, 2021, Computing with continuous objects: a uniform co-inductive approach, Mathematical Structures in Computer Science, 31, 2, pp. 144-192, 10.1017/s0960129521000116, https://doi.org/10.1017/s0960129521000116.

Emmanuel Hainry;Damiano Mazza;Romain Péchoux, 2020, Polynomial Time over the Reals with Parsimony, Lecture notes in computer science, pp. 50-65, 10.1007/978-3-030-59025-3_4.

Ulrich Berger;Hideki Tsuiki, 2020, Intuitionistic fixed point logic, arXiv (Cornell University), 172, 3, pp. 102903, 10.1016/j.apal.2020.102903, http://arxiv.org/abs/2002.00188.

Ulrich Berger, 2019, On the Constructive and Computational Content of Abstract Mathematics, Synthese Library/Synthese library, pp. 55-73, 10.1007/978-3-030-20447-1_6.

BASIL A. KARÁDAIS, 2018, Nonflatness and totality, Mathematical Structures in Computer Science, 29, 2, pp. 309-338, 10.1017/s0960129518000026.

Ulrich Berger;Olga Petrovska, 2018, Optimized Program Extraction for Induction and Coinduction, Lecture notes in computer science, pp. 70-80, 10.1007/978-3-319-94418-0_7.

ULRICH BERGER;TIE HOU, 2016, A realizability interpretation of Church's simple theory of types, Mathematical Structures in Computer Science, 27, 8, pp. 1364-1385, 10.1017/s0960129516000104.

Kenji Miyamoto;Fredrik Nordvall Forsberg;Helmut Schwichtenberg, 2013, Program Extraction from Nested Definitions, Lecture notes in computer science, pp. 370-385, 10.1007/978-3-642-39634-2_27.

Celia Picard;Ralph Matthes, 2012, Permutations in Coinductive Graph Representation, Lecture notes in computer science, pp. 218-237, 10.1007/978-3-642-32784-1_12, https://doi.org/10.1007/978-3-642-32784-1_12.

Ulrich Berger;Tie Hou, 2012, Typed vs. Untyped Realizability, Electronic Notes in Theoretical Computer Science, 286, pp. 57-71, 10.1016/j.entcs.2012.08.005, https://doi.org/10.1016/j.entcs.2012.08.005.

Keiko Nakata;Tarmo Uustalu;Marc Bezem, 2011, A Proof Pearl with the Fan Theorem and Bar Induction, Lecture notes in computer science, pp. 353-368, 10.1007/978-3-642-25318-8_26.

Ulrich Berger;Monika Seisenberger, 2011, Proofs, Programs, Processes, Theory of Computing Systems, 51, 3, pp. 313-329, 10.1007/s00224-011-9325-8.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3588 times.

This article's PDF has been downloaded 520 times.