Newest at the top
| 2026-01-16 00:40:20 +0100 | <int-e> | nothing beyond omega arises in this fashion |
| 2026-01-16 00:40:09 +0100 | <int-e> | omega arises naturally as the least upper bound of all natural numbers, corresponding to having computations of arbitrary length |
| 2026-01-16 00:39:57 +0100 | <jreicher> | I know. That's kind of what I mean by "fine line". We seem to be saying we've got "observable", "unobservable", and then something like "observable in principle" (conceivable?) |
| 2026-01-16 00:39:34 +0100 | <Leary> | jreicher: SillyType caps out at omega since you can only "add 1" on the left to get 1 + omega = omega; there's no omega + 1. |
| 2026-01-16 00:39:17 +0100 | <int-e> | No it's not the same. |
| 2026-01-16 00:39:12 +0100 | <jreicher> | (I'm just arguing devil's advocate now) |
| 2026-01-16 00:39:08 +0100 | <EvanR> | are you sure? |
| 2026-01-16 00:39:02 +0100 | <jreicher> | ...just like infinitely running programs are not observable |
| 2026-01-16 00:38:43 +0100 | <int-e> | like, sure, you can pretend that there is an element of SillyType for every ordinal number. Or that there's some other unobservable feature that makes the values more plentiful. There's no purpose to it though, since none of this will be observable. |
| 2026-01-16 00:38:22 +0100 | <EvanR> | (like 1) |
| 2026-01-16 00:38:12 +0100 | <EvanR> | it's about the number of possible streams |
| 2026-01-16 00:38:07 +0100 | <EvanR> | you're not asking about the number of 1s in the stream |
| 2026-01-16 00:37:54 +0100 | <jreicher> | int-e: which is why I queried the use of an "infinitely running program" to begin with. It's an interesting dividing line. |
| 2026-01-16 00:37:38 +0100 | <EvanR> | if this is uncountable then, I'll eat my hat |
| 2026-01-16 00:37:25 +0100 | <EvanR> | there's like 1 possible value of SillyType |
| 2026-01-16 00:37:24 +0100 | <int-e> | you're also stepping beyond what's useful for modelling program semantics |
| 2026-01-16 00:37:17 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 00:37:03 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:36:27 +0100 | <jreicher> | OK, but depending on what we allow for BitStream, can't I be allowed to construct all the aleph numbers from SillyType? That would make it uncountable i think |
| 2026-01-16 00:35:52 +0100 | <int-e> | So it's nothing like a bit stream. |
| 2026-01-16 00:35:31 +0100 | <int-e> | jreicher: Anyway, at an intuitive level, SillyType has no bits that you could flip to make Cantor's diagonal argument work. |
| 2026-01-16 00:35:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 00:35:03 +0100 | <EvanR> | and subfinite |
| 2026-01-16 00:34:23 +0100 | <EvanR> | there's other fun stuff like subcountable |
| 2026-01-16 00:33:55 +0100 | <monochrom> | so "more than" is helpful for me. |
| 2026-01-16 00:33:41 +0100 | <monochrom> | For BitStream I'm using: if a subset is uncountable, then a superset is also uncountable. |
| 2026-01-16 00:33:13 +0100 | <monochrom> | Sure. That's doesn't get you anywhere per se. |
| 2026-01-16 00:32:53 +0100 | <monochrom> | (You can also attempt diagonalization on SillyType and get stuck.) |
| 2026-01-16 00:32:49 +0100 | <jreicher> | monochrom: am I allowed to say SillyType has more the infinite unary strings? |
| 2026-01-16 00:32:25 +0100 | <monochrom> | (so use Cantor diagonlization again) |
| 2026-01-16 00:32:08 +0100 | <monochrom> | BitStream has more than infinite bit strings. |
| 2026-01-16 00:31:40 +0100 | <jreicher> | monochrom: what's your preferred proof that bitstream is uncountable? I'm looking for what it uses that SillyType isn't entitled to |
| 2026-01-16 00:31:29 +0100 | <int-e> | 1^N has cardinality 1; 2^N or 3^N is uncountable. |
| 2026-01-16 00:31:21 +0100 | <monochrom> | 2-colourability is polynomial-time, 3-colourability is NP-complete. |
| 2026-01-16 00:31:10 +0100 | <int-e> | bitstream adds additional observations for each natural number. |
| 2026-01-16 00:30:54 +0100 | <monochrom> | SillyType is countable, BitStream is uncountable. |
| 2026-01-16 00:30:51 +0100 | <int-e> | jreicher: NO! |
| 2026-01-16 00:30:35 +0100 | <jreicher> | monochrom: hang on, are you now saying bitstream is countable? I was hoping that, having proved SillyType is countable, you'd now prove bitstream is uncountable. |
| 2026-01-16 00:30:22 +0100 | <monochrom> | Generally there are multiple instance when switching from 1 to 2, or 2 to 3, or 3 to 4 makes breaking changes. |
| 2026-01-16 00:30:04 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 00:29:56 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-16 00:29:51 +0100 | k0zy | (~user@user/k0zy) k0zy |
| 2026-01-16 00:29:51 +0100 | k0zy | (~user@75-164-179-179.ptld.qwest.net) (Changing host) |
| 2026-01-16 00:29:43 +0100 | k0zy | (~user@75-164-179-179.ptld.qwest.net) |
| 2026-01-16 00:29:37 +0100 | <int-e> | Sure. It's morally finite ("morally" being the view where you don't have bottoms) |
| 2026-01-16 00:29:36 +0100 | <monochrom> | But intuitively I'm not surprised. Expressing natural numbers in unary requires n units of memory for n; "merely" switching to binary, that drops down to lg n. |
| 2026-01-16 00:28:51 +0100 | <jreicher> | And so SillyType is countable, yes? |
| 2026-01-16 00:27:29 +0100 | <monochrom> | I map 0 to the infinite stream z = I z, 1 to bottom, 2 to I bottom, 3 to I (I bottom), etc. |
| 2026-01-16 00:26:51 +0100 | <jreicher> | Every proof I sketch out results in an inconsistency. |
| 2026-01-16 00:26:25 +0100 | <jreicher> | No, prove away, please. I'd like to understand. |