The very notions of a "partial function" and a "normal form" are language-dependent. And yes, certainly in those languages, throwing an exception is called divergence. But partial functions are not an essential concept of computation. A computation can terminate or not, and the name divergence in that context applies to that. In any event, I was careful to speak of termination, the computational concept, rather than divergence, which can have a formalism-specific meaning.
Such terms are certainly used in that sense by PLs eg in scala Function and PartialFunction types exist with those intended semantics, and it seems haskell recognises the terminology https://wiki.haskell.org/Partial_functions (though whether it supports them in the language definition or libraries I don't know).
> Partial function is a standard mathematical term, not a programming language (PL) one
Like many things in mathematics, the term has been borrowed and changed. Look, for example at "function". Do you think "function" in programming (even in Haskell) means the exact same thing as in mathematics?
In general, partial functions mean that for some values, a function is undefined. But in a PL nothing is undefined. In some cases there would be an exception; in others the subroutine would loop forever. But a language like Haskell, because it wants its "functions" to resemble mathematical functions, declares that those perfectly normal computational behaviors correspond to "undefined". In imperative languages, where subroutines don't try to correspond to (partial) functions, throwing an exception does not correspond to undefined.
@pron then makes an apparently incorrect claim which I dispute to try to help clarify. That's clarification not nitpicking (I intended that way anyway). @pron's point may be valid but if we don't have common meanings to words, this will go nowhere.
The confusion is about a word that I didn't use. I said that both subroutines "terminate". That is a word with a precise meaning in computation -- every possible trace is finite. Someone started arguing about whether or not they "diverge", and I said that that's language-dependent (https://news.ycombinator.com/item?id=20723623). Both foo and bar always terminate, and that is both precise and a common meaning.
> The confusion is about a word that I didn't use.
which word?
> I said that both subroutines "terminate". That is a word with a precise meaning in computation
I'd say so. But here's a clip from previous:
> zopa 23 hours ago :- How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.
-and you say-
> pron 23 hours ago :- It would terminate with an exception.
So you're claiming that 'terminating with an exception' is termination "with a precise meaning in computation". But that's a bloody strange definition I have never come across.
In fact it's so weird I had trouble finding a definition because it seems so fundamentally bizarre that nobody I've ever met has ever considered throwing an exception (or similar) due to precondition violation to be termination. But here goes:
1943: In a paper, Stephen Kleene states that "In setting up a complete algorithmic theory, what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer, 'Yes' or 'No,' to the question, 'Is the predicate value true?'."
> But that's a bloody strange definition I have never come across.
I don't know what else I can say. Exceptions are not a computational concept, they're a language concept. The computation terminates in some well-defined state. That the language declares that that well-defined state is not considered a value is a language-specific thing.
> So yes termination is defined and no it's not what you claim it is.
It is exactly what I defined, as your quote shows. Termination and decision are not the same thing. Imagine that the decider could terminate with, Yes, No, or Error. It would still not be a decision procedure, but it is very much termination. And your very quote says exactly that when it says "terminates and in such manner that..."? If termination already means that it is in such manner, why is the qualification necessary?
Your definition of termination (to mean anything other than reaching a terminal state after a finite number of steps) is based on the fact that in a particular formalism, the lambda calculus, termination yields a normal form. Now, the lambda calculus doesn't have exceptions, and so every lambda term either reduces to a normal form or the reduction never terminates, but a language like Haskell adds a third possibility. Because Haskell draws inspiration from the lambda calculus, it's easier, in the discussion of Haskell, to map exceptions -- which don't yield a normal form but do terminate at a definite computational state -- to the same notion of divergence, that, in the lambda calculus, is synonymous with termination, but in Haskell it isn't. So I wouldn't be surprised if some people took it further, and used termination to be synonymous with "produces a normal form" in Haskell. But, again, this is not how the notion of termination is commonly defined in computation (many notions of computations don't even have the concept of a normal form or of a value). In Java, for example, where the denotation of a subroutine isn't similar to a partial function but is, rather, a predicate transformer, an exception and a return value are equally valid results.
But yeah, I agree that selling Haskell as maths, does tend to confuse, and so people can mistakenly think that Haskell terminology is canonical mathematical or computer-science terminology. And yeah, it is sometimes frustrating to speak with those who are only familiar with the mathematics of functional programming and not with the mathematics of imperative programming, or with the theory of computation in general, and so don't even know which terms are overloaded and which are canonical.
All of this, however, is so irrelevant to the point of my `foo bar` example (namely, that knowing things about components does not mean you can feasibly know things about their composition) that it's ridiculous.
> Yep, and that reply was posted 10 minutes before you referred to it.
So not only are you determined to focus on something that is entirely beside the point because you've completely missed the point, you are also wrong in the side-track you've chosen.
I believe these terms (including "exceptional state", but no "exception") are commonly used in formal languages, combinatorics, rewriting systems, mathematical logic and so. They are also used in Haskell because this was partially based on System F, which comes from the simply typed lambda calculus. I understand your frustration and please believe me that it was not my intention to turn this thread into a pedantic show.
But now coming back to your original point and example: I don't think anyone from the Haskell and ML-family languages camp is claiming one can automatically deduce every possible decidable property from any function with their type system, or at least not yet :)
Yes, they are commonly used in formal languages, and their precise meaning is language dependent, which is why I didn't use partial or divergence but termination, which has a unique computational meaning.
I don't think anyone claims that any property can be proven. I do think that some think that if a program can be decomposed into simple parts, whose "interesting" properties are provable in isolation, then you can feasibly prove interesting properties of their composition, which is not true. A proof of that was only given in the past 10-15 years, and is referenced in my post.
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.
