3 ms·
This is classic Schmidhubris, a mixture of truth and exaggeration. Turing's paper is a landmark, and includes even an equivalence proof of the power of the lam
by sn41 5y ago
This is classic Schmidhubris, a mixture of truth and exaggeration.
Turing's paper is a landmark, and includes even an equivalence proof of the power of the lambda calculus and his universal machine. In doing so, he came up with a fixed-point combinator, an applicative combinator, now called the Turing fixed point combinator [1]. Especially appropriate on a website run by the Y combinator.
Turing's paper should run as a TV ad "But wait, there's more..." Many applications of topology (he argues why the alphabet should be finite, rather than simply saying that it is finite, by using the Bolzano-Weierstrass theorem, essentially), combinatorics, logic, functional programming - when FP was hardly a decade old and largely unknown outside Princeton - and all from an undergraduate course project report!
[1] https://en.wikipedia.org/wiki/Fixed-point_combinator#Other_fixed-point_combinators https://en.wikipedia.org/wiki/Fixed-point_combinator#Other_f...
- P-NP 5y agoI see neither hubris nor exaggeration. Before Turing, it was Church who proved the equivalence of the power of his lambda calculus and Gödel's universal model.
- ProfHewitt 5y ago[Church 1935] proved the computational undecidability of the halting problem before [Turing 1936], which was written up in a hurry after [Church 1935]. The Y-combinator does not work for strongly-typed systems. Instead recursion must be explicitly added as an additional primitive to the lambda calculus. See following for more information: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003
- sn41 5y agoIt's an honor to receive a response from you. I agree on all points, especially the lack of combinators for strongly typed systems. (As I understand it, it is impossible to assign types to such terms.) My main point was that disrespect for Turing's paper is largely unjustified.