Abstract
We sketch a development of constructive analysis in Bishop’s style, with special emphasis on low type-level witnesses (using separability of the reals). The goal is to set up things in such a way that realistically executable programs can be extracted from proofs. This is carried out for (1) the Intermediate Value Theorem and (2) the existence of a continuous inverse to a monotonically increasing continuous function. Using the Minlog proof assistant, the proofs leading to the Intermediate Value Theorem are formalized and realizing terms extracted. It turns out that evaluating these terms is a reasonably fast algorithm to compute, say, approximations of √2.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Patrik Andersson. Exact real arithmetic with automatic error estimates in a computer algebra system. Master’s thesis, Mathematics department, Uppsala University, 2001.
Josef Berger. Exact calculation of inverse functions. Math. Log. Quart., 51(2):201–205, 2005.
Ulrich Berger. Program extraction from normalization proofs. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, vol. 664 of LNCS, pp. 91–106. Springer Verlag, Berlin, Heidelberg, New York, 1993.
Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967.
Errett Bishop. Mathematics as a numerical language. In J. Myhill A. Kino and R.E. Vesley, editors, Intuitionism and Proof Theory, Proceedings of the summer conference at Buffalo N.Y. 1968, Studies in logic and the foundations of mathematics, pp. 53–71. North–Holland, Amsterdam, 1970.
Luis Cruz-Filipe. Constructive Real Analysis: A Type-Theoretical Formalization and Applications. PhD thesis, Nijmegen University, 2004.
Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pp. 101–128. North–Holland, Amsterdam, 1959.
Mark Mandelkern. Continuity of monotone functions. Pacific J. Math., 99(2):413–418, 1982.
Erik Palmgren. Constructive nonstandard analysis. In A. Petry, editor, Méthods et analyse non standard, vol. 9, pp. 69–97. Cahiers du Centre de Logique, 1996.
Helmut Schwichtenberg. Minlog. In F. Wiedijk, editor, The Seventeen Provers of the World, vol. 3600 of LNAI, pp. 151–157. Springer Verlag, Berlin, 2006.
Helmut Schwichtenberg. Recursion on the partial continuous functionals. In C. Dimitracopoulos, L. Newelski, D. Normann and J. Steel, editors, Logic Colloquium 2005, vol. 26 of Lecture Notes in Logic, pp. 173–201. Amer. Math. Soc., 2006.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Schwichtenberg, H. (2009). Program Extraction in Constructive Analysis. In: Lindström, S., Palmgren, E., Segerberg, K., Stoltenberg-Hansen, V. (eds) Logicism, Intuitionism, and Formalism. Synthese Library, vol 341. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-8926-8_13
Download citation
DOI: https://doi.org/10.1007/978-1-4020-8926-8_13
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-8925-1
Online ISBN: 978-1-4020-8926-8
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)