Halting still standing - Programs versus specifications

In UTP’06 [4], Hehner claims that the traditional proof of the incomputability of the Halting Function is rather a proof of the inconsistency of its specification. We identify where his argument fails. Hehner claims that assuming a well-defined Halting Function for specifications leads to a contradiction by a very similar argument as assuming a computable Halting Function for programs does. In the case of programs, this argument leads to concluding that the Halting Function is not computable, porting the proof to the case of specifications, it is claimed to allow concluding that the Halting Function is ill-defined. He reasons that if the Halting Function for specifications is ill-defined, then the concept of the Halting Function in general is inconsistent, including the one for programs. We do not challenge this generalization, but rather point out a flaw in his argument for the specification case. We formalize his argument in UTP-style. This enables us to show that there is a subtle tacit assumption being made about the recursive definition that is used to arrive at the contradiction, namely that the defining equation has a solution. We also explain why this does not affect the proof for the program case. Furthermore, we analyze whether recursion in the language Hehner uses is essential for his argument and our refutation. Porting the arguments to a language without recursion shows that the issue of the existence of the contradicting specification remains. We conclude that this line of argument does not challenge the healthiness of the concept of the Halting Function, including its extension to specifications