Newest at the top
| 2026-01-16 01:32:56 +0100 | Tuplanolla | (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2026-01-16 01:30:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 01:29:26 +0100 | <monochrom> | haha |
| 2026-01-16 01:29:18 +0100 | <TMA> | monochrom: good idea, I'll go to bed instead |
| 2026-01-16 01:27:25 +0100 | <monochrom> | TMA: Please don't go there :( >:) |
| 2026-01-16 01:26:53 +0100 | <monochrom> | "my car can do 0 to infinity in 60 seconds" >:) |
| 2026-01-16 01:26:43 +0100 | <TMA> | monochrom: you can still have uncomputable subsets of unary strings though |
| 2026-01-16 01:25:28 +0100 | DetourNe- | DetourNetworkUK |
| 2026-01-16 01:24:43 +0100 | <EvanR> | monochrom, the zero, infinity, ... rule |
| 2026-01-16 01:24:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:23:59 +0100 | <EvanR> | I'm good |
| 2026-01-16 01:23:51 +0100 | <jreicher> | Umm, that's philosophical turf on which I'm very comfortable arguing, but that would be even more off-topic than we already have been. Can still go there if you want. |
| 2026-01-16 01:23:40 +0100 | <int-e> | EvanR: Now that's different. Clearly chess was designed to make me lose! |
| 2026-01-16 01:23:31 +0100 | DetourNetworkUK | (DetourNetw@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 2026-01-16 01:23:16 +0100 | <EvanR> | and is valid |
| 2026-01-16 01:23:14 +0100 | <EvanR> | the game in which you lost nonetheless exists |
| 2026-01-16 01:23:12 +0100 | <monochrom> | Shannon's definition of "information" implies that {0} has 0 bits of information, {0,1} has 1 bit of information. That is already a kind of "everything is different" if you look at the ratio: from 0 to 1 is an infinite percent increase. To a large extent the whole conversation above follows. |
| 2026-01-16 01:23:11 +0100 | DetourNe- | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2026-01-16 01:23:01 +0100 | <jreicher> | Then it arguably doesn't satisfy its goal |
| 2026-01-16 01:22:47 +0100 | <jreicher> | More like questioning it if it's too easy or too hard to play. Or not fun. Something like that. |
| 2026-01-16 01:22:42 +0100 | <int-e> | "Young man, in mathematics you don't understand things. You just get used to them." -- John von Neumann |
| 2026-01-16 01:22:39 +0100 | <EvanR> | better to play / define another game |
| 2026-01-16 01:22:26 +0100 | <EvanR> | that's like questioning the game of chess itself if you lose |
| 2026-01-16 01:21:51 +0100 | <jreicher> | or question the definitions/axioms that result in the theorem. |
| 2026-01-16 01:21:44 +0100 | <EvanR> | intuition can be adjusted to fit the facts :tm: |
| 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. |