Back for three months in the mild Cambridge summer of 1937, there were three major projects on hand.
First there was some tidying up of Computable Numbers.
Bernays, in Zurich, had perhaps rather annoyingly found some errors13 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'.
By now there existed yet a third definition of the same sort of idea.
This was the 'recursive function', which was a way of making absolutely precise the notion of defining a mathematical function in terms of other more elementary functions;
Gdel had suggested it, and it had been taken up by Kleene.
This idea, when formalised and extended somewhat, led to the definition of the 'recursive function'.
And now it had turned out that the general recursive function was exactly equivalent to the computable function.
So Church's lambda-calculus, and Gdel's way of defining arithmetical functions, both turned out to be equivalent to the Turing machine.
Gdel himself later acknowledged the Turing machine construction as the most satisfactory definition of a 'mechanical procedure'.