\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{The Halting Problem is Soluble in Malament-Hogarth Spacetimes}
\author{Mike Stannett\\University of Sheffield, UK}
\maketitle

\abstract{We provide an Isabelle verification that the (Turing) 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 simply assume the existence of a
reachability relation, $p \leadsto q$, defined on an abstract space of \emph{locations}; this captures the idea that a user (or signal) can travel from one location to another in finite proper time. An MH spacetime can then be described as a space in which there exists an unboundedly long path $mhline$, and a location $mhpoint$ which is reachable from all points on $mhline$. Likewise, we use a very general notion of \emph{computation} - the `current state' of a computation is assumed to be representable as a machine \emph{configuration} containing all the information required to determine how the system changes with the execution of each ensuing instruction. To specify a computation you provide the initial configuration, and the `operating system' (the action of which is modeled via an assumed function, $\mathit{getNextConfig}$, then computes successor configurations one by one. The program is deemed to halt if the system enters a configuration which is left unchanged under $\mathit{getNextConfig}$. 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.
}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
