Newest at the top
| 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 |
| 2026-01-15 22:50:22 +0100 | <jreicher> | Any bitstream value is INDEFINITE length, but it's still FINITE. |
| 2026-01-15 22:50:06 +0100 | <EvanR> | that's .. neither here nor there |
| 2026-01-15 22:49:55 +0100 | <jreicher> | You can't make the diagonalisation from it |
| 2026-01-15 22:49:53 +0100 | <EvanR> | reals? |
| 2026-01-15 22:49:46 +0100 | <jreicher> | Yes, but that datatype is not all the reals |