5 ms·

@pron: I'm not an expert in rewriting systems and type theory, but in the literature I have studied a partial function is said to diverge when it's applied to s

by pera 7y ago

@pron: I'm not an expert in rewriting systems and type theory, but in the literature I have studied a partial function is said to diverge when it's applied to some particular value that won't return / produce a normal form (i.e. non-terminating), either because it will recur ad infinitum or because the applied value doesn't map to the function's codomain. One could argue that in a well typed program the latter shouldn't happen, but then one would require a type system with dependent types to type-check programs with functions like head : [a] -> a :) An exception is just a mechanism that some PLs provide to indicate that the program reached such exceptional state where, for whatever reason, some assumption failed and there is no meaningful reduction to compute.

pron 7y ago
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.
- tempguy9999 7y ago
  Partial function is a standard mathematical term, not a programming language (PL) one: https://en.wikipedia.org/wiki/Partial_function https://en.wikipedia.org/wiki/Partial_function so what you say seems wrong A function that is non-partial is, in standard maths parlance, a total function https://en.wikipedia.org/wiki/Partial_function#Total_function https://en.wikipedia.org/wiki/Partial_function#Total_functio... 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 https://wiki.haskell.org/Partial_functions (though whether it supports them in the language definition or libraries I don't know).
  - tome 7y ago
    Could people please respond to pron's actual point rather than nitpicking terminology? If it helps I've tried to elucidate here: https://news.ycombinator.com/item?id=20722887 https://news.ycombinator.com/item?id=20722887
    - tempguy9999 7y ago
      The point is @pera said in https://news.ycombinator.com/item?id=20717160 https://news.ycombinator.com/item?id=20717160 "Now I'm genuinely confused". That seems to be down to confusion in terminology. @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.
      - pron 7y ago
        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 https://news.ycombinator.com/item?id=20723623). Both foo and bar always terminate, and that is both precise and a common meaning.
        tempguy9999 7y ago
        > 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?'." That from https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem So yes termination is defined and no it's not what you claim it is. No wonder people are getting confused. as for... (edit: deleted this as poster accidentally linked to wrong comment)

by pera 7y ago

pron 7y ago

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.

tempguy9999 7y ago
Partial function is a standard mathematical term, not a programming language (PL) one: https://en.wikipedia.org/wiki/Partial_function https://en.wikipedia.org/wiki/Partial_function so what you say seems wrong A function that is non-partial is, in standard maths parlance, a total function https://en.wikipedia.org/wiki/Partial_function#Total_function https://en.wikipedia.org/wiki/Partial_function#Total_functio... 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 https://wiki.haskell.org/Partial_functions (though whether it supports them in the language definition or libraries I don't know).
- tome 7y ago
  Could people please respond to pron's actual point rather than nitpicking terminology? If it helps I've tried to elucidate here: https://news.ycombinator.com/item?id=20722887 https://news.ycombinator.com/item?id=20722887
  - tempguy9999 7y ago
    The point is @pera said in https://news.ycombinator.com/item?id=20717160 https://news.ycombinator.com/item?id=20717160 "Now I'm genuinely confused". That seems to be down to confusion in terminology. @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.
    - pron 7y ago
      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 https://news.ycombinator.com/item?id=20723623). Both foo and bar always terminate, and that is both precise and a common meaning.
      - tempguy9999 7y ago
        > 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?'." That from https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem So yes termination is defined and no it's not what you claim it is. No wonder people are getting confused. as for... (edit: deleted this as poster accidentally linked to wrong comment)