4 ms·

How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.

by zopa 7y ago

pron 7y ago
It would terminate with an exception.
- ernst_klim 7y ago
  Hence diverge, aka not terminates. You've even stated this yourself: > But now I claim that their composition `foo bar` never crashes (on `head`) It does, because foo does.
  - pron 7y ago
    > Hence diverge, aka not terminates. By focusing on FP nomenclature (whether an exception is regarded as "divergence" or not depends on your language -- note that I said "terminates"; the point is that the trace for each execution is finite) you're missing the issue, that exists regardless of language. > It does, because foo does. `foo bar` never crashes (unless I made some silly bug).
    - pera 7y ago
      Now I'm genuinely confused: do you consider a program that diverge (as in reaches some exceptional state) not as a "crash" but as a form of termination? If so then I don't understand what your original point was; if you could prove that both functions always return some value then you can also say that composing them will always return some value.
      - pron 7y ago
        > diverge (as in reaches some exceptional state) The term "diverge," when applied to an exception, is not a computational term but a term from a specific formalism (e.g.: Haskell). A computation is a sequence of states; if it ever reaches a terminal state (i.e., a state from which it cannot exit), it is said to terminate. You can apply the terms converge/diverge to termination/non-termination, but once you speak of exceptions, you're using a language-specific terminology. > if you could prove that both functions always return some value then you can also say that composing them will always return some value Yes, but that would be too hard. `foo` doesn't always return a value, but `foo bar` does. What can you prove about `foo` and `bar` separately that would make proving that easier, not harder?
      - 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

How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.

by zopa 7y ago

How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.

pron 7y ago

It would terminate with an exception.

ernst_klim 7y ago
Hence diverge, aka not terminates. You've even stated this yourself: > But now I claim that their composition `foo bar` never crashes (on `head`) It does, because foo does.
- pron 7y ago
  > Hence diverge, aka not terminates. By focusing on FP nomenclature (whether an exception is regarded as "divergence" or not depends on your language -- note that I said "terminates"; the point is that the trace for each execution is finite) you're missing the issue, that exists regardless of language. > It does, because foo does. `foo bar` never crashes (unless I made some silly bug).
  - pera 7y ago
    Now I'm genuinely confused: do you consider a program that diverge (as in reaches some exceptional state) not as a "crash" but as a form of termination? If so then I don't understand what your original point was; if you could prove that both functions always return some value then you can also say that composing them will always return some value.
    - pron 7y ago
      > diverge (as in reaches some exceptional state) The term "diverge," when applied to an exception, is not a computational term but a term from a specific formalism (e.g.: Haskell). A computation is a sequence of states; if it ever reaches a terminal state (i.e., a state from which it cannot exit), it is said to terminate. You can apply the terms converge/diverge to termination/non-termination, but once you speak of exceptions, you're using a language-specific terminology. > if you could prove that both functions always return some value then you can also say that composing them will always return some value Yes, but that would be too hard. `foo` doesn't always return a value, but `foo bar` does. What can you prove about `foo` and `bar` separately that would make proving that easier, not harder?
    - 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