Abstract
We give a coinductive characterization of the set of continuous functions defined on a compact real interval, and extract certified programs that 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. This is a pilot study in using proof-theoretic methods for certified algorithms in exact real arithmetic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Marcial-Romero, J.R., Escardo, M.H.: Semantics of a sequential language for exact real-number computation. Theor. Comput. Sci. 379, 120–141 (2007)
Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17, 3–36 (2007)
Edalat, A., Heckmann, R.: Computing with real numbers: I. The LFT approach to real number computation; II. A domain framework for computational geometry. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 193–267. Springer, Heidelberg (2002)
Ciaffaglione, A., Di Gianantonio, P.: A certified, corecursive implementation of exact real numbers. Theor. Comput. Sci. 351, 39–51 (2006)
Bertot, Y.: Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. 17, 37–63 (2007)
Berger, U., Hou, T.: Coinduction for exact real number computation. Theory Comput. Sys. (to appear, 2009)
Niqui, M.: Coinductive formal reasoning in exact real arithmetic. Logical Methods in Computer Science 4, 1–40 (2008)
Schwichtenberg, H.: Realizability interpretation of proofs in constructive analysis. Theory Comput. Sys. (to appear, 2009)
Berger, U., Seisenberger, M.: Applications of inductive definitions and choice principles to program synthesis. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis Towards practicable foundations for constructive mathematics. Oxford Logic Guides, vol. 48, pp. 137–148. Oxford University Press, Oxford (2005)
Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electr. Notes in Theoret. Comp. Sci. 164 (2006)
Buchholz, W., Feferman, F., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof–Theoretical Studies. Lecture Notes in Mathematics, vol. 897. Springer, Berlin (1981)
Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3, pp. 721–756. Elsevier, Amsterdam (2007)
Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous Lattices and Domains. Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press, Cambridge (2003)
Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, 101–128 (1959)
Tatsuta, M.: Realizability of monotone coinductive definitions and its application to program synthesis. In: Jeuring, J. (ed.) MPC 1998. Lecture Notes in Mathematics, vol. 1422, pp. 338–364. Springer, Heidelberg (1998)
Troelstra, A.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Heidelberg (1973)
Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handb. Logic Comput. Sci., vol. 3, pp. 1–168. Clarendon Press, Oxford (1994)
Malcolm, G.: Data structures and program transformation. Science of Computer Programming 14, 255–279 (1990)
Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, pp. 115–134. Clarendon Press, Oxford (2005)
Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333, 3–66 (2005)
Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Information and Computation 204, 437–468 (2006)
Konečný, M.: Real functions incrementally computable by finite automata. Theor. Comput. Sci. 315, 109–133 (2004)
Blanck, J.: Efficient exact computation of iterated maps. Journal of Logic and Algebraic Programming 64, 41–59 (2005)
Plume, D.: A Calculator for Exact Real Number Computation. PhD thesis. University of Edinburgh (1998)
Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., Zuber, W.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction – A Basis for Applications. Applied Logic Series, vol. II, pp. 41–71. Kluwer, Dordrecht (1998)
Scriven, A.: A functional algorithm for exact real integration with invariant measures. Electron. Notes Theor. Comput. Sci. 218, 337–353 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berger, U. (2009). From Coinductive Proofs to Exact Real Arithmetic. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-04027-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04026-9
Online ISBN: 978-3-642-04027-6
eBook Packages: Computer ScienceComputer Science (R0)