Logs: liberachat/#haskell
| 2026-01-15 22:31:25 | <lambdabot> | cjeris says: vincenz: no, on a 286 GHC feels warm, like a little fire you can warm your hands at. wait, that smells funny. wait, that was my CPU. |
| 2026-01-15 22:31:26 | <monochrom> | Now consider that this tree happens to be my proof tree. So node = theorem. Period. |
| 2026-01-15 22:31:27 | <EvanR> | no reason everything needs to fit into the same tree |
| 2026-01-15 22:31:44 | <monochrom> | Oh the root node is also called "axiom". Sure. Whatever. |
| 2026-01-15 22:31:59 | <jreicher> | dolio: what do you mean when you say that uncountability comes "naturally" from "constructive" mathematics? (I'm probably paraphasing badly, and I'm not disagreeing; I'm just trying to understand your idea) |
| 2026-01-15 22:32:03 | <monochrom> | Sure. s/tree/forest/ ? |
| 2026-01-15 22:32:48 | <monochrom> | Wait, you can run GHC on a 286?! |
| 2026-01-15 22:32:49 | <EvanR> | everything is in the same forest... as a tree of 1 node... back to the penchant for containerization |
| 2026-01-15 22:33:18 | <EvanR> | in lambda MOO luckily nodes aren't all required to be in one tree, or even in any tree |
| 2026-01-15 22:33:35 | <int-e> | monochrom: emulators are a thing you know ;-) |
| 2026-01-15 22:33:58 | <dolio> | jreicher: Cantor's diagonal argument is constructive. It's basically what I linked. Given `enum : ℕ → (ℕ → 2)`, one can construct a `ℕ → 2` that is not in the image of `enum`. |
| 2026-01-15 22:34:05 | <monochrom> | Wait, does that you use a 286 to emulate a 386 then run GHC there? |
| 2026-01-15 22:34:15 | <monochrom> | s/does that you/does that mean/ |
| 2026-01-15 22:34:19 | <jreicher> | OK. But what about the set he's diagonlising? |
| 2026-01-15 22:34:36 | <int-e> | monochrom: I don't know. I'm filling in my own details here :P |
| 2026-01-15 22:34:42 | <monochrom> | Heh |
| 2026-01-15 22:35:12 | <EvanR> | "wavfunction collapse procedural generation" of anecdotes xD |
| 2026-01-15 22:35:22 | <dolio> | jreicher: I don't understand the question. |
| 2026-01-15 22:35:24 | <monochrom> | Because AFAIK GHC assumes a flat/linear 32-bit addressing model i.e. at least 386. |
| 2026-01-15 22:35:43 | <jreicher> | dolio: I think you're presupposing that the set of reals is "constructive". No? |
| 2026-01-15 22:35:44 | <int-e> | I don't know that there never was a 16 bit version of GHC. |
| 2026-01-15 22:35:56 | <EvanR> | who ordered reals |
| 2026-01-15 22:36:03 | <int-e> | (It does seem rather unlikely though.) |
| 2026-01-15 22:36:12 | <monochrom> | OK OK April's Fool project: Drastically overhaul GHC to be runnable on 286's segment model! |
| 2026-01-15 22:36:18 | <dolio> | Reals are too complicated to get into. This is just the bit streams. |
| 2026-01-15 22:36:32 | <jreicher> | If you have infinite bitstreams, you have all the reals |
| 2026-01-15 22:36:33 | <int-e> | monochrom: protected mode or real mode? |
| 2026-01-15 22:36:36 | <monochrom> | (Oh then it probably also runs on 8088 DOS too...) |
| 2026-01-15 22:36:40 | <jreicher> | Sorry, I should say ALL the infinite bitstreams |
| 2026-01-15 22:36:42 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-01-15 22:36:44 | <dolio> | Reals are a quotient. |
| 2026-01-15 22:36:57 | <jreicher> | Huh? |
| 2026-01-15 22:37:08 | <int-e> | dolio: Don't you like Dedekind cuts? |
| 2026-01-15 22:37:10 | <EvanR> | we're getting off topic trying to jam classical reals into the discussion |
| 2026-01-15 22:37:16 | <EvanR> | which isn't about them |
| 2026-01-15 22:37:28 | <int-e> | (so *now* we're getting off topic, huh) |
| 2026-01-15 22:37:30 | int-e | runs |
| 2026-01-15 22:37:31 | <dolio> | jreicher: Like 0.11111... = 1.0 (binary). |
| 2026-01-15 22:37:33 | <EvanR> | lol |
| 2026-01-15 22:37:56 | <jreicher> | EvanR: how can you have Cantor's diagonalisation without the reals? |
| 2026-01-15 22:38:01 | <jreicher> | (Maybe I've misunderstood the idea) |
| 2026-01-15 22:38:04 | <EvanR> | yes that is what this whole discussion is about |
| 2026-01-15 22:38:06 | <dolio> | It's actually possible for the (Dedekind) reals to be countable in constructive mathematics. |
| 2026-01-15 22:38:10 | <EvanR> | was cantor even talking about real numbers |
| 2026-01-15 22:38:18 | <dolio> | Even though the bit streams are uncountable. |
| 2026-01-15 22:38:21 | <jreicher> | To begin with I'm pretty sure he was |
| 2026-01-15 22:38:22 | <monochrom> | I think GCC for DOS could do 32-bit in real mode. I forgot. But just do whatever GCC-for-DOS does. |
| 2026-01-15 22:38:42 | <jreicher> | dolio: Ok, I'll stick to bistreams. In what way is a non-computable (infinite) bitstream "constructive"? |
| 2026-01-15 22:38:44 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 22:38:52 | <EvanR> | at that time, it wasn't appreciated the subtleties that binary streams created for defining reals... but a stream of bits is pretty simple |
| 2026-01-15 22:39:04 | <dolio> | They aren't. We only need the computable ones. |
| 2026-01-15 22:40:15 | <jreicher> | And if you only have the computable ones, the set is countable. |
| 2026-01-15 22:40:24 | <dolio> | No, it isn't. |
| 2026-01-15 22:40:45 | <EvanR> | at some point doing the proof might help since this is ... mathematical |
| 2026-01-15 22:40:55 | <jreicher> | "computable" can be understood as "generated by a program", and all program texts are finite. So the set of all program texts is countable, and so is the set of computable outputs |
| 2026-01-15 22:41:00 | <dolio> | Cantor's diagonal argument shows every computable enumeration of the computable bit streams misses a computable bit stream. |
| 2026-01-15 22:41:05 | <EvanR> | a proof is worth 1000 words |
| 2026-01-15 22:41:34 | <EvanR> | jreicher, I went over that in a few ways above |
| 2026-01-15 22:42:03 | tomsmeding | . o O ( every _computable_ enumeration -- that bit is relevant here ) |
| 2026-01-15 22:42:08 | <dolio> | Yeah. |
| 2026-01-15 22:42:28 | <dolio> | If you want to say there's a non-computable enumeration, you have again exited constructive mathematics. |
| 2026-01-15 22:42:34 | <tomsmeding> | this is not classical set-theoretical "countable", this is "computably countable" |
| 2026-01-15 22:42:51 | <int-e> | tomsmeding: But the only reason we are in this mess is that we pretend that "everything" is computable. As I said earlier, you need to be very clear about object and meta levels for this discussion to be meaningful. |
| 2026-01-15 22:42:59 | <EvanR> | another way to say that, already said, Bitstream is uncountable (in haskell). (Assuming a lot about what kind of haskell you are allowed to write) |
| 2026-01-15 22:43:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-15 22:43:25 | <tomsmeding> | int-e: right -- I haven't really been following the discussion. You know what, I'll leave you at it :) |
| 2026-01-15 22:43:50 | <int-e> | tomsmeding: Ah sorry, I'm not complaining! |
| 2026-01-15 22:43:53 | <EvanR> | if I hook up my Bitstream generator to an external entity then it only makes matters worse |
| 2026-01-15 22:44:02 | <EvanR> | we're not going to get less bitstreams that way |
| 2026-01-15 22:44:08 | <jreicher> | dolio: You're saying that because the set of computable numbers is not itself computably enumrable, that it's "constructively" uncountable? Something like that? |
| 2026-01-15 22:44:27 | <int-e> | tomsmeding: It's in the nature of IRC that discussions become circular, for better or worse. |
| 2026-01-15 22:44:33 | <tomsmeding> | :D |
| 2026-01-15 22:45:09 | <dolio> | jreicher: Something like that. Maybe it's backwards. The constructive proof of its uncountability 'means' that the computable bit streams are not computably enumerable. |
| 2026-01-15 22:45:22 | <dolio> | Because constructive mathematics is valid for computability. |
| 2026-01-15 22:45:26 | <EvanR> | whatever the proof means, the proof goes through |
| 2026-01-15 22:45:30 | <EvanR> | it's valid in of itself |
| 2026-01-15 22:45:31 | <jreicher> | I don't really understand why that serves as a meanginful notion of uncountability |
| 2026-01-15 22:45:33 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-01-15 22:45:49 | <EvanR> | jreicher, you're working on the level of vibes it seems... instead of defining stuff, then proof a theorem |
| 2026-01-15 22:46:16 | <jreicher> | At the moment I'm just trying to understand dolio's definitions |
| 2026-01-15 22:46:17 | <EvanR> | for whatever reason you don't like the result, even though it jives exactly with classical math xD |
| 2026-01-15 22:46:32 | <EvanR> | instead yeah lets understand it on its own terms |
| 2026-01-15 22:46:37 | <dolio> | The reason the 'program text' thing won't work is that the computable bit streams are (at best) a quotient of program texts. So being able to enumerate program texts won't help you enumerate all the bit streams. |
| 2026-01-15 22:46:38 | <jreicher> | I know what the definitions and theorems are in classical maths. I don't have a problem with any of that. |
| 2026-01-15 22:47:16 | <jreicher> | dolio: but why is enumeration important here at all? What's the connection with uncountability, for you? |
| 2026-01-15 22:47:29 | jmcantrell_ | is now known as jmcantrell |
| 2026-01-15 22:47:29 | <jreicher> | Sorry, I mean computable enumeration |
| 2026-01-15 22:47:45 | <dolio> | Countability is 'there is a surjection from ℕ'. |
| 2026-01-15 22:47:50 | <EvanR> | Bitstream is uncountable (in haskell) <- |
| 2026-01-15 22:48:12 | <dolio> | (Or similar) |
| 2026-01-15 22:48:26 | <int-e> | if you dislike "countability" you can say that recursive functions are not recursively enumerable ;-) |
| 2026-01-15 22:48:29 | <dolio> | And I don't believe in uncomputable things. So the surjection is computable. |
| 2026-01-15 22:48:41 | <jreicher> | Oh. I haven't heard that view before. |
| 2026-01-15 22:48:43 | → | mange joins (~mange@user/mange) |
| 2026-01-15 22:48:58 | <EvanR> | which definition are you having issues with again |
| 2026-01-15 22:49:05 | <dolio> | That is the premise, at least. We are in the world where everything is inherently computable. |
| 2026-01-15 22:49:18 | <jreicher> | So you don't believe something like Chaitin's omega exists? |
| 2026-01-15 22:49:29 | × | michalz quits (~michalz@185.246.207.205) (Remote host closed the connection) |
| 2026-01-15 22:49:33 | <EvanR> | you said you weren't a platonist! |
| 2026-01-15 22:49:47 | <dolio> | It's not a real number, at least. |
All times are in UTC.