Strachey and ApSimon, 1965

Dated: 

1 November 2017

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]=True if R terminates if run and that T[R]=False if R does not terminate. Consider the routine P defined as follows

 

rec routine P

   #L:   if T[P] go to L

Return #

 

If T[P]=True the 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]=True if R terminates if run; T[R]=False if 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 instructions P'

#L:   if Y go to L 

Return #

 

In working through this set of instructions we arrive at the question: what is the value of Y? Is Y true or is it false? 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 absurdum argument 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 indicate which of 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.

Tags: