Newest at the top
| 2026-01-16 01:21:22 +0100 | <jreicher> | Yes |
| 2026-01-16 01:21:16 +0100 | <monochrom> | I mean, if a theorem is counterintuitive, then question the intuition not the theorem. |
| 2026-01-16 01:21:11 +0100 | <jreicher> | I certainly think it's interesting. It just doesn't seem to be something that should happen, but it does. |
| 2026-01-16 01:20:27 +0100 | <monochrom> | which is again just the counterintuitive "change '1' to '2' suddenly everything is different". |
| 2026-01-16 01:19:50 +0100 | <monochrom> | EvanR: I would be the one that threw in uncomputable bit streams. But I am not being inconsistent; if possible I would threw in uncomputable unary streams too, except that it is impossible, no such thing exists. |
| 2026-01-16 01:19:09 +0100 | <EvanR> | I think agda makes this nicer by letting you define ordinals indexed by universe, then "useful programs using ordinals" (??) can then be universe polymorphic |
| 2026-01-16 01:18:01 +0100 | k0zy | (~user@user/k0zy) (Ping timeout: 264 seconds) |
| 2026-01-16 01:14:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-16 01:12:16 +0100 | <jreicher> | Yeah it seems to me the "first few" would be straightforward |
| 2026-01-16 01:11:37 +0100 | <EvanR> | all the ordinals is ... problematic but you can have a lot of them |
| 2026-01-16 01:10:48 +0100 | <jreicher> | Now you've got me wondering if it's possible to define a type that will allow construction of all the limit ordinals using infinite lists. |
| 2026-01-16 01:08:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:05:48 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 01:05:34 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:58:57 +0100 | trickard_ | trickard |
| 2026-01-16 00:57:24 +0100 | <EvanR> | though if you want to get into that there's more exotic constructions |
| 2026-01-16 00:57:21 +0100 | <jreicher> | No, I know. I'm just picking out where the line is. |
| 2026-01-16 00:56:59 +0100 | <EvanR> | they're not needed to make the original point, just as in cantor |
| 2026-01-16 00:56:41 +0100 | <jreicher> | But not transfinite lists |
| 2026-01-16 00:56:17 +0100 | <EvanR> | turns out |
| 2026-01-16 00:56:16 +0100 | ttybitnik | (~ttybitnik@user/wolper) (Ping timeout: 256 seconds) |
| 2026-01-16 00:56:12 +0100 | <EvanR> | this is haskell an we have infinite lists |
| 2026-01-16 00:56:09 +0100 | <int-e> | Also has it really been 2 hours of this... |
| 2026-01-16 00:55:58 +0100 | <TMA> | jreicher: BUT there is just a single such string in the smallest model of the data SillyType = I SillyType theory |
| 2026-01-16 00:55:51 +0100 | <jreicher> | I'm not insisting anything of the sort. I also don't think they're analogous. I'm just trying to understand why. |
| 2026-01-16 00:55:43 +0100 | <EvanR> | jreicher, the original definition of Bitstream and SillyType both have nothing but infinite streams. Not really a double standard |
| 2026-01-16 00:55:43 +0100 | <Inline> | lol |
| 2026-01-16 00:55:38 +0100 | <Inline> | the egotist set |
| 2026-01-16 00:55:29 +0100 | <int-e> | jreicher: You're insisting that two things are analogous despite strong evidence to the contrary, all of which has been laid out in front of you above. |
| 2026-01-16 00:55:24 +0100 | <Inline> | aye aye aye eye eye aye....... |
| 2026-01-16 00:54:54 +0100 | <TMA> | jreicher: there is transfinite silly string... it goes: I I I I I I I I I ... |
| 2026-01-16 00:53:58 +0100 | EvanR | boggles |
| 2026-01-16 00:53:47 +0100 | <jreicher> | I'm not suggesting we do that. I'm just trying to understand the double standard. |
| 2026-01-16 00:53:42 +0100 | <int-e> | . o O ( if you disallow inifinte bitstreams, bitstream becomes empty ) |
| 2026-01-16 00:53:38 +0100 | <EvanR> | would have saved us a lot of trouble |
| 2026-01-16 00:53:32 +0100 | <EvanR> | why didn't cantor think of disallowing infinite streams |
| 2026-01-16 00:53:10 +0100 | <jreicher> | If we disallow infinite bitstreams, bitstream becomes countable. If we allow infinite bitstreams, why can't we allow transfinite silly strings? |
| 2026-01-16 00:52:47 +0100 | <int-e> | EvanR: No, we've crossed that line long ago. |
| 2026-01-16 00:52:37 +0100 | <int-e> | (data SillyType = End | I SillyType) |
| 2026-01-16 00:52:33 +0100 | <EvanR> | it's borderline Silly |
| 2026-01-16 00:52:23 +0100 | <int-e> | (data Nat = Z | S N) |
| 2026-01-16 00:52:18 +0100 | <EvanR> | int-e, looooool |
| 2026-01-16 00:52:12 +0100 | <EvanR> | if you try that on Bitstream, then somebody can come along and get a counterexample stream |
| 2026-01-16 00:52:05 +0100 | <int-e> | (that's borderline stupid; SillyType is obviously isomorphic to Nat) |
| 2026-01-16 00:51:27 +0100 | <EvanR> | specifically, f Z = End; f (S n) = I (f n) |
| 2026-01-16 00:50:45 +0100 | <EvanR> | seems countable |
| 2026-01-16 00:50:44 +0100 | <TMA> | jreicher: BitStream is uncountable. |
| 2026-01-16 00:50:20 +0100 | <EvanR> | I mean, all |
| 2026-01-16 00:50:08 +0100 | <EvanR> | you can map (ok... lazy?) Nat to any SillyType = End | I SillyType |
| 2026-01-16 00:50:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |