Newest at the top
| 2026-01-15 23:12:22 +0100 | <monochrom> | Avoiding the cumbersomeness and missing-the-forest-for-the-trees of operational semantics and Turing machines. |
| 2026-01-15 23:12:18 +0100 | <EvanR> | jreicher, it's not an assertion, there's a constructive proof xD |
| 2026-01-15 23:12:14 +0100 | <int-e> | It's a simplification. |
| 2026-01-15 23:12:03 +0100 | <int-e> | When you model programs mathematically, you typically do not impose a running time bound up front, so the modelled program behavior is effectively infinite (since you can run it to any arbitrary length, giving you a state after n steps for all natural numbers n). |
| 2026-01-15 23:12:03 +0100 | <EvanR> | this is why I began by phrasing the whole thing as "are you sure" about not having uncountable things, it depends on how you think about it |
| 2026-01-15 23:12:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 23:11:47 +0100 | <monochrom> | Another example: Translating Haskell to Turing machines. |
| 2026-01-15 23:11:44 +0100 | <jreicher> | OK. So what do we gain from adding the assertion (because we'd need to) that makes it uncountable? |
| 2026-01-15 23:11:26 +0100 | <monochrom> | Yes. For example operational semantics. |
| 2026-01-15 23:11:21 +0100 | <EvanR> | sure |
| 2026-01-15 23:11:04 +0100 | <jreicher> | So let me re-ask the question. Do you think it's possible to model all this mathematically such that BitStream is a countable infinite type? |
| 2026-01-15 23:10:58 +0100 | <dolio> | Every computable map misses many computable streams. |
| 2026-01-15 23:10:42 +0100 | Zemy | (~Zemy@72.178.108.235) |
| 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. |