Program Extraction in Constructive Analysis

  • Helmut Schwichtenberg
Part of the Synthese Library book series (SYLI, volume 341)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Patrik Andersson. Exact real arithmetic with automatic error estimates in a computer algebra system. Master’s thesis, Mathematics department, Uppsala University, 2001.Google Scholar
  2. 2.
    Josef Berger. Exact calculation of inverse functions. Math. Log. Quart., 51(2):201–205, 2005.zbMATHCrossRefGoogle Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    Luis Cruz-Filipe. Constructive Real Analysis: A Type-Theoretical Formalization and Applications. PhD thesis, Nijmegen University, 2004.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    Mark Mandelkern. Continuity of monotone functions. Pacific J. Math., 99(2):413–418, 1982.zbMATHMathSciNetGoogle Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    Helmut Schwichtenberg. Minlog. In F. Wiedijk, editor, The Seventeen Provers of the World, vol. 3600 of LNAI, pp. 151–157. Springer Verlag, Berlin, 2006.Google Scholar
  11. 11.
    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.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  • Helmut Schwichtenberg
    • 1
  1. 1.Mathematisches Institut der Universität MüncheMünchenGermany

Personalised recommendations