Re:1931: Kurt Gödel shows limits of math, logic, computing, AI
by ProfHewitt on Monday June 21, 2021 @09:45AM
(#27579095)
[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:
Re:1931: Kurt Gödel shows limits of math, logic, computing, AI
by sn41 on Tuesday June 22, 2021 @08:34AM
(#27590861)
It'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.
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_f...