Skip to main content

Towards Formal Verification of Computations and Hypercomputations in Relativistic Physics

  • Conference paper
  • First Online:
Machines, Computations, and Universality (MCU 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9288))

Included in the following conference series:

Abstract

It is now more than 15 years since Copeland and Proudfoot introduced the term hypercomputation. Although no hypercomputer has yet been built (and perhaps never will be), it is instructive to consider what properties any such device should possess, and whether these requirements could ever be met. Aside from the potential benefits that would accrue from a positive outcome, the issues raised are sufficiently disruptive that they force us to re-evaluate existing computability theory. From a foundational viewpoint the questions driving hypercomputation theory remain the same as those addressed since the earliest days of computer science, viz. what is computation? and what can be computed? Early theoreticians developed models of computation that are independent of both their implementation and their physical location, but it has become clear in recent decades that these aspects of computation cannot always be neglected. In particular, the computational power of a distributed system can be expected to vary according to the spacetime geometry in which the machines on which it is running are located. The power of a computing system therefore depends on its physical environment and cannot be specified in absolute terms. Even Turing machines are capable of super-Turing behaviour, given the right environment.

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

References

  1. Andréka, H., Madarász, J.X., Németi, I.: Logical analysis of relativity theories. In: Hendricks, et al. (eds.) First-Order Logic Revisited, pp. 1–30. Logos Verlag, Berlin (2004)

    Google Scholar 

  2. Copeland, J., Proudfoot, D.: Alan Turing’s forgotten ideas in computer science. Sci. Am. 280(4), 99–103 (1999)

    Article  Google Scholar 

  3. Etesi, G., Németi, I.: Non-turing computations via Malament-Hogarth space-times. Int. J. Theor. Phys. 41, 341–370 (2002)

    Article  MATH  Google Scholar 

  4. Genzel, R., Schoedel, R., Ott, T., Eckart, A., Alexander, T., Lacombe, F., Rouan, D., Aschenbach, B.: Near-infrared flares from accreting gas around the supermassive black hole at the Galactic Centre (2003). arXiv:astro-ph/0310821

  5. Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis. Graduate Texts in Mathematics, vol. 188. Springer-Verlag, Heidelberg (1998)

    MATH  Google Scholar 

  6. Hogarth, M.: Deciding arithmetic using SAD computers. Br. J. Philos. Sci. 55, 681–691 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  7. Madarász, J.X., Székely, G.: Special relativity over the field of rational numbers. Int. J. Theor. Phys. 52(5), 1706–1718 (2013)

    Article  MATH  Google Scholar 

  8. Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  9. Nipkow, T.: Programming and proving in Isabelle/HOL, August 2014. http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/prog-prove.pdf

  10. Robinson, A.: Non-Standard Analysis. Princeton University Press, Princeton (1996)

    MATH  Google Scholar 

  11. Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  12. Siegelmann, H.: Computation beyond the Turing limit. Science 268(5210), 545–548 (1995). http://www.dx.doi.org/10.1126/science.268.5210.545

    Article  Google Scholar 

  13. Stannett, M.: Super-Turing computation. Seminar presentation, Department of computer science, University of Sheffield (1990). http://www.researchgate.net/publication/258848388_1990_Super-Turing_Computation

  14. Stannett, M.: X-machines and the halting problem: building a super-Turing machine. Formal Aspects Comput. 2(1), 331–341 (1990). http://www.dx.doi.org/10.1007/BF01888233

    Article  MathSciNet  MATH  Google Scholar 

  15. Stannett, M.: An introduction to post-Newtonian and super-Turing computation. Technical report CS-91-02, Department of Computer Science, University of Sheffield (1991). http://www.researchgate.net/publication/236852111_An_Introduction_to_post-Newtonian_and_super-Turing_computation

  16. Stannett, M.: Computation and spacetime structure. Int. J. Unconv. Comput. 9(1–2), 173–184 (2013)

    Google Scholar 

  17. Stannett, M., Németi, I.: Using Isabelle/HOL to verify first-order relativity theory. J. Autom. Reasoning 52(4), 361–378 (2014)

    Article  Google Scholar 

  18. Welch, P.: The extent of computation in Malament-Hogarth spacetimes (2006). arXiv:gr-qc/0609035

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Mike Stannett .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Stannett, M. (2015). Towards Formal Verification of Computations and Hypercomputations in Relativistic Physics. In: Durand-Lose, J., Nagy, B. (eds) Machines, Computations, and Universality. MCU 2015. Lecture Notes in Computer Science(), vol 9288. Springer, Cham. https://doi.org/10.1007/978-3-319-23111-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23111-2_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23110-5

  • Online ISBN: 978-3-319-23111-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics