AFAICS you are fundamentally confused which is causing this mess. This is a good example:
> Imagine that the decider could terminate with, Yes, No, or Error.
That's just not how it works. Mathematically a function, if it terminated, terminates with an answer. There is no error - the precondition of the function states what is acceptable and the function must come back with an answer (or possibly not terminate, but that's another thing). That's why the quote from Stephen Kleene[0] didn't mention errors.
If I want to define a function computing real-number square root, I set as a precondition that negative numbers must never be passed to it. That's it. That's the precondition - "this and only this is acceptable to this bit of code" is what it means.
In any language an exception should happen if you violate that ie. pass in a negative number. That may show up as an exception. But you don't want exceptions! Which is why you try to formally guarantee the precondition is met! So You are guaranteed of an answer (leaving aside non-termination).
All this formal stuff (at least in my world) is about verifying the code conforms to the precondition such that an error will never occur (edit: wrong, it's more than verifying to the precondition but go with it for now) . Also verifying that if the precondition is verified that termination will happen.
Put another way, taking the head of an empty list is meaningless, so you set the precondition (edit: of the function hd())to be that always
is_not_empty(lst)
yes, you may get an exception unless verified. But if you can prove that at the point of call lst is never empty then hd() will guarantee never to except.
If any program was entirely verified thus then no exceptions would be needed because the program would be correct (excluding resource exhaustion on our regrettably finite computers).
> Termination and decision are not the same thing.
Mathematically if it terminates, it decides. If it decided then it has terminated. Yes they are the same thing. That's what the quote says. Termination via exception is not in that world: "in such manner that from the outcome we can read a definite answer". Blowing up without deciding would mean termination (an exception in your terms) without providing yes/no. Useless.
I'm pretty weak in this area but I do know the basics, and it does not come across that you do.
> OMG, I linked to that one...
No probs, I edited out that.
[0] Heh, same kleene after whom was named the kleene star in regexes. Who know.
> Mathematically a function, if it terminated, terminates with an answer.
There is no such thing for a mathematical function to "terminate." In classical mathematics, a function is a one-valued relation, a set of pairs, if you like. There is no algorithm and no computation involved. Termination is a computation term. Divergence is a formalism-specific.
> Imagine that the decider could terminate with, Yes, No, or Error.
That's just not how it works. Mathematically a function, if it terminated, terminates with an answer. There is no error - the precondition of the function states what is acceptable and the function must come back with an answer (or possibly not terminate, but that's another thing). That's why the quote from Stephen Kleene[0] didn't mention errors.
If I want to define a function computing real-number square root, I set as a precondition that negative numbers must never be passed to it. That's it. That's the precondition - "this and only this is acceptable to this bit of code" is what it means.
In any language an exception should happen if you violate that ie. pass in a negative number. That may show up as an exception. But you don't want exceptions! Which is why you try to formally guarantee the precondition is met! So You are guaranteed of an answer (leaving aside non-termination).
All this formal stuff (at least in my world) is about verifying the code conforms to the precondition such that an error will never occur (edit: wrong, it's more than verifying to the precondition but go with it for now) . Also verifying that if the precondition is verified that termination will happen.
Put another way, taking the head of an empty list is meaningless, so you set the precondition (edit: of the function hd())to be that always
yes, you may get an exception unless verified. But if you can prove that at the point of call lst is never empty then hd() will guarantee never to except.If any program was entirely verified thus then no exceptions would be needed because the program would be correct (excluding resource exhaustion on our regrettably finite computers).
> Termination and decision are not the same thing.
Mathematically if it terminates, it decides. If it decided then it has terminated. Yes they are the same thing. That's what the quote says. Termination via exception is not in that world: "in such manner that from the outcome we can read a definite answer". Blowing up without deciding would mean termination (an exception in your terms) without providing yes/no. Useless.
I'm pretty weak in this area but I do know the basics, and it does not come across that you do.
> OMG, I linked to that one...
No probs, I edited out that.
[0] Heh, same kleene after whom was named the kleene star in regexes. Who know.