4 ms·

Non-termination, my bad! And of course that's true! Trivially so, though, in that we could do the same by picking the counter to be 10 instead of 2^1000, since

by tel 11y ago

Non-termination, my bad! And of course that's true! Trivially so, though, in that we could do the same by picking the counter to be 10 instead of 2^1000, since we don't appear to care about changing the meaning of the program. If we do, then we have to consider whether we want our equality to distinguish terminating and non-terminating programs. If it does distinguish, then non-terminating ones are impure. Now, what I think you're really asking for is a blurry edge where we consider equality module "reasonable finite observation" in which something different might arise. But in this case you need partial information so we're headed right at CRDTs, propagators, LVars, and all that jazz. I'm not for a single second going to state that there aren't interesting semanticses out there. Although I will say that CRDTs have really nice value semantics with partial information. I think it's a lot nicer than the operational/combining model.

pron 11y ago
> If we do, then we have to consider whether we want our equality to distinguish terminating and non-terminating programs. But this is what bugs me. As someone working on algorithms (and does not care as much about semantics and abstractions), the algorithm's correctness is only slightly more important than its complexity. While there are (pragmatic) reasons to care about proving partial correctness more than total correctness (or prioritizing safety over liveness in algorithmists' terms), it seems funny to me to almost completely sweep complexity -- the mother of all effects, and the one at the very core of computation -- under the rug. Speaking about total functions does us no favors: there is zero difference between a program that never terminates, and one that terminates one nanosecond "after" the end of the physical universe. Semantic proof of termination, then, cannot give us any more useful information than no such proof. Just restricting our computational model from TM to total-FP doesn't restrict it in any useful way at all! Moreover, in practical terms, there is also almost no difference (for nearly all programs) between a program that never terminates and one that terminates after a year. Again, I fully understand that there are pragmatic reasons to do that (concentrate on safety rather than liveness), but pretending that there is a theoretical justification to ignore complexity -- possibly the most important concept in computation -- in the name of "mathematics" (rather than pragmatism) just boggles my mind. The entire notion of purity is the leakiest of all abstractions (hyperbole; there are other abstractions just as leaky or possibly leakier). But we've swayed waaaay off course of this discussion (entirely my fault), and I'm just venting :)
- tel 11y ago
  I don't think at all that "value semantics" without any mention of complexity is an end in and of itself. Any sensible programmer will either (a) intentionally decide that performance is minimally important at the moment (and hopefully later benchmark) or (b) concern themselves also with a semantic model which admits a cost model. Or, to unpack that last statement, simulate the machine instructions. I'm never one to argue that a single semantic model should rule them all. Things are wonderful then multiple semantic models can be used in tandem. But while I'd like to argue for the value of cost models, at this point I'd like to also fight for the value-based ones. Totality is important not because it has a practical effect. I vehemently agree with how you are arguing here to that end. It's instead important because in formal systems which ignore it you completely lose the notion of time. Inclusion of non-termination and handling for it admits that there is at least one way which we are absolutely unjustified in ignoring the passage of time: if we accidentally write something that literally will never finish. It is absolutely a shallow way of viewing things. You're absolutely right to say that practical termination is more important that black-and-white non-termination. But that's why it's brought up. It's a criticism of certain value-based models: you guys can't even talk about termination! And then it's also brought up because the naive way of adding it to a theorem prover makes your logic degenerate.
  - pron 11y ago
    > And then it's also brought up because the naive way of adding it to a theorem prover makes your logic degenerate. Well, I'd argue that disallowing non-termination in your logic doesn't help in the least[1], so you may as well allow it. :) But we already discussed in the past (I think) the equivalence classes of value-based models, and I think we're in general agreement (more or less). [1]: There are still infinitely many different ways to satisfy the type a -> a (loop once and return x, loop twice, etc. all of them total functions), and allowing (and equating) all of them loses the notion of time just as completely as disallowing just one of them, their limit (I see no justification for assuming a "discontinuity" at the limit).
    - tel 11y ago

by tel 11y ago

pron 11y ago

> If we do, then we have to consider whether we want our equality to distinguish terminating and non-terminating programs. But this is what bugs me. As someone working on algorithms (and does not care as much about semantics and abstractions), the algorithm's correctness is only slightly more important than its complexity. While there are (pragmatic) reasons to care about proving partial correctness more than total correctness (or prioritizing safety over liveness in algorithmists' terms), it seems funny to me to almost completely sweep complexity -- the mother of all effects, and the one at the very core of computation -- under the rug. Speaking about total functions does us no favors: there is zero difference between a program that never terminates, and one that terminates one nanosecond "after" the end of the physical universe. Semantic proof of termination, then, cannot give us any more useful information than no such proof. Just restricting our computational model from TM to total-FP doesn't restrict it in any useful way at all! Moreover, in practical terms, there is also almost no difference (for nearly all programs) between a program that never terminates and one that terminates after a year. Again, I fully understand that there are pragmatic reasons to do that (concentrate on safety rather than liveness), but pretending that there is a theoretical justification to ignore complexity -- possibly the most important concept in computation -- in the name of "mathematics" (rather than pragmatism) just boggles my mind. The entire notion of purity is the leakiest of all abstractions (hyperbole; there are other abstractions just as leaky or possibly leakier). But we've swayed waaaay off course of this discussion (entirely my fault), and I'm just venting :)

tel 11y ago
I don't think at all that "value semantics" without any mention of complexity is an end in and of itself. Any sensible programmer will either (a) intentionally decide that performance is minimally important at the moment (and hopefully later benchmark) or (b) concern themselves also with a semantic model which admits a cost model. Or, to unpack that last statement, simulate the machine instructions. I'm never one to argue that a single semantic model should rule them all. Things are wonderful then multiple semantic models can be used in tandem. But while I'd like to argue for the value of cost models, at this point I'd like to also fight for the value-based ones. Totality is important not because it has a practical effect. I vehemently agree with how you are arguing here to that end. It's instead important because in formal systems which ignore it you completely lose the notion of time. Inclusion of non-termination and handling for it admits that there is at least one way which we are absolutely unjustified in ignoring the passage of time: if we accidentally write something that literally will never finish. It is absolutely a shallow way of viewing things. You're absolutely right to say that practical termination is more important that black-and-white non-termination. But that's why it's brought up. It's a criticism of certain value-based models: you guys can't even talk about termination! And then it's also brought up because the naive way of adding it to a theorem prover makes your logic degenerate.
- pron 11y ago
  > And then it's also brought up because the naive way of adding it to a theorem prover makes your logic degenerate. Well, I'd argue that disallowing non-termination in your logic doesn't help in the least[1], so you may as well allow it. :) But we already discussed in the past (I think) the equivalence classes of value-based models, and I think we're in general agreement (more or less). [1]: There are still infinitely many different ways to satisfy the type a -> a (loop once and return x, loop twice, etc. all of them total functions), and allowing (and equating) all of them loses the notion of time just as completely as disallowing just one of them, their limit (I see no justification for assuming a "discontinuity" at the limit).
  - tel 11y ago