3 ms·
The author says that simply typed lambda calculus proves that programs terminate. That sounds to me like saying "simply typed lambda calculus is not Turing-comp
by aufreak 17y ago
The author says that simply typed lambda calculus proves that programs terminate. That sounds to me like saying "simply typed lambda calculus is not Turing-complete". Disclaimer: I know basics of lambda calculus but don't exactly know what the "simply typed" one is.
- camccann 17y agoYou are correct, it's not. In the simply-typed lambda calculus, generally recursive constructs (such as fixed-point combinators like our friend Y) do not have valid types and are not legal. Wikipedia has a nice article on it: http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus