Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 2000: Types for Proofs and Programs pp 125–144Cite as

Towards Limit Computable Mathematics

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2277))

Abstract

The notion of Limit-Computable Mathematics (LCM) will be introduced. LCM is a fragment of classical mathematics in which the law of excluded middle is restricted to Δ 02 -formulas. We can give an accountable computational interpretation to the proofs of LCM. The computational content of LCM-proofs is given by Gold’s limiting recursive functions, which is the fundamental notion of learning theory. LCM is expected to be a right means for “Proof Animation”, which was introduced by the first author [10]. LCM is related not only to learning theory and recursion theory, but also to many areas in mathematics and computer science such as computational algebra, computability theories in analysis, reverse mathematics, and many others.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Akama, Y.: Limiting PartialC ombinatory Algebras Towards Infinitary Lambdacalculi and Classical Logic, in Proc. of Computer Science Logic, Lecture Notes in Computer Science, Springer, 2001.

    Google Scholar 

  2. Beeson, M.: Foundations of Constructive Mathematics, Springer, 1985

    Google Scholar 

  3. Baratella, S. and Berardi, S.: Constructivization via Approximations and Examples, Theories of Types and Proofs, M. Takahashi, M. Okada and M. Dezani-Ciancaglini eds., MSJ Memories 2 (1998) 177–205

    Google Scholar 

  4. Berardi, S.: Classical logic as Limit Completion,-a constructive model for non-recursive maps-, submitted, 2001, available at http://www.di.unito.it/~stefano/Berardi-ClassicalLogicAsLimit-I.rtf.

  5. Bishop, E.: Foundations of Constructive Analysis, McGraw-Hill, 1967

    Google Scholar 

  6. Blum, L. et al.: Complexity and Real Computation, Springer, 1997

    Google Scholar 

  7. Coquand, Th. and Palmgren, E.: Intuitionistic choice and classical logic, Archive for Mathematical Logic, 39 (2000) 53–74

    Article  MATH  MathSciNet  Google Scholar 

  8. Gold, E. M.: Limiting Recursion, The Journal of Symbolic Logic, 30 (1965) 28–48

    Article  MATH  MathSciNet  Google Scholar 

  9. Hayashi, S. and Nakano, H.: PX: A Computational Logic, 1988, The MIT Press

    Google Scholar 

  10. Hayashi, S., Sumitomo, R. and Shii, K.: Towards Animation of Proofs-Testing Proofs by Examples-, Theoretical Computer Science (to appear)

    Google Scholar 

  11. Hilbert, D.: Über die Theorie der algebraische Formen, Mathematische Annalen 36 473–531

    Google Scholar 

  12. Hilbert, D.: Theory of Algebraic Invariants, Cambridge Mathematical Library (1993)

    Google Scholar 

  13. Ishihara, H.: Anomniscience principle, the König lemma and the Hahn-Banach theorem, Zeitschrift für Logik und Grundlagen der Mathematik 36 (1990) 237–240

    Article  MATH  MathSciNet  Google Scholar 

  14. Kohlenbach, U.: Intuitionistic choice and restricted classical logic, Math. Logic Quarterly (to appear)

    Google Scholar 

  15. Kohlenbach, U.: Two unpublished notes, November and December, 2000.

    Google Scholar 

  16. Nakata, M. and Hayashi, S.: Realizability Interpretation for Limit Computable Mathematics, 2001, Scientiae Mathematicae Japonicae (to appear)

    Google Scholar 

  17. Odifreddi, P. G.: Classical Recursion Theory North-Holland, 1989

    Google Scholar 

  18. Simpson, S. G.: Subsystems of Second Order Arithmetic, Springer, 1999

    Google Scholar 

  19. Simpson, S. G.: Ordinaln umbers and the Hilbert basis theorem, Journalo f Symbolic Logic, 53 (1988) 961–974

    Article  MATH  MathSciNet  Google Scholar 

  20. Strong, H. R.: Algebraically Generalized Recursive Function Theory, IBM journal of Research and Development, 12 (1968) 465–475

    Article  MATH  MathSciNet  Google Scholar 

  21. Takeuti, G.: Proof Theory, 2nd ed., North-Holland, 1987

    Google Scholar 

  22. Wagner, E. G.: Uniformly Reflexive Structures: On the Nature of Gödelizations and Relative Computability, Transactions of the American Mathematical Society, 144 (1969) 1–41

    Article  MathSciNet  Google Scholar 

  23. Yasugi, M., Brattka, V. and Washihara, M.: Computability aspects of some discontinuous functions, 2001, Scientiae Mathematicae Japonicae(to appear)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Systems Engineering, Kobe University, Rokko, Nada, Kobe, Japan

    Susumu Hayashi

  2. Graduate School of Science and Technology, Kobe University, Rokko, Nada, Kobe, Japan

    Masahiro Nakata

Authors
  1. Susumu Hayashi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Masahiro Nakata
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK

    Paul Callaghan , Zhaohui Luo , James McKinna  & Robert Pollack , ,  & 

  2. Division of Informatics Laboratory for Foundations of Computer Science, The University of Edinburgh, James Clerk Maxwell Building, The King’s Buildings Mayfield Road, EH9 3JZ, Edinburgh, Scotland, UK

    Robert Pollack

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hayashi, S., Nakata, M. (2002). Towards Limit Computable Mathematics. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds) Types for Proofs and Programs. TYPES 2000. Lecture Notes in Computer Science, vol 2277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45842-5_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-45842-5_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43287-6

  • Online ISBN: 978-3-540-45842-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation