8 Jan
2007
8 Jan
'07
8:13 a.m.
On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote:
So Terminating contains all the terminating terms in the untyped lambda calculus and none of the non-terminating ones. And the type checker checks this. So it sounds to me like the (terminating) type checker solves the halting problem. Can you please explain which part of this I have misunderstood?
Perhaps you, the user, have to encode the proof of halting in the way you construct the term? Just guessing. Best regards Tomasz