Logs: liberachat/#haskell
| 2026-01-15 23:29:36 | <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-15 23:29:37 | <int-e> | Sure. It's morally finite ("morally" being the view where you don't have bottoms) |
| 2026-01-15 23:29:43 | → | k0zy joins (~user@75-164-179-179.ptld.qwest.net) |
| 2026-01-15 23:29:51 | × | k0zy quits (~user@75-164-179-179.ptld.qwest.net) (Changing host) |
| 2026-01-15 23:29:51 | → | k0zy joins (~user@user/k0zy) |
| 2026-01-15 23:29:56 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-15 23:30:04 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 23:30:22 | <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-15 23:30:35 | <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-15 23:30:51 | <int-e> | jreicher: NO! |
| 2026-01-15 23:30:54 | <monochrom> | SillyType is countable, BitStream is uncountable. |
| 2026-01-15 23:31:10 | <int-e> | bitstream adds additional observations for each natural number. |
| 2026-01-15 23:31:21 | <monochrom> | 2-colourability is polynomial-time, 3-colourability is NP-complete. |
| 2026-01-15 23:31:29 | <int-e> | 1^N has cardinality 1; 2^N or 3^N is uncountable. |
| 2026-01-15 23:31:40 | <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-15 23:32:08 | <monochrom> | BitStream has more than infinite bit strings. |
| 2026-01-15 23:32:25 | <monochrom> | (so use Cantor diagonlization again) |
| 2026-01-15 23:32:49 | <jreicher> | monochrom: am I allowed to say SillyType has more the infinite unary strings? |
| 2026-01-15 23:32:53 | <monochrom> | (You can also attempt diagonalization on SillyType and get stuck.) |
| 2026-01-15 23:33:13 | <monochrom> | Sure. That's doesn't get you anywhere per se. |
| 2026-01-15 23:33:41 | <monochrom> | For BitStream I'm using: if a subset is uncountable, then a superset is also uncountable. |
| 2026-01-15 23:33:55 | <monochrom> | so "more than" is helpful for me. |
| 2026-01-15 23:34:23 | <EvanR> | there's other fun stuff like subcountable |
| 2026-01-15 23:35:03 | <EvanR> | and subfinite |
| 2026-01-15 23:35:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 23:35:31 | <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-15 23:35:52 | <int-e> | So it's nothing like a bit stream. |
| 2026-01-15 23:36:27 | <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-15 23:37:03 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 23:37:17 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 23:37:24 | <int-e> | you're also stepping beyond what's useful for modelling program semantics |
| 2026-01-15 23:37:25 | <EvanR> | there's like 1 possible value of SillyType |
| 2026-01-15 23:37:38 | <EvanR> | if this is uncountable then, I'll eat my hat |
| 2026-01-15 23:37:54 | <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-15 23:38:07 | <EvanR> | you're not asking about the number of 1s in the stream |
| 2026-01-15 23:38:12 | <EvanR> | it's about the number of possible streams |
| 2026-01-15 23:38:22 | <EvanR> | (like 1) |
| 2026-01-15 23:38:43 | <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-15 23:39:02 | <jreicher> | ...just like infinitely running programs are not observable |
| 2026-01-15 23:39:08 | <EvanR> | are you sure? |
| 2026-01-15 23:39:12 | <jreicher> | (I'm just arguing devil's advocate now) |
| 2026-01-15 23:39:17 | <int-e> | No it's not the same. |
| 2026-01-15 23:39:34 | <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-15 23:39:57 | <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-15 23:40:09 | <int-e> | omega arises naturally as the least upper bound of all natural numbers, corresponding to having computations of arbitrary length |
| 2026-01-15 23:40:20 | <int-e> | nothing beyond omega arises in this fashion |
| 2026-01-15 23:40:24 | <EvanR> | that's the point of semantics to define what the values (what the programs mean) |
| 2026-01-15 23:40:40 | <EvanR> | if you're counting values, you're not counting programs, unless that's the semantics you're using |
| 2026-01-15 23:40:45 | <EvanR> | or counting runtime behaviors |
| 2026-01-15 23:40:52 | <jreicher> | Leary: but then why wouldn't we say BitStream caps out at computable streams? (I know it's not the same) |
| 2026-01-15 23:41:17 | <EvanR> | I missed how we're distinguishing any values of SillyType beyond the obvious 1 |
| 2026-01-15 23:42:46 | <int-e> | EvanR: "we" apparently allow bottoms |
| 2026-01-15 23:43:44 | <TMA> | ackshually, if we take SillyType as constructed then there is one value in it. if we take the definition as an axiom in a theory, there might exists a nonstandard model, in which there are more members of the SillyType |
| 2026-01-15 23:44:29 | <EvanR> | so like, bottom, 1 bottom, 1 (1 bottom) etc are all consistent |
| 2026-01-15 23:44:37 | <EvanR> | so maybe they all count as 1 |
| 2026-01-15 23:44:53 | <jreicher> | Would you prefer data SillyType = I | I SillyType? |
| 2026-01-15 23:45:06 | <EvanR> | that would allow finite strings |
| 2026-01-15 23:45:11 | <int-e> | TMA: You're disallowing bottoms so what you said is not true since we can show coinductively that for all a, b in SillyType, a = b. |
| 2026-01-15 23:45:28 | <int-e> | IOW, there can't be any distinct non-standard element of that type. |
| 2026-01-15 23:45:51 | <EvanR> | now you have many distinguishable SillyType strings |
| 2026-01-15 23:45:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 23:46:04 | <jreicher> | But still countable? |
| 2026-01-15 23:46:11 | <EvanR> | looks like yes |
| 2026-01-15 23:46:30 | <int-e> | Yes, that's still countable. |
| 2026-01-15 23:46:34 | <EvanR> | exercise write the function from Nat to SillyType which witnesses it |
| 2026-01-15 23:46:40 | → | Inline joins (~User@2001-4dd6-dd24-0-f7db-3cda-3b52-1dd2.ipv6dyn.netcologne.de) |
| 2026-01-15 23:46:51 | <TMA> | so the sequence of ω⁺Is could also be in SillyType |
| 2026-01-15 23:46:51 | <int-e> | (It's an infinite type though so adding non-standard elements will generally work.) |
| 2026-01-15 23:46:56 | <jreicher> | OK. So I'm still curious why we think it's OK to throw in bitstreams that can't be computed, but we can't throw in sillytype strings that can't be computed |
| 2026-01-15 23:47:00 | <jreicher> | TMA: exactly |
| 2026-01-15 23:47:15 | <EvanR> | nobody threw in bitstreams that can't be computed that was iterated like 3 times |
| 2026-01-15 23:47:28 | <EvanR> | (though I tried to once but everyone ignored me) |
| 2026-01-15 23:47:30 | int-e | loves moving goalposts btw. Not. |
| 2026-01-15 23:48:16 | <Leary> | jreicher: You can say that if you want to, but as has already been pointed out, you're "crossing the streams" of two settings. You can model BitStream in either a constructive or a classical setting, but it's uncountable in both /because the notion of countability also depends on the setting/. |
| 2026-01-15 23:48:36 | <jreicher> | EvanR: sorry, I must be missing something fundamental. I thought bitstream can't be (classically) uncountable without including non-computable streams |
| 2026-01-15 23:48:51 | <TMA> | but the smallest model contains just one infinite sequence of Is |
| 2026-01-15 23:48:53 | <EvanR> | well I never brought up classical uncountability |
| 2026-01-15 23:49:02 | <EvanR> | you're beyond me now |
| 2026-01-15 23:50:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 23:50:08 | <EvanR> | you can map (ok... lazy?) Nat to any SillyType = End | I SillyType |
| 2026-01-15 23:50:20 | <EvanR> | I mean, all |
| 2026-01-15 23:50:44 | <TMA> | jreicher: BitStream is uncountable. |
| 2026-01-15 23:50:45 | <EvanR> | seems countable |
| 2026-01-15 23:51:27 | <EvanR> | specifically, f Z = End; f (S n) = I (f n) |
| 2026-01-15 23:52:05 | <int-e> | (that's borderline stupid; SillyType is obviously isomorphic to Nat) |
| 2026-01-15 23:52:12 | <EvanR> | if you try that on Bitstream, then somebody can come along and get a counterexample stream |
| 2026-01-15 23:52:18 | <EvanR> | int-e, looooool |
| 2026-01-15 23:52:23 | <int-e> | (data Nat = Z | S N) |
| 2026-01-15 23:52:33 | <EvanR> | it's borderline Silly |
| 2026-01-15 23:52:37 | <int-e> | (data SillyType = End | I SillyType) |
| 2026-01-15 23:52:47 | <int-e> | EvanR: No, we've crossed that line long ago. |
| 2026-01-15 23:53:10 | <jreicher> | If we disallow infinite bitstreams, bitstream becomes countable. If we allow infinite bitstreams, why can't we allow transfinite silly strings? |
| 2026-01-15 23:53:32 | <EvanR> | why didn't cantor think of disallowing infinite streams |
| 2026-01-15 23:53:38 | <EvanR> | would have saved us a lot of trouble |
| 2026-01-15 23:53:42 | <int-e> | . o O ( if you disallow inifinte bitstreams, bitstream becomes empty ) |
| 2026-01-15 23:53:47 | <jreicher> | I'm not suggesting we do that. I'm just trying to understand the double standard. |
| 2026-01-15 23:53:58 | EvanR | boggles |
| 2026-01-15 23:54:54 | <TMA> | jreicher: there is transfinite silly string... it goes: I I I I I I I I I ... |
| 2026-01-15 23:55:24 | <Inline> | aye aye aye eye eye aye....... |
| 2026-01-15 23:55:29 | <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. |
All times are in UTC.