Newest at the top
| 2026-01-15 23:42:08 +0100 | <dolio> | Yeah. |
| 2026-01-15 23:42:03 +0100 | tomsmeding | . o O ( every _computable_ enumeration -- that bit is relevant here ) |
| 2026-01-15 23:41:34 +0100 | <EvanR> | jreicher, I went over that in a few ways above |
| 2026-01-15 23:41:05 +0100 | <EvanR> | a proof is worth 1000 words |
| 2026-01-15 23:41:00 +0100 | <dolio> | Cantor's diagonal argument shows every computable enumeration of the computable bit streams misses a computable bit stream. |
| 2026-01-15 23:40:55 +0100 | <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 23:40:45 +0100 | <EvanR> | at some point doing the proof might help since this is ... mathematical |
| 2026-01-15 23:40:24 +0100 | <dolio> | No, it isn't. |
| 2026-01-15 23:40:15 +0100 | <jreicher> | And if you only have the computable ones, the set is countable. |
| 2026-01-15 23:39:04 +0100 | <dolio> | They aren't. We only need the computable ones. |
| 2026-01-15 23:38:52 +0100 | <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 23:38:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:38:42 +0100 | <jreicher> | dolio: Ok, I'll stick to bistreams. In what way is a non-computable (infinite) bitstream "constructive"? |
| 2026-01-15 23:38:22 +0100 | <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 23:38:21 +0100 | <jreicher> | To begin with I'm pretty sure he was |
| 2026-01-15 23:38:18 +0100 | <dolio> | Even though the bit streams are uncountable. |
| 2026-01-15 23:38:10 +0100 | <EvanR> | was cantor even talking about real numbers |
| 2026-01-15 23:38:06 +0100 | <dolio> | It's actually possible for the (Dedekind) reals to be countable in constructive mathematics. |
| 2026-01-15 23:38:04 +0100 | <EvanR> | yes that is what this whole discussion is about |
| 2026-01-15 23:38:01 +0100 | <jreicher> | (Maybe I've misunderstood the idea) |
| 2026-01-15 23:37:56 +0100 | <jreicher> | EvanR: how can you have Cantor's diagonalisation without the reals? |
| 2026-01-15 23:37:33 +0100 | <EvanR> | lol |
| 2026-01-15 23:37:31 +0100 | <dolio> | jreicher: Like 0.11111... = 1.0 (binary). |
| 2026-01-15 23:37:30 +0100 | int-e | runs |
| 2026-01-15 23:37:28 +0100 | <int-e> | (so *now* we're getting off topic, huh) |
| 2026-01-15 23:37:16 +0100 | <EvanR> | which isn't about them |
| 2026-01-15 23:37:10 +0100 | <EvanR> | we're getting off topic trying to jam classical reals into the discussion |
| 2026-01-15 23:37:08 +0100 | <int-e> | dolio: Don't you like Dedekind cuts? |
| 2026-01-15 23:36:57 +0100 | <jreicher> | Huh? |
| 2026-01-15 23:36:44 +0100 | <dolio> | Reals are a quotient. |
| 2026-01-15 23:36:42 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-01-15 23:36:40 +0100 | <jreicher> | Sorry, I should say ALL the infinite bitstreams |
| 2026-01-15 23:36:36 +0100 | <monochrom> | (Oh then it probably also runs on 8088 DOS too...) |
| 2026-01-15 23:36:33 +0100 | <int-e> | monochrom: protected mode or real mode? |
| 2026-01-15 23:36:32 +0100 | <jreicher> | If you have infinite bitstreams, you have all the reals |
| 2026-01-15 23:36:18 +0100 | <dolio> | Reals are too complicated to get into. This is just the bit streams. |
| 2026-01-15 23:36:12 +0100 | <monochrom> | OK OK April's Fool project: Drastically overhaul GHC to be runnable on 286's segment model! |
| 2026-01-15 23:36:03 +0100 | <int-e> | (It does seem rather unlikely though.) |
| 2026-01-15 23:35:56 +0100 | <EvanR> | who ordered reals |
| 2026-01-15 23:35:44 +0100 | <int-e> | I don't know that there never was a 16 bit version of GHC. |
| 2026-01-15 23:35:43 +0100 | <jreicher> | dolio: I think you're presupposing that the set of reals is "constructive". No? |
| 2026-01-15 23:35:24 +0100 | <monochrom> | Because AFAIK GHC assumes a flat/linear 32-bit addressing model i.e. at least 386. |
| 2026-01-15 23:35:22 +0100 | <dolio> | jreicher: I don't understand the question. |
| 2026-01-15 23:35:12 +0100 | <EvanR> | "wavfunction collapse procedural generation" of anecdotes xD |
| 2026-01-15 23:34:42 +0100 | <monochrom> | Heh |
| 2026-01-15 23:34:36 +0100 | <int-e> | monochrom: I don't know. I'm filling in my own details here :P |
| 2026-01-15 23:34:19 +0100 | <jreicher> | OK. But what about the set he's diagonlising? |
| 2026-01-15 23:34:15 +0100 | <monochrom> | s/does that you/does that mean/ |
| 2026-01-15 23:34:05 +0100 | <monochrom> | Wait, does that you use a 286 to emulate a 386 then run GHC there? |
| 2026-01-15 23:33:58 +0100 | <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`. |