3 ms·
But I mean, 'run' is a total function and it does halt. When you call 'run' on your non-halting TuringMachine, the language interpreter reduces exactly one call
by cvoss 4y ago
But I mean, 'run' is a total function and it does halt. When you call 'run' on your non-halting TuringMachine, the language interpreter reduces exactly one call to 'step' and then terminates with the result 'Later <an unevaluated expression>'. Further computation only occurs if and when you pump the 'Later ...' value for further terms, and that can happen only finitely many times because repeated pumping can only come from a standard recursion, ultimately, which is terminating.