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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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)
Copeland, J., Proudfoot, D.: Alan Turing’s forgotten ideas in computer science. Sci. Am. 280(4), 99–103 (1999)
Etesi, G., Németi, I.: Non-turing computations via Malament-Hogarth space-times. Int. J. Theor. Phys. 41, 341–370 (2002)
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
Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis. Graduate Texts in Mathematics, vol. 188. Springer-Verlag, Heidelberg (1998)
Hogarth, M.: Deciding arithmetic using SAD computers. Br. J. Philos. Sci. 55, 681–691 (2004)
Madarász, J.X., Székely, G.: Special relativity over the field of rational numbers. Int. J. Theor. Phys. 52(5), 1706–1718 (2013)
Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge University Press, Cambridge (1999)
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
Robinson, A.: Non-Standard Analysis. Princeton University Press, Princeton (1996)
Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2003)
Siegelmann, H.: Computation beyond the Turing limit. Science 268(5210), 545–548 (1995). http://www.dx.doi.org/10.1126/science.268.5210.545
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
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
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
Stannett, M.: Computation and spacetime structure. Int. J. Unconv. Comput. 9(1–2), 173–184 (2013)
Stannett, M., Németi, I.: Using Isabelle/HOL to verify first-order relativity theory. J. Autom. Reasoning 52(4), 361–378 (2014)
Welch, P.: The extent of computation in Malament-Hogarth spacetimes (2006). arXiv:gr-qc/0609035
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)