Hmm I wonder if that loop example can be rehabilitated. If we interpret it, not as a description of how to evaluate loop, but rather as a constraint on loop. Then we see that the statement is simply a non-condition on loop.
This would mean that non-termination is not a property of the function, but of the compiler/runtime, in that they failed to notice that loop was a partial function called with an input value for which it was not defined!
Comments
Hmm I wonder if that loop example can be rehabilitated. If we interpret it, not as a description of how to evaluate loop, but rather as a constraint on loop. Then we see that the statement is simply a non-condition on loop.
This would mean that non-termination is not a property of the function, but of the compiler/runtime, in that they failed to notice that loop was a partial function called with an input value for which it was not defined!
That's probably possibly in this particular case but it sounds a lot like you're heading toward Halting Problem territory here :)