Newest at the top
| 2026-01-15 23:16:07 +0100 | <monochrom> | But if you do the denotational "construct the approximation sequence, take limit" it's plain as day. |
| 2026-01-15 23:15:27 +0100 | <jreicher> | *fiat |
| 2026-01-15 23:15:25 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 256 seconds) |
| 2026-01-15 23:15:24 +0100 | <jreicher> | "fiar" is "assertion" |
| 2026-01-15 23:15:24 +0100 | <monochrom> | Every textbook or tutorial I saw tried to explain it poorly with lazy evaluation. |
| 2026-01-15 23:15:21 +0100 | <EvanR> | introduced* |
| 2026-01-15 23:15:12 +0100 | <EvanR> | an example of an axiom in type theory is the law of excluded middle. Introduces by fiat. As opposed to proven as a theorem somehow |
| 2026-01-15 23:14:53 +0100 | <jreicher> | int-e: monochrom: I appreciate the use of "extra" infinity as a simplification. Not the first time I've heard that argument. |
| 2026-01-15 23:14:51 +0100 | <monochrom> | The hardest example made easy being fs = 1 : 1 : zipWith (+) fs (tail fs). |
| 2026-01-15 23:14:22 +0100 | <EvanR> | to save space |
| 2026-01-15 23:14:16 +0100 | <EvanR> | definition is just naming something that you could already say long winded |
| 2026-01-15 23:14:10 +0100 | <jreicher> | Not for a formal theory, no |
| 2026-01-15 23:13:57 +0100 | <EvanR> | well that's muddying things a lot isn't it |
| 2026-01-15 23:13:55 +0100 | <int-e> | Again, keeping things as mathematically simple as possible. |
| 2026-01-15 23:13:46 +0100 | <jreicher> | Definitions are axioms |
| 2026-01-15 23:13:40 +0100 | <int-e> | And, correspondingly, the easiest model for streams of Bools gives you an arbitrary boolean value for the n-th element of the stream, for each natural number N. The set of all these functions is uncountable. |
| 2026-01-15 23:13:37 +0100 | <EvanR> | definitions |
| 2026-01-15 23:13:33 +0100 | <jreicher> | How can you have a theory without axioms? |
| 2026-01-15 23:13:20 +0100 | <EvanR> | jreicher, in type theory, we don't always have axioms! |
| 2026-01-15 23:13:13 +0100 | <monochrom> | My lecture notes also shows that if you use this "unrealistic" (but still sound) denotational approach, it is easier to predict the outcome of certain recursive definitions. |
| 2026-01-15 23:13:04 +0100 | <EvanR> | that's more like ultrafinitism |
| 2026-01-15 23:13:00 +0100 | <EvanR> | that you can't run a program for infinite time isn't the secret sauce to model it as countable |
| 2026-01-15 23:12:57 +0100 | <jreicher> | EvanR: the proof (like all proofs) starts with axioms. The axioms are the assertions. |
| 2026-01-15 23:12:27 +0100 | <EvanR> | yielding the missing stream |
| 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. |