Newest at the top
| 2026-01-16 00:47:15 +0100 | <EvanR> | nobody threw in bitstreams that can't be computed that was iterated like 3 times |
| 2026-01-16 00:47:00 +0100 | <jreicher> | TMA: exactly |
| 2026-01-16 00:46:56 +0100 | <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-16 00:46:51 +0100 | <int-e> | (It's an infinite type though so adding non-standard elements will generally work.) |
| 2026-01-16 00:46:51 +0100 | <TMA> | so the sequence of ω⁺Is could also be in SillyType |
| 2026-01-16 00:46:40 +0100 | Inline | (~User@2001-4dd6-dd24-0-f7db-3cda-3b52-1dd2.ipv6dyn.netcologne.de) Inline |
| 2026-01-16 00:46:34 +0100 | <EvanR> | exercise write the function from Nat to SillyType which witnesses it |
| 2026-01-16 00:46:30 +0100 | <int-e> | Yes, that's still countable. |
| 2026-01-16 00:46:11 +0100 | <EvanR> | looks like yes |
| 2026-01-16 00:46:04 +0100 | <jreicher> | But still countable? |
| 2026-01-16 00:45:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 00:45:51 +0100 | <EvanR> | now you have many distinguishable SillyType strings |
| 2026-01-16 00:45:28 +0100 | <int-e> | IOW, there can't be any distinct non-standard element of that type. |
| 2026-01-16 00:45:11 +0100 | <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-16 00:45:06 +0100 | <EvanR> | that would allow finite strings |
| 2026-01-16 00:44:53 +0100 | <jreicher> | Would you prefer data SillyType = I | I SillyType? |
| 2026-01-16 00:44:37 +0100 | <EvanR> | so maybe they all count as 1 |
| 2026-01-16 00:44:29 +0100 | <EvanR> | so like, bottom, 1 bottom, 1 (1 bottom) etc are all consistent |
| 2026-01-16 00:43:44 +0100 | <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-16 00:42:46 +0100 | <int-e> | EvanR: "we" apparently allow bottoms |
| 2026-01-16 00:41:17 +0100 | <EvanR> | I missed how we're distinguishing any values of SillyType beyond the obvious 1 |
| 2026-01-16 00:40:52 +0100 | <jreicher> | Leary: but then why wouldn't we say BitStream caps out at computable streams? (I know it's not the same) |
| 2026-01-16 00:40:45 +0100 | <EvanR> | or counting runtime behaviors |
| 2026-01-16 00:40:40 +0100 | <EvanR> | if you're counting values, you're not counting programs, unless that's the semantics you're using |
| 2026-01-16 00:40:24 +0100 | <EvanR> | that's the point of semantics to define what the values (what the programs mean) |
| 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. |