Submitted by egdaylight on

## Dated:

In 1965 Christopher Strachey introduced his termination problem, which I also call *Strachey's Halting Problem* in my writings, to the readership of The Computer Journal. Specifically, Strachey provided a “proof” that it is

impossible to write a program which can examine any other program and tell, in every case, if it will terminate or get into a closed loop when it is run. [5]

The word “program” here refers to a computer program written in the Combined Programming Language (CPL), a predecessor of C.

Several people disagreed with Strachey in Volume 8 of The Computer Journal, including H.G. ApSimon in 1965. I shall first present Strachey's short “proof” and then discuss some interesting passages from one of ApSimon's letters.

## Strachey's "Proof"

The “proof” provided by Strachey in his 1965 letter [5] goes like this:

Suppose T[R] is a Boolean function taking a routine (or program) R with no formal or free variables as its argument and that for all R, T[R]=

Trueif R terminates if run and that T[R]=Falseif R does not terminate. Consider the routine P defined as follows

rec routineP#L:

ifT[P]go toL

Return#

If T[P]=

Truethe routine P will loop, and it will only terminate if T[P]=False. In each case T[P] has exactly the wrong value, and this contradiction shows that the function T cannot exist.

Strachey's line of reasoning is incorrect for at least one obvious reason: T[...] should be taken to be a *computable* Boolean function, not merely a Boolean function. The conclusion of Strachey's proof should then amount to the rejection that T is computable. Strachey did not seem to be aware of the need for this correction, as his replies in Volume 8 (not shown here) indicate. Nevertheless, I emphasize that Strachey was at the forefront, advancing computer science by appropriating ideas from modern logic [2].

## ApSimon's Corrections, 27 August 1965

I believe ApSimon was trying to get the very same point across to Strachey: that T[...] should be taken to be a *computable* Boolean function. My hunch is that ApSimon was not well versed in now-classical recursion theory. Moreover, he was not able to rely on the concise terminology that we have today about computability. What I am trying to say is that while I, today, insist on using the adjective *computable*, ApSimon already conveyed the same message half a century ago.

ApSimon questioned Strachey's line of reasoning and Strachey's conclusion in particular, namely that the “function T cannot exist.” Here's part of ApSimon's letter from 27 August 1965:

I asserted that the function T exists by definition. Let us define it now.

Let R be a program (with no formal or free variables). Either R terminates if run or it does not. Define T[R]=

Trueif R terminates if run; T[R]=Falseif R does not terminate if run. T[R] is, then, defined for all R.

It should be noted that for certain R the value of T[R] is unknown [...] But the fact that the value of a function is in some cases unknown or unknowable does not affect the question of the existence of the function.

So, once again, T[...] is most definitely a function and Strachey was wrong to conclude that it is not. Moreover, T[...] is — using modern terminology — a partially computable function. Strachey only wrote about functions, not partially computable functions.

In the follow-up passage from ApSimon, it becomes clear that he was characterizing T[...] as a total partially computable function, i.e. a computable function. In ApSimon's words:

Consider the set of instructions P'

Set of instructionsP'#L:

ifYgo toL

Return#

In working through this set of instructions we arrive at the question: what is the value of Y? Is Y

trueor is itfalse? If the value of Y is known, then we can insert this value and, so, proceed with the execution of the set of instructions. But if the value of Y can not be determined until after the execution of P' has been proceeded with beyond this point (and clearly P' can not be proceeded with until after the value of Y has been determined) then we are at an impasse: P' can not be executed, and, so, is not a program. A particular case occurs when Y is T[P']; in this case P' is P. P is not, then, a program.

Today we have terminology to get the same message across more concisely: Y has to be *computable*. To be even more precise: subroutine Y has to implement a computable Boolean function. (There are some hidden assumptions here, such as “Hardware failure does not occur when executing Y,” and the like.)

Once again, if Y is strictly partially computable, then P' cannot be called a “program” in ApSimon's sense of the word. Subsequently, ApSimon was quite right to maintain that Strachey's proof was flawed:

I asserted that Mr. Strachey had drawn too restricted a conclusion from his argument. In any

reductio ad absurdumargument one has not just one hypothesis but several (or, if you like, one compound hypothesis). Arrival at a contradiction by a valid argument demonstrates that (at least) one of the original hypotheses is false. But it does not indicatewhichof the original hypotheses is false.

In the case of Mr. Strachey's argument a second hypothesis is (implicitly) introduced: that P is a program. The contradiction at which he arrives by valid argument demonstrates that one of the hypotheses is false. I maintain that his conclusion can be no more that “either T does not exist or P is not a program”.

Saying that “P is a program” is equivalent (or is almost equivalent) to saying that T is computable. Since T definitely exists by definition, Strachey's conclusion should have been that T is not computable.

This is good stuff given that Strachey's 1965 letter is often cited without mentioning that it contains a flawed proof; see e.g. [1, 3, 4]. A similar concern was raised by B.E. Boutel in August 1965, also in Volume 8 of The Computer Journal.

## REFERENCES

**[1]** B. Cook, A. Podelski, and A. Rybalchenko. Proving program termination. Communications of the ACM, 54(5):88-98, May 2011.**[2]** E.G. Daylight. *The Dawn of Software Engineering: from Turing to Dijkstra*. Lonely Scholar, 2012.**[3]** C.A.R. Hoare and D.C.S. Allison. Incomputability. ACM Computing Surveys, 4(3):169-178, 1972.**[4]** H.J. Schneider. Computability in an Introductory Course on Programming. Bulletin of the European Association for Theoretical Computer Science, 73:153-164, 2001.**[5]** C. Strachey. An impossible program. Letter to the Editor of the Computer Journal, page 313, 1965.