Hacker News Reader

Though still useful to remember that some of the earliest mathematical write ups of the Halting Problem were also by Alonso Church and directly in the lambda calculus. The Church-Turing Theorem is a lasting reminder that the two worlds imperative and functional describe the same algorithms (form the set of Turing Completeness).

View on HN

It depends on the type system you choose to apply to LC. Simply-typed LC terminates.

You have to include a construct that introduces general recursion to make it Turing complete.

There's a cool practical space within those constraints that needs more exploration.

Non-total functions can call total functions, but not vice-versa.

Imagine a web server whose main loop is non-total, because you want it to stay up. But each route is total, to guarantee termination.

Reply on news.ycombinator.com