Alan Turing in America
medium.com
medium.com
> Turing’s approach to the problem would be the solution that has endured, likely due to Church’s solution’s reliance on his so-called λ-calculus
So-called λ-calculus? Isn't that rather dismissive of λ-calculus. λ-calculus contributed not only to mathematics/computer science, but also, logic, linguistics, etc. Not to mention its practical contributions in many programming languages. And as long as the Church-Turing theorem endures, church's so-called λ-calculus will endure as well.
Interesting article nonetheless. I wonder if Turing's correspondences are available to the public online?
https://www.merriam-webster.com/dictionary/so-called
> 1: commonly named
> the so-called pocket veto
True, but it didn't actually show what Church had wanted to show in 1936 about what later became known as computability. First, it should be clear that after Gödel's incompleteness results, it was all but certain that arithmetics was undecidable. The problem with showing that, however, was defining what a "decision procedure", or an algorithm, is. Church's approach, essentially defining it as "anything that could be expressed as a lambda expression" suffered from serious difficulties, inherent to all languages (until Turing, all discussions of computation rested on formal languages with some inference calculus), which is that the computational power of a language rests on arbitrary axioms. One could easily define a second-order lambda calculus that has an axiomatic term, H, that axiomatically reduces to whether its argument is normalizable or not, provided that it does not contain H itself. Why, then, should we choose the "first-order" lambda calculus as the definition of computation rather than the second-, third- or fourth-order?
Church does a decent job explaining why "calculability" (computability) is no weaker than his lambda calculus, but his explanation for why it can't be stronger -- which is the more important point -- is poor. Church himself admits as much when he realizes his definition relies on some circularity -- as we now know, a calculus is computable iff each of its derivations are computable (which wouldn't be true for the "second-order" lambda calculus), but how can we tell that if we wish to define computability using the calculus itself? So he waves his hands a bit and then writes: [1]
> If this interpretation or some similar one is not allowed, it is difficult to see how the notion of an algorithm can be given any exact meaning at all.
Turing did just that. He was able to define computation in an absolute way, one that does not depend on any language or arbitrary axioms (just physical observation). As Gödel said: [2]
> [W]ith this concept one has for the first time succeeded in giving an absolute definition of an interesting epistemological notion, i.e., one not depending on the formalism chosen. In all other cases treated previously, such as demonstrability or [lambda] definability, one has been able to define them only relative to a given language, and for each individual language it is clear that the one thus obtained is not the one looked for. For the concept of [Turing] computability, however, although it is merely a special kind of demonstrability or decidability, the situation is different. By a kind of miracle it is not necessary to distinguish orders, and the diagonal procedure does not lead outside the defined notion.
Unlike any language, Turing's treatment has no "orders." One could, of course -- as Turing has done -- imagine a Turing machine with an oracle, but it is clear that the oracle cannot itself be a machine, while a "second-order" lambda calculus is just another language, no more or less arbitrary than the "first-order" one. The problem, then, was to define what computation was, and Turing was the first to succeed.
[1]: An Unsolvable Problem of Elementary Number Theory, footnote 19
[2]: Remarks before the Princeton bicentennial conference on problems in mathematics, 1942, in Collected Works, Vol II
There's an article somewhere about how EU bureaucrats mis-understood what 'co-called' means idiomatically and started to put it in lots of documents just meaning innocently 'that is called' and how they caused offence.
That's probably what's happening here - the author doesn't know idiomatic English.
The section on the misuse of 'so-called' is on page 54.
I feel like this sort of thing happens in a large number of places I've been to. People in some professions think, "oh, here is an out of towner, I will charge them a little more." By no means restricted to New York or the United States.
I read somewhere opposite, I do not remember source.
At that time he was forced to take strong medication and had his security clearance removed. He could only continue his work at US, but he was not allowed to immigrate due to criminal charges.