Email Gateway (May 10 2023 at 01:37): Email Gateway (May 10 2023 at 01:37):From: Tobias Nipkow <nipkow@in.tum.de>
The Halting Problem Is Soluble in Malament-Hogarth Spacetimes
Mike Stannett
We provide an Isabelle verification that the Halting Problem can be solved in
Malament-Hogarth (MH) spacetimes. Our proof is quite general -- rather than
assume the full machinery of general relativity, we only assume the existence of
a reachability relation defined on an abstract space of locations. An MH
spacetime can then be described as a space in which there exists an unboundedly
long path together with a location which is reachable from all points on that
path. Likewise, we use a very general notion of computation - the current state
of a computation is assumed to be representable as a machine configuration
containing all the information required to determine how the system changes with
the execution of each ensuing instruction. The program is deemed to halt if the
system enters a stable configuration. Since this situation is generally
detectable by an operating system, we can use its occurrence to trigger events
that exploit the nature of MH spacetimes, thereby enabling us to detect whether
or not halting will eventually have occurred. Our verification follows existing
arguments in the literature, albeit translated into this more general setting.
https://www.isa-afp.org/entries/MHComputation.html
Enjoy!
Last updated: Apr 24 2024 at 12:33 UTC