Newest at the top
| 2026-06-23 23:41:07 +0000 | <dolio> | That is the 'productive' part of totality. |
| 2026-06-23 23:40:38 +0000 | <dolio> | Like, 'non-termination' is fine if your witness of the infinitude of primes is a stream of distinct prime numbers, as long as there's no point in the stream where it goes, "hold on a second," and then never comes back. |
| 2026-06-23 23:38:54 +0000 | <EvanR> | a term which can be used at any type |
| 2026-06-23 23:38:39 +0000 | <dolio> | That was my point. |
| 2026-06-23 23:38:32 +0000 | <dolio> | Not really non-termination, I guess, depending on what you mean. |
| 2026-06-23 23:37:16 +0000 | <dolio> | Non-termination allows vacuous proofs of false things, usually. |
| 2026-06-23 23:37:04 +0000 | <EvanR> | something on top of that would need to identify that you're talking about a turing machine |
| 2026-06-23 23:36:37 +0000 | <EvanR> | base haskell being not particularly expressive as a logic, you basically proved some stream exists |
| 2026-06-23 23:36:23 +0000 | <jreicher> | And how does that relate to termination? |
| 2026-06-23 23:35:58 +0000 | <dolio> | The type is what is being proved. |
| 2026-06-23 23:35:35 +0000 | <jreicher> | dolio: the analogy is not straightforward. You still have to be clear what is being proven by the program you are taking as a proof |
| 2026-06-23 23:35:01 +0000 | <dolio> | The connection is that proofs are analogous to Haskell programs, but saying that the text of a Haskell program is finite doesn't really tell you whether it stops or not, and some Haskell programs are not 'supposed' to stop, depending on what you mean by that. |
| 2026-06-23 23:33:52 +0000 | czan | (~czan@user/mange) czan |
| 2026-06-23 23:33:51 +0000 | <EvanR> | presumably, for this case |
| 2026-06-23 23:33:26 +0000 | <EvanR> | each WHNF step terminates |
| 2026-06-23 23:32:18 +0000 | <EvanR> | yeah the proof would be the program in this case, not the semantics value (the infinite stream) |
| 2026-06-23 23:31:02 +0000 | <jreicher> | How does that relate to what we're talking about? |
| 2026-06-23 23:30:59 +0000 | <dolio> | The ones that don't finish in pathological ways, too. |
| 2026-06-23 23:30:27 +0000 | <dolio> | All Haskell programs are finite, including the ones that don't finish. |
| 2026-06-23 23:30:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-06-23 23:29:54 +0000 | <jreicher> | "Good" theorem prover. :p |
| 2026-06-23 23:29:40 +0000 | <EvanR> | if you carefully walk the space of sentences |
| 2026-06-23 23:29:20 +0000 | <jreicher> | So a theorem prover will always terminate if a proof exists. |
| 2026-06-23 23:29:12 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 246 seconds) |
| 2026-06-23 23:29:04 +0000 | <jreicher> | dolio: exactly. And that's the proof. |
| 2026-06-23 23:28:52 +0000 | <EvanR> | this program would need to be verfified |
| 2026-06-23 23:28:41 +0000 | <dolio> | Everything you write on a page is described finitely. |
| 2026-06-23 23:28:30 +0000 | <EvanR> | yeah you'd need a valid program which constructs the turing machine's stream, without failing to pick a next move |
| 2026-06-23 23:28:28 +0000 | <dolio> | Yeah, it's an infinite stream described in a finite way. |
| 2026-06-23 23:27:27 +0000 | <dolio> | Like `data Stream a = Cons a (Stream a)` |
| 2026-06-23 23:27:22 +0000 | <jreicher> | dolio: I don't think what you've said makes sense. How do you know the Turing machine is going to have an infinite sequence of steps unless you can demonstrate that with a FINITE set of SENTENCES? |
| 2026-06-23 23:27:18 +0000 | <EvanR> | if you have a meta proof of that, then great |
| 2026-06-23 23:27:07 +0000 | <dolio> | Well, it's infinite by construction. |
| 2026-06-23 23:27:05 +0000 | <EvanR> | is another issue |
| 2026-06-23 23:26:54 +0000 | <EvanR> | there would be no way to run that proof and observe the fact that it's infinite |
| 2026-06-23 23:26:06 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 23:24:42 +0000 | <EvanR> | making it logically pointless |
| 2026-06-23 23:24:26 +0000 | <EvanR> | if proofs = programs, then freezing up programs can prove anything |
| 2026-06-23 23:24:23 +0000 | <dolio> | A proof that a Turing machine diverges is an infinite sequence of steps. |
| 2026-06-23 23:24:01 +0000 | <dolio> | Proofs don't need to 'terminate.' |
| 2026-06-23 23:23:50 +0000 | <jreicher> | I would venture to say most programmers aren't writing theorem provers. |
| 2026-06-23 23:23:31 +0000 | <jreicher> | A theorem prover is a very particular kind of program with very particular requirements. That explains the "want" in THAT case. |
| 2026-06-23 23:21:28 +0000 | <EvanR> | so you might ask why do we want proofs to terminate and confuse some people |
| 2026-06-23 23:20:55 +0000 | <EvanR> | so a vast subset of general programming |
| 2026-06-23 23:20:48 +0000 | <EvanR> | also I think the whole total thing really came out of theorem proving where proofs take the form of definitely terminating computations |
| 2026-06-23 23:20:06 +0000 | Digitteknohippie | Digit |
| 2026-06-23 23:19:41 +0000 | <EvanR> | or map over finite structure |
| 2026-06-23 23:19:17 +0000 | <EvanR> | but it's surprising how much easier it is to mentally verify when you move from e.g. explicit for loops to foreach over a (finite) array |
| 2026-06-23 23:18:28 +0000 | <dolio> | Lots of Haskell tricks are fine, but not allowed in any straight forward way. |
| 2026-06-23 23:18:22 +0000 | <EvanR> | many algorithms are total but the compiler can't just look at it and verify |