Should computations halt?

Abstract

The so-called Hilbert's Program, aiming at a full axiomatization of mathematics, fuelled the quest to provide an answer to the Entscheidungsproblem, the Decision Problem, aiming to find effective methods to obtain the truth value of logical sentences. Intuitively, when using such methods a halting behavior would be desirable, thus providing a clear answer to the prospective user. This was implicit in Hilbert's finitist approach to the foundations of mathematics and practical use of logical methods. In 1936 the quest for such effective methods brought four different approaches: Kleene's formulation of G"odel/Herbrand general recursion, Church's $\lambda$-definability, Turing's computation with automatic machines (a-machines), and Post's machines. However, the halting issue was treated quite differently in those approaches. In particular, the \emph{technical} meaning of ``computation'' was explicitly introduced by Turing in his 1936 paper and he payed no attention to halting computations there. This paper traces how the halting requirement became a stable part of the definition of computation which is often used today.