Newest at the top
| 2026-01-15 23:04:20 +0100 | <EvanR> | (but I might be wrong here beacuse of higher order programs) |
| 2026-01-15 23:03:54 +0100 | Inline | (~User@cgn-195-14-218-118.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 2026-01-15 23:03:46 +0100 | <EvanR> | or definability, because you have to write the code, and code is countable |
| 2026-01-15 23:03:29 +0100 | <dolio> | jreicher: The only way to believe that being recursive makes things countable is by not taking recursion seriously enough. When you set up your mathematics such that everything is inherently recursive, some things in that mathematics become uncountable again. |
| 2026-01-15 23:03:22 +0100 | <int-e> | (I can defend the idea that streams are countable but it'll involve computability and/or Scott domains) |
| 2026-01-15 23:02:58 +0100 | <EvanR> | jreicher, good xD |
| 2026-01-15 23:02:48 +0100 | <EvanR> | you first need to know what Bitstreams even are, and then you can progress to the cantor style proof which mirrors the classic version for binary strings |
| 2026-01-15 23:02:39 +0100 | <jreicher> | I'm not finitist. I just said infinite series of finite objects. |
| 2026-01-15 23:02:30 +0100 | <monochrom> | OK sure. Read my lecture notes first? |
| 2026-01-15 23:02:25 +0100 | <int-e> | But how can you discuss countability in a finitist context? :P |
| 2026-01-15 23:02:17 +0100 | <jreicher> | I'm not rejecting denotational semantics. I'd just like a pointer to something that explains where/how/why anything uncountable comes in. |
| 2026-01-15 23:01:52 +0100 | <monochrom> | I can respect that you reject denotational semantics altogether, but then you should also be rejecting "bottom". |
| 2026-01-15 23:01:08 +0100 | <EvanR> | the corresponding complaint about infinite objects in normal math is getting worse than I thought, though allowing "infinite" versions of each value at least isn't ultrafinite |
| 2026-01-15 23:01:01 +0100 | <monochrom> | If you don't complain that I said "bottom", then you have accepted that I am doing a denotational semantics model, and therefore there are infinite strings in the model. |
| 2026-01-15 23:00:54 +0100 | <lambdabot> | [0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1... |
| 2026-01-15 23:00:53 +0100 | <dolio> | > cycle [0,1] |
| 2026-01-15 23:00:25 +0100 | <int-e> | . o O ( it must be nice to have convictions ) |
| 2026-01-15 23:00:10 +0100 | EvanR | looks at jreicher |
| 2026-01-15 22:59:58 +0100 | <EvanR> | I guess including all these partially defined possibilities is making it even more infinite |
| 2026-01-15 22:59:48 +0100 | <jreicher> | You have an infinite series of finite strings |
| 2026-01-15 22:59:40 +0100 | <jreicher> | monochrom: My only point is that none of these recursive datatypes give you infinite strings. |
| 2026-01-15 22:58:55 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds) |
| 2026-01-15 22:58:52 +0100 | <monochrom> | The increasing sequence I bottom, I (I bottom), I (I (I bottom)) ... needs a least upper bound. |
| 2026-01-15 22:58:18 +0100 | <EvanR> | there's no finite strings by design, so I'm confused by that |
| 2026-01-15 22:57:57 +0100 | <monochrom> | You need infinite strings for completeness. |
| 2026-01-15 22:57:12 +0100 | <jreicher> | monochrom: Exactly. So making it a "binary choice" recursion doesn't magically make it uncountable |
| 2026-01-15 22:56:59 +0100 | <EvanR> | so cardinalty 1 |
| 2026-01-15 22:56:54 +0100 | <EvanR> | jreicher, is the only (respectable) value here I (I (I (I ...)))? |
| 2026-01-15 22:56:47 +0100 | <monochrom> | SillyType is countable. |
| 2026-01-15 22:56:46 +0100 | <jreicher> | monochrom: there aren't any infinite bit strings in the set |
| 2026-01-15 22:56:23 +0100 | <monochrom> | With my notes, you can either take the watered-down take in the first half, where I just assert that all infinite bit strings are in the set for the type, then use the usual diagonizable argument; or use the second half where I describe the recipe for the set for non-strict ADTs in general, then do it for BitStream yourself... |
| 2026-01-15 22:56:22 +0100 | <jreicher> | EvanR: Take (as a silly example) data SillyType = I SillyType. Countable or uncountable? |
| 2026-01-15 22:56:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 22:56:02 +0100 | <dolio> | https://hub.darcs.net/dolio/unpossible/browse/src/Cantor/Properties.agda#66 |
| 2026-01-15 22:55:57 +0100 | <EvanR> | possibly infinite |
| 2026-01-15 22:55:45 +0100 | <EvanR> | one way to look at countable A is you can make a [A] which contains at some point all possible A values |
| 2026-01-15 22:54:55 +0100 | <jreicher> | dolio: reference? I don't see how that would be the case |
| 2026-01-15 22:54:40 +0100 | <dolio> | The type of lazy streams is uncountable. |
| 2026-01-15 22:54:02 +0100 | <monochrom> | Well here goes shameless plug. This is my lecture notes for this stuff: https://www.cs.utoronto.ca/~trebla/CSCC24-latest/partial-order-recursion.html |
| 2026-01-15 22:53:53 +0100 | <EvanR> | all things constructed are finite? |
| 2026-01-15 22:53:41 +0100 | <EvanR> | I don't follow... |
| 2026-01-15 22:53:29 +0100 | <jreicher> | I've already explained. The "recursion" of the construction is infinite, but all the things constructed are finite. So you don't get diagonalisation. |
| 2026-01-15 22:52:47 +0100 | <EvanR> | what makes you say that |
| 2026-01-15 22:52:36 +0100 | <jreicher> | I'm just after anything that will prove (without question-begging assertions) that BitStream is uncountable. It looks entirely countable to me. |
| 2026-01-15 22:51:39 +0100 | <monochrom> | Consider the usual denotational sematnics of BitStream, as opposed to the usual operational semantics of it in Haskell? So do you mean that you seek materials for teaching denotational semantics? |
| 2026-01-15 22:51:37 +0100 | <EvanR> | ignoring bottoms there's no way to make a finite Bitstream |
| 2026-01-15 22:51:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:50:56 +0100 | <EvanR> | we're about to jump the shark from uncountability to ultrafinitism |
| 2026-01-15 22:50:44 +0100 | <jreicher> | You can't have an infinite bitstream value |
| 2026-01-15 22:50:31 +0100 | <EvanR> | wat |