Newest at the top
| 2026-01-15 23:10:18 +0100 | <EvanR> | that's what uncountable is |
| 2026-01-15 23:10:09 +0100 | <EvanR> | sure |
| 2026-01-15 23:10:05 +0100 | <jreicher> | Not "some". Most. |
| 2026-01-15 23:10:05 +0100 | <EvanR> | which is what we're trying to say |
| 2026-01-15 23:09:52 +0100 | <EvanR> | jreicher, this is like saying any map from N into A necessarily misses some As |
| 2026-01-15 23:09:22 +0100 | <EvanR> | kind of cool |
| 2026-01-15 23:09:21 +0100 | <int-e> | If you don't model this mathematically, countability doesn't even come up; there is no set whose cardinality you could possibly discuss. |
| 2026-01-15 23:09:21 +0100 | <jreicher> | And if they're missing, how is it meaningful to say the type is uncountable? (I feel like this is hitting downward lowenheim-skolem somehow) |
| 2026-01-15 23:09:20 +0100 | <EvanR> | and cantor's proof produces a constructive example list which isn't there |
| 2026-01-15 23:09:01 +0100 | <dolio> | Uncomputable lists aren't real. |
| 2026-01-15 23:08:55 +0100 | <EvanR> | no matter how you go about it |
| 2026-01-15 23:08:47 +0100 | <EvanR> | some are necessarily missing |
| 2026-01-15 23:08:34 +0100 | <monochrom> | I thought I explained that. A model that contains impractical elements can be a useful approximation and/or abstraction. |
| 2026-01-15 23:08:33 +0100 | <EvanR> | you can't generate a stream of all the lists |
| 2026-01-15 23:08:11 +0100 | <int-e> | EvanR: Well, in isolation, assuming it isn't fused away :P |
| 2026-01-15 23:08:05 +0100 | <EvanR> | that's the point |
| 2026-01-15 23:07:56 +0100 | <jreicher> | EvanR: I don't think so, no. I'm saying something more like you can't generate ALL infinite lists that way (e.g. uncomputable ones) |
| 2026-01-15 23:07:46 +0100 | <EvanR> | if you're lucky |
| 2026-01-15 23:07:39 +0100 | <EvanR> | in ghc! |
| 2026-01-15 23:07:32 +0100 | <int-e> | (once fully evaluated) |
| 2026-01-15 23:07:25 +0100 | <int-e> | it's a very finite graph :P |
| 2026-01-15 23:07:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:07:04 +0100 | <EvanR> | in haskell xD |
| 2026-01-15 23:07:00 +0100 | <EvanR> | you're trying to say like > repeat 'a' is not an infinite list |
| 2026-01-15 23:06:25 +0100 | <jreicher> | If we say infinite bitstreams exist, then the type is uncountable. I'm not arguing with that. But in practice (and I hesitate as I say that) you're never going to have an infinite bitstream, so I'm not sure this is a sensible thing to say. |
| 2026-01-15 23:06:21 +0100 | <dolio> | I.E. given a computable enumeration of computable bit streams, one can compute a bit stream not in the enumeration. |
| 2026-01-15 23:06:03 +0100 | <EvanR> | i.e. the only thing that is real is a real running program on a computer, which will never be infinite, because the universe is purely finite or something. Which is the kind of stuff I'd like to use math to avoid entirely |
| 2026-01-15 23:05:51 +0100 | <dolio> | Viewed externally as built in classical mathematics, that is the statement, 'the set of recursive bit streams is "computably uncountable."' |
| 2026-01-15 23:05:23 +0100 | <int-e> | And a clear distinction between object and meta levels, because at the object level, for any sequence of sequences f :: Nat -> (Nat -> Bool) you can apply Cantor's diagonal construction, s n = not (f n n) to obtain a sequence that's not in the enumeration. (I'll skip how Nat -> Bool is equivalent to streams of bools) |
| 2026-01-15 23:05:11 +0100 | <dolio> | Internally to the world of recursive mathematics, Cantor's diagonal argument holds, and the type of infinite bit streams is uncountable. |
| 2026-01-15 23:05:09 +0100 | <EvanR> | sounds like operational semantics |
| 2026-01-15 23:04:52 +0100 | <jreicher> | I have to think this through carefully, but I think you are all accepting the existence of infinitely-running programs? |
| 2026-01-15 23:04:26 +0100 | <dolio> | E.G. if you build recursive things in classical mathematics, it will appear that the set of recursively definable streams is countable. But the enumeration of all such streams is not recursive. |
| 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 ) |