Complexity and Intensionality in a Type-1 Framework for Computable Analysis

  • Branimir Lambov
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


This paper describes a type-1 framework for computable analysis designed to facilitate efficient implementations and discusses properties that have not been well studied before for type-1 approaches: the introduction of complexity measures for type-1 representations of real functions, and ways to define intensional functions, i.e. functions that may return different real numbers for the same real argument given in different representations.

This approach has been used in a recently developed package for exact real number computations, which achieves performance comparable to the performance of machine precision floating point.


Real Function Computable Analysis Machine Precision Computable Function Domain Theoretic Framework 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Berger, U., Oliva, P.: Modified Bar Recursion and Classical Dependent Choice. Lecture Notes in Logic 20, 89–107 (2005)MathSciNetGoogle Scholar
  2. 2.
    Brattka, V.: Recursive characterisation of computable real-valued functions and relations. Theoret. Comput. Sci. 162, 47–77 (1996)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Briggs, K.: Implementing exact real arithmetic in python, C++ and C (to appear in Journal of theoretical computer science), See also
  4. 4.
    Buss, S.R., Kapron, B.M.: Resource-bounded continuity and sequentiality for type-two functionals. ACM Transactions on Computational Logic 3(3), 402–417 (7/2002)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Cook, S.A., Kapron, B.M.: Characterizations of the basic feasible functionals of finite type. In: Buss, S., Scott, P. (eds.) Feasible Mathematics: A Mathematical Sciences Institute Workshop, Birkhauser, pp. 71–96 (1990)Google Scholar
  6. 6.
    Cook, Stephen, A.: Computability and complexity of higher type functions. In: Logic from computer science, Berkeley, CA, 1989. Math. Sci. Res. Inst. Publ, vol. 21, pp. 51–72. Springer, New York (1992)Google Scholar
  7. 7.
    Edalat, A.: Exact Real Number Computation Using Linear Fractional Transformations. Final Report on EPSRC grant GR/L43077/01, Available at
  8. 8.
    Edalat, A., Sünderhauf, P.: A domain-theoretic approach to computability on the real line. Theoret. Comput. Sci. 210(1), 73–98 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Escardo, M., Hofmann, M., Streicher, T.: On the non-sequential nature of the intervaldomain model of real-number computation. Math. Struct. in Comp. Science 14, 803–814 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 280–287 (1958)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Grzegorczyk, A.: On the definitions of computable real continuous functions. Fundamenta Matematicae 44, 61–67 (1957)zbMATHMathSciNetGoogle Scholar
  12. 12.
    Hinman, P.G.: Recursion-theoretic hierarchies. Springer, Heidelberg (1978)zbMATHGoogle Scholar
  13. 13.
    Howard, W.A.: Hereditarily majorizable functionals of finite type. In: Troelstra (ed.) Metamathematical investigation of intuitionistic arithmetic and analysis, vol. 344, pp. 454–461. Springer LNM, Heidelberg (1973)Google Scholar
  14. 14.
    Kapron, B.M., Cook, S.A.: A new characterization of type-2 feasibility. SIAM J. Comput. 25(1), 117–132 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Kleene, S.C.: Countable Functionals. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 81–100. North-Holland, Amsterdam (1959)Google Scholar
  16. 16.
    Kleene, S.C.: Recursive Functionals and Quantifiers of Finite Types I. Trans. Amer. Math. Soc. 91, 1–52 (1959)zbMATHMathSciNetGoogle Scholar
  17. 17.
    Ko, K.-I.: Complexity theory of real functions. Birkhäuser, Boston-Basel-Berlin (1991)Google Scholar
  18. 18.
    Kohlenbach, U.: Theory of majorizable and continuous functionals and their use for the extraction of bounds from non-constructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness (german). PhD Dissertation, Frankfurt (1990)Google Scholar
  19. 19.
    Kreisel, G.: Interpretation of analysis by means of functionals of finite type. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 101–128. North-Holland, Amsterdam (1959)Google Scholar
  20. 20.
    Lambov, B.: A two-layer approach to the computability and complexity of real functions. Computability and complexity in analysis (Cincinnati, 2003), 279–302, Informatik Berichte, 302, Fernuniversität Hagen (8/2003), See also
  21. 21.
    Lambov, B.: RealLib, an Efficient Implementation of Exact Real Arithmetic (submitted), Available at
  22. 22.
    Lambov, B.: RealLib3 Manual, Available at
  23. 23.
    Mosses, P.D.: Action Semantics. Cambridge Tracts in Theoretical Computer Science, vol. 26. Cambridge University Press, Cambridge (1992)zbMATHCrossRefGoogle Scholar
  24. 24.
    Pour-El, M.B., Richards, J.I.: Computability in Analysis and Physics. Springer, Heidelberg (1989)zbMATHGoogle Scholar
  25. 25.
    Marcial-Romero, J.R., Escardo, M.: Semantics of a sequential language for exact realnumber computation. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 426–435 (7/2004)Google Scholar
  26. 26.
    Müller, N.: The iRRAM: Exact arithmetic in C++. In: Blank, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, p. 222. Springer, Heidelberg (2001), See also CrossRefGoogle Scholar
  27. 27.
    Schwichtenberg, H.: Constructive Analysis with Witnesses (Marktoberdorf 2003) (2003), Available at
  28. 28.
    Skordev, D.: Characterization of the computable real numbers by means of primitive recursive functions. In: Blank, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 296–309. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  29. 29.
    Weihrauch, K.: Computable Analysis. Springer, Heidelberg (2000)zbMATHGoogle Scholar
  30. 30.
    Yap, Chee: Towards Exact Geometric Computation. Computational Geometry: Theory and application, 3-23 (9/1997), See also

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Branimir Lambov
    • 1
  1. 1.BRICS, Department of Computer ScienceUniversity of AarhusDenmark

Personalised recommendations