4 ms·
[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
by 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.