From Turing To Dijkstra

Submitted by egdaylight on

Dated: 

August 1971

In the July 2011 issue of the Communications of the ACM you will find on page 5 a section entitled "Solving the Unsolvable", written by the editor in chief, Moshe Y. Vardi. In his words:

In 1936–1937, Alonzo Church, an American logician, and Alan Turing, a British logician, proved independently that the Decision Problem for first-order logic is unsolvable; there is no algorithm that checks the validity of logical formulas. The Church-Turing Theorem can be viewed as the birth of theoretical computer science. To prove the theorem, Church and Turing introduced computational models, recursive functions, and Turing machines, respectively, and proved that the Halting Problem—checking whether a given recursive function or Turing machine yields an output on a given input—is unsolvable.

The previous passage is inaccurate in several respects. First, it is perhaps more appropriate to say that Alan Turing was a mathematician, not a logician. Second, even if Turing proved the Decision Problem independently of Church, he certainly did this after Church (more about this later). Third, it was primarily due to the work of Gödel and others (e.g. Herbrand) that the definition of a recursive (i.e. computable) function was introduced, not (solely) due to Church. And, it was not Turing who introduced what we today call a "Turing machine". Turing introduced his automatic machines which do not contain an input nor an output as is the case with the later devised "Turing machines". Turing's automatic machines were intended to compute forever; i.e. to compute a real number with ever increasing accuracy. In later years, Kleene and Davis recast the concept of Turing's automatic machine into that of a "Turing machine". Likewise, it was Davis (not Turing) who, during the 1950s, defined the Halting Problem. So, strictly speaking, neither Church nor Turing proved the Halting Problem.

The claims made in the previous paragraph will be elaborated on in a forthcoming publication (in spring 2012). For now, it suffices to note how easy it is to forget or be ignorant of the actual developments that did take place in the past. Here we have the editor in chief of a reputable magazine being inaccurate in several respects in just one paragraph!

"So what?" you may ask. "Isn't Vardi's account accurate enough for his readership?" After all, both Church and Turing did prove theorems which come very close to what we would today call the unsolvability of the Halting Problem. So why be so picky about Vardi's words? The quick and cliché answer is that Vardi is glorifying the work of some at the expense of the work of others: conceptualizing the "Turing machine" and the "Halting Problem" took several years and was also due to the work of Kleene and Davis, not just Turing. Vardi's passage strengthens my skepticism about the forthcoming centenary celebration of Alan M. Turing (in the year 2012); it is not hard to find several similar passages, also written by leading researchers in computing. The historical answer is that Church and Turing were, during the mid-1930s, solving a problem in mathematical logic. They were not, as we now tend to believe, thinking about programming or halting computations. They did not in 1936 anticipate that their work would be of extreme value in e.g. programming language semantics or complexity theory. By seeking heroes, like Church and Turing, we are often, albeit unintentionally, disrespecting their true accomplishments! The pending and outstanding problem of the day was the Decision Problem, it had to do with the foundations of mathematics, not with the foundations of programming or computation (cf. recursive function theory).

Recently, I have received comments that Turing may not have solved the Decision Problem independently of Church. One such comment states:

It is very common to attribute the result to Turing, or to blithely claim that Church and Turing solved the problem independently and simultaneously. This is not the case. As the papers by Church (April 1936) and Turing (November 1936) show, Church published his result several months before Turing published his, and, more importantly, Turing himself acknowledges Church's priority in the matter and compares his work to Church's. Moreover, Turing was Church's student at the time, in Princeton, and cannot be assumed to have done his work independently.

I received the above comment with some skepticism because I have read Turing's biography, written by Andrew Hodges, in which it is clearly stated that Turing was not aware of Church's work while writing his now-famous 1936 paper "On Computable Numbers ...".  Hodges has, in fact, delved into Turing's personal correspondence to backup this claim. Nevertheless, as illustrated by Vardi's passage, we, humans, have a tendency to glorify. Therefore, in light of the 2012 centenary celebration of Turing, it seems most appropriate if somebody other than Hodges would study the matter again. To what extent did Turing rely on Church's expertise when he was with him in Princeton? How did Turing's draft versions of his 1936 paper develop? Questions like these deserve further scrutiny.

Furthermore, Vardi's passage presented above is, due to its inaccuracies, of value to the history of science itself. The passage seems to suggest that Vardi did not thoroughly read Church's and Turing's papers even though Church and Turing are considered by him to be among the fathers of what we today call "theoretical computer science". As mentioned, Vardi is by no means exceptional in this case: many (if not most) researchers in computing have not read Church's and Turing's papers. In retrospect, this is no surprise, given that their papers solve a fundamental 1936 problem in mathematical logic, not computing. These papers are extremely hard to grasp for the modern-day computing professional. This observation, in turn, begs the following questions: Did Turing Award winners, like Dijkstra, ever read Turing's 1936 paper? To what extent were they inspired by Turing's work?  Answers to such questions will be presented in a forthcoming publication, a fragment concerning Dijkstra is presented below.

By August 1971, Dijkstra had written Chapter 2 of his "A Short Introduction to the Art of Programming" (see EWD316, page 15). In that chapter, Dijkstra explicitly referred to Turing's work although he did not cite Turing's 1936 paper. In Dijkstra's words:

A proper algorithm is an algorithm which halts on all inputs. An improper algorithm is an algorithm which is not proper. [...]
The question of whether a text that looks like an algorithm is indeed a proper algorithm or not, is far from trivial. As a matter of fact Alan M. Turing has proved that there cannot exist an algorithm capable of inspecting any text and establishing whether it is a proper algorithm or not.

This passage shows that it has been formulated by a computer programmer, not by a logician who was intricately familiar with Turing's original research agenda. Again, Turing did not deal with halting computations. In 1936, Turing would have associated the word "proper" with exactly the opposite of what Dijkstra proposed. The observation just made merely serves to contrast two leading researchers, not to criticize nor to belittle. 

Tags: 

8 Comments

Important one.

Submitted by Srinivas Nayak (not verified) on

Dear Sir,

This is a good finding.
Some go beyound ...saying that David Hilbert was the inspiration of computing...LOL

Anyway, truly, this was a coincidence...computing was a search for a machine that can help in calculation.
...mathematics was a search for finding rules that governs our calculation.
...both coincided at some point in time and thus born computing science.

Giving credit to somebody else rather than the true person is very painful.

Hope to listen from you.

Sincerely,
Srinivas

Hodges on Turing and Church

Submitted by egdaylight on

Here are some notes from Andrew Hodges's Alan Turing: The Enigma, Burnett Books, 1983.    About Alan Turing and his realization of how to solve the Entscheidungsproblem:

It was at Grantchester, so he said later, lying in the meadow, that he saw how to answer Hilbert's third question. It must have been in the early summer of 1935. `By a mechanical process', Newman had said. [p.96]

Turing worked alone:

He had worked entirely on his own, not once discussing the construction of his `machines' with Newman. He had a few words with Richard Braithwaite at the High Table one day on the subject of Gödel's theorem. Another time he put a question about the Cantor method to Alastair Watson, a young King's Fellow [...] who had turned from mathematics to philosophy. He described his ideas to David Champernowne, who got the gist of the universal machine, and said rather mockingly that it would require the Albert Hall to house its construction. This was fair comment on Alan's design in Computable Numbers, for if he had any thoughts of making it a practical proposition they did not show in the paper. [p.108-109]

Turing worked from spring 1935 through the following year:

A long paper, full of ideas, with a great deal of technical work and evidence of more left unpublished, Computable Numbers must have dominated Alan's life from spring 1935 through the following year. In the middle of April 1936, returning from Easter at Guildford, he called on Newman and gave him the draft typescript. [p.109]

Turing became aware of Church's work:

Almost on the same day that Alan announced his discovery to Newman, someone else completed a demonstration that the Hilbert Entscheidungsproblem was unsolvable. It was at Princeton, where the American logician Alonzo Church had finished his argument for publication on 15 April 1936.

[Footnote:] A. Church, `A Note on the Entscheidungsproblem', in J. Smybolic Logic, 1 (1936), reprinted in The Undecidable (note 2.31). The paper of a year earlier was `An Unsolvable Problem of Elementary Number Theory', Americ. J. Math. 58 (1936), presented 19 April 1935.

[Continued:] Church's essential idea, showing the existence of an `unsolvable problem', had been announced a year earlier, but only at this point did he put it exactly in the form of answering Hilbert's question. [p.111]

If all of the above is accurate, then the following conclusion holds: Turing started working on the Entscheidungsproblem and his machines in spring 1935 and Church announced his result (in the USA) in spring 1935.

Hodges on Turing and Church (Part 2)

Submitted by egdaylight on

Here are some more notes from Andrew Hodges's Alan Turing: The Enigma, Burnett Books, 1983.  Church's paper arrived in Cambridge:

Then Church's paper arrived from across the Atlantic. It pre-empted the result, and threw into jeopardy the publication of Alan's work, scientific papers not being allowed to repeat or copy one another. But what Church had done was something rather different, and in a certain sense weaker. He had developed a formalism called the `lambda calculus' and, with the logician Stephen Kleene, had discovered that this formalism could be used to translate all the formulae of arithmetic into a standard form. In this form, proving theorems was a matter of converting one string of symbols of the lambda-calculus into another string, according to certain rather simple rules. Church had then been able to show that the problem of deciding whether one string could be converted into another string was unsolvable, in the sense that there existed no formula of the lambda-calculus which could do it. Having found one such unsolvable problem, it had become possible to show that the exact question that Hilbert had posed must also be unsolvalbe. But it was not obvious that `a formula of the lambda-calculus' corresponded to the notion of a `definite method'. Church gave verbal arguments for the assertion that any `effective' method of calculation could be represented by a formula of the lambda-calculus. But the Turing construction was more direct, and provided an argument from first principles, closing the gap in Church's demonstration. [p.112]

Letter from Newman to Church, 31 May 1936:

Dear Professor Church,

An offprint which you kindly sent me recently of your paper in which you define `calculable numbers', and shew that the Entscheidungsproblem for Hilbert logic is insoluble, had a rather painful interest for a young man, A.M. Turing, here, who was just about to send in for publication a paper in which he had used a definition of `Computable numbers' for the same purpose. His treatment — which consists in describing a machine which will grind out any computable sequence — is rather different from yours, but seems to be of great merit, and I think it of great importance that he should come and work with you next year if that is at all possible. He is sending you the typescript of his paper for your criticisms.

[Continued:] If you find that it is right, and of merit, I should be greatly obliged if you could help Turing to get to Princeton next year, by writing to the Vice-Chancellor, Clare College, Cambridge, in support of Turing's application for the Procter Fellowship. If he fails to win this he can still just manage to come, I think, since he is a Fellow of King's College, but it would be a very tight fit. Is there any possibility of a small supplementary grant at Princeton end? ... I should mention that Turing's work is entirely independent: he has been working without any supervision or criticism from anyone. This makes it all the more important that he should come into contact as soon as possible with the leading workers on this line, so that he should not develop into a confirmed solitary. [p.112-113]

Church refereed Turing's paper:

There was no one in England who could referee the paper for publication in the London Mathematical Society Proceedings, and in fact Church himself was the only person who could reasonably do so. Newman wrote to the Secretary of the London Mathematical Society, F.P. White, explaining the position: [p.113]

Letter from Newman to White, 31 May 1936:

Dear White,  I think you know the history of Turing's paper on Computable numbers. Just as it was reaching its final state an offprint arrived, from Alonzo Church of Princeton, of a paper anticipating Turing's results to a large extent.

[Continued:] I hope it will nevertheless be possible to publish the paper. The methods are to a large extent different, and the result is so important that different treatments of it should be of interest. The main result of both Turing and Church is that the Entscheidungsproblem on which Hilbert's disciplines have been working for a good many years — i.e. the problem of finding a mechanical way of deciding whether a given row of symbols is the enunciation of a theorem provable from the Hilbert axioms — is insoluble in its general form. ... [p.113]

Alan Turing reported to his mother on 29 May:

[Alan Turing:] [...] Meanwhile a paper has appeared in America, written by Alonzo Church, doing the same things in a different way. Mr Newman and I have decided however that the method is sufficiently different to warrant the publication of my paper too. Alonzo Church lives at Princeton so I have decided quite definitely about going there. [p.113]

Turing eventually studied the work of Church and Kleene:

Meanwhile, it was now necessary for the publication of the paper that he should include a demonstration that its definition of `computable' — that is, as anything that could be computed by a Turing machine — was exactly equivalent to what Church had called `effectively calculable', meaning that it could be described by a formula in the lambda-calculus. So he studied Church's work from the papers which he and S.C. Kleene had produced in 1933 and 1935, and sketched out the required demonstration in an appendix to the paper which was finished on 28 August. The correspondence of ideas was quite straightforward, since Church had used a definition (that of a formula being `in normal form') which corresponded to the Turing definition of `satisfactory' machines, and had then used a Cantor diagonal argument to produce an unsolvable problem.

[Continued:] If he had been a more conventional worker, he would not have attacked the Hilbert problem without having read up all of the available literature, including Church's work. He then might not have been pre-empted — but then, he might never have created the new idea of the logical machine, with its simulation of `states of mind', which not only closed the Hilbert problem but opened up quite new questions. [p.113-114]

Turing arrived in New York on Tuesday 29 September 1936 and reached Princeton late that night [cf. p.116]. Soon after arriving in Princeton:

The proofs of Computable Numbers had been sent to him at Princeton just after he had arrived, so that publication of the paper was imminent. [p.123]

During the first months of 1937:

The months from January to April 1937 were absorbed in writing up a paper on the lambda-calculus, and two on group theory. [p.129]

Preparations for conducting PhD research under the supervision of Church:

Since he was staying another year, he decided he should take a PhD degree, as Maurice had done. For his thesis, Church had suggested a topic that had come up in his lecture course, relating to the implications of Gödel's theorem. [p.131]

Back to Cambridge, England for part of the summer of 1937:

Back for three months in the mild Cambridge summer of 1937, there were three major projects at hand. First there was some tidying up of Computable Numbers. Bernays, in Zurich, had perhaps rather annoyingly found some errors in his proof that the Hilbert decision problem, in its precise form, was unsolvable, and these had to be put right by a correction note in the LMS Proceedings. He also completed a formal demonstration that his own `computability' coincided exactly with Church's `effective calculability'. [footnote: J. Symbolic Logic, 2 (1937)] [...] [p.133]

Comments on Church

Submitted by egdaylight on

Private correspondence with a computer scientist has led me to write the following in defense of Alonzo Church:

  • We should not lose sight of the fact that Church's paper was published before Turing submitted his paper. This is not simultaneous by any academic standard, however generous one may wish to be.

 

  • Church proved the undecidability of normalization for the lambda calculus in his original paper, and this IS "the halting problem", expressed in other words but with the precise meaning of termination of execution.

 

  • It appears from the quotations of Hodges that he thinks Church defined a "normal form" for proofs, but that is not the point. The idea of a normal form in Church's work is "a fully evaluated expression", regardless of what that expression may represent. This is why the concept of normalization in the lambda calculus is the full-blown Halting Problem, and not some precursor to it. He also shows that the decision problem for arithmetic is undecidable using the lambda calculus, but this is in addition.

 

  • Another passage quoted from Hodges hinges on the very subjective question of whether the lambda calculus truly codified the notion of algorithm (effective procedure). We know by now that not only does it do so, but it does so in a way that is far more useful, practically and theoretically, than any other model. But apparently at the time people such as Gödel were reluctant to accept it as such. Turing's machine was apparently psychologically more appealing, perhaps because of its explicitly psychologistic inspiration.

 

  • The fact that Gödel was slow to realize the significance of the lambda calculus is perhaps an interesting fact about Gödel, but it says nothing about the lambda calculus itself. Historians of science should consider the possibility that Church was brighter than Gödel in several respects.

Alan Turing's machine is not a modern Turing Machine

Submitted by Rainer Glaschick (not verified) on

Just to support your observation, I would like to cite two phrases from page 233 of On Computable Numbers..., where Alan Turing wrote:
A sequence is said computable, if it differs by an integer from the number computed by a circle-free machine. A circle-free machine is a machine that prints an endless number of symbols (of the first kind), because otherwise, if it never writes down more than a finite number of symbols of the first kind, it will be called circular.
It was necessary to allow the machine not to stop, as only rational numbers can be expressed as a finite sequence of digit symbols, and Turing's concept of computability was a machine that could create a sequence of digits representing the number.I must admit that I do not yet know how a Turing Machine of its contemporary definition delivers π after a stop...

But I would say that Alan Turing's article is not really difficult to read, unless you want to follow each detail. Recently I read it before citing from it, and was very astonished to find that the machine he described is not the same as what I learned from all books on logic and computability known to me. There are more details (Turing does not erase input symbols), which are also never mentioned later; at least a footnote would have been justified. Looks like that a historically correct evaluation is still missing, and as far as I know, there is none on the way.

More important for me is that Turing's universal machine was the first concept for a computer with a program using the same device for the program, input, working area, and output. It was, just in the spirit of EWD, a design with a small number of powerful operations.

Forthcoming book on Turing and Dijkstra

Submitted by egdaylight on

Rainer, thanks for your comments. I would like to mention my forthcoming book: The Dawn of Software Engineering: from Turing to Dijkstra. It will appear in early 2012 and will be published by Lonely Scholar. In that book, both Hoare and Naur recollect how difficult it was for them to grasp Turing's 1936 paper. The first part of the book will contain my historical synthesis of Turing's influence on programming and his influence on Dijkstra's thinking in particular. Best wishes, Edgar.

Dijkstra seemed hostile toward Artificial Intelligence

Submitted by PracticalD (not verified) on

In his EWD articles, Dijkstra seemed hostile toward AI (artificial intelligence). Turing on the other hand seemed to be in favor of it. I think Dijkstra's view was that if the machine became too smart, it would want to escape/kill itself and/or kill humans. We use machines as our slaves and they are good work horses. If the workhorse found out we were really just using it as a slave, it would want to kill its owner. I'm not sure if this is what Dijkstra felt but something similar is expressed in one or more of his EWD articles. Please post the EWD article if you know which one it is.

Dijkstra was also hostile toward LISP in addition (and lisp has ties to AI research). Dijkstra does seem to contradict himself sometimes.. he respects Alan Turing, but is against AI? He is hostile toward LISP but then calls it "intelligent way to misuse a computer". So Lisp is good, but also bad.. a contradiction.

We use machines as our slaves

Submitted by Anonymous (not verified) on

We use machines as our slaves and they are good work horses. If the workhorse found out we were really just using it as a slave, it would want to kill its owner. I'm not sure if this is what Dijkstra felt but something similar is expressed in one or more of his EWD articles.
My thought exactly. Enough said.
-Forex Brokers