Logs: liberachat/#haskell
| 2026-01-15 22:50:01 | <jreicher> | EvanR: :D I'm just trying to use the word "exists" the same way everybody else does |
| 2026-01-15 22:50:14 | <EvanR> | everybody doesn't sound right... |
| 2026-01-15 22:50:25 | <jreicher> | Normal people then. :p |
| 2026-01-15 22:50:30 | <monochrom> | Ugh. But everybody uses a different meaning for "exists"! |
| 2026-01-15 22:50:49 | <c_wraith> | as if I only use a single meaning |
| 2026-01-15 22:50:57 | <monochrom> | hehe me too |
| 2026-01-15 22:51:05 | <jreicher> | dolio: I haven't heard the view that Chaitin's omega is not a real number. Interesting. What kind of object is it then? |
| 2026-01-15 22:51:28 | <monochrom> | But in this context we only need two: classical math, constructive math |
| 2026-01-15 22:51:53 | <EvanR> | sometimes that's not the discriminator |
| 2026-01-15 22:52:08 | <EvanR> | because you can often backport the insights you got from constructive math back to classical and realize it was bogus all along |
| 2026-01-15 22:52:23 | × | tcard_ quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2026-01-15 22:52:39 | → | tcard_ joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2026-01-15 22:52:46 | <dolio> | I'm not that familiar with what it even does, exactly. You can have a halting relation for Turing machines, but that relation will lack properties that would allow constructing a corresponding real number. |
| 2026-01-15 22:53:19 | <EvanR> | or it intrinsically requires an unrestricted choice principle |
| 2026-01-15 22:54:01 | × | fp quits (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 264 seconds) |
| 2026-01-15 22:54:07 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 22:54:09 | <EvanR> | instead accidentally |
| 2026-01-15 22:55:52 | <int-e> | dolio: Basically you define a prefix code {0,1}^* -> Turing machines. And you map the reals [0,1) to Turing machines via binary expansion and matching a prefix. Assign a non-halting TM to anything that doesn't match a prefix. So now you have a subset of R that corrsponds to halting Turing machines, and you can show classically that it's measurable with measure <= 1. Call that measure "halting... |
| 2026-01-15 22:55:58 | <int-e> | ...probability". |
| 2026-01-15 22:57:10 | <int-e> | (The arrow there is very much informal.) |
| 2026-01-15 22:57:33 | <dolio> | Okay, so, not every real has a binary expansion. |
| 2026-01-15 22:57:49 | <dolio> | Or, there is no mapping from reals to binary expansions, I should say. |
| 2026-01-15 22:57:54 | <int-e> | you have a set of measure 0 of real numbers that have two expansions. |
| 2026-01-15 22:57:58 | <jreicher> | Well, the point of Chaitin's omega is that the binary expansion is not computable |
| 2026-01-15 22:58:00 | <dolio> | There's a ∀∃, but not a function, I think. |
| 2026-01-15 22:58:12 | <jreicher> | (If you accept that the binary expansion exists in the first place) |
| 2026-01-15 22:58:24 | <geekosaur> | thinking informally, wouldn't a binary expansion have to be countable length? |
| 2026-01-15 22:58:30 | <int-e> | I said "classically"> |
| 2026-01-15 22:59:10 | <jreicher> | geekosaur: that might take us back to the start of the debate. :) I think the consensus is that denoting semantics for infinitely executing programs "in principle" simplifies things |
| 2026-01-15 22:59:47 | <jreicher> | Oh, sorry |
| 2026-01-15 22:59:56 | <jreicher> | I misread what you wrote! You said "countable" and I read "finite" |
| 2026-01-15 23:00:48 | <geekosaur> | right, I was abbreviating "countably finite", thought that would be fairly obvious from the ongoing context |
| 2026-01-15 23:00:53 | <geekosaur> | *infinite |
| 2026-01-15 23:01:02 | <geekosaur> | damn, fingers ahead of brain again |
| 2026-01-15 23:01:58 | <monochrom> | Me is even finger-disobeys-brain. (How else do you think I mistyped "you" for "mean"?! :) ) |
| 2026-01-15 23:02:17 | <dolio> | Presumably the prefix code is going to be set up so that there's a unique prefix for each binary expansion. |
| 2026-01-15 23:02:27 | <dolio> | Hopefully each real number. |
| 2026-01-15 23:03:12 | <dolio> | So even though the expansions are infinitely long, you only need to look at a finite portion. |
| 2026-01-15 23:03:13 | <EvanR> | jreicher, classic article in the earth days of modern math, "does every real number have a decimal expansion" |
| 2026-01-15 23:03:16 | <EvanR> | early* |
| 2026-01-15 23:03:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 23:04:07 | <EvanR> | this was before classical math "won" and "asserted" "yes" xD |
| 2026-01-15 23:04:27 | <EvanR> | no one will drive us out of the paradise cantor created for us |
| 2026-01-15 23:04:34 | <jreicher> | EvanR: OK.... Not sure what the point is? (And FYI I don't think classical math has won, but that's a debate for another day/channel) |
| 2026-01-15 23:04:51 | <EvanR> | around 1940s debate of this sort died out |
| 2026-01-15 23:05:01 | <EvanR> | resurrected way later |
| 2026-01-15 23:05:17 | <EvanR> | but hopefully now we can just state our systems and assumptions ahead of time and not debate vibes |
| 2026-01-15 23:05:41 | <EvanR> | jreicher, the point of the paper? well that's in the paper, and relevant to the above story about chaitin's number |
| 2026-01-15 23:05:41 | <monochrom> | Leibniz would have loved that. |
| 2026-01-15 23:06:03 | <jreicher> | EvanR: no, not the point of the paper, the point you are wanting to make by providing the paper |
| 2026-01-15 23:06:38 | <EvanR> | remarks about about the "construction" hinging on obtaining a digital expansion of any real number |
| 2026-01-15 23:06:49 | <TMA> | mapping digit sequences of countably infinite lenght to real numbers is a classic way to show that {0,1}^* (or {0..9}^*) is not countable set |
| 2026-01-15 23:07:22 | <EvanR> | we just did that |
| 2026-01-15 23:07:24 | <EvanR> | xD |
| 2026-01-15 23:07:32 | <EvanR> | except skipping the reals |
| 2026-01-15 23:07:38 | <jreicher> | EvanR: you mean the construction of diagonalisation? |
| 2026-01-15 23:07:42 | × | Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 23:07:57 | → | Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 23:08:26 | × | AlexNoo quits (~AlexNoo@5.139.232.54) (Read error: Connection reset by peer) |
| 2026-01-15 23:08:48 | → | AlexNoo joins (~AlexNoo@5.139.232.54) |
| 2026-01-15 23:10:17 | <jreicher> | (Because you don't need every real number to have a decimal/binary expansion for that construction) |
| 2026-01-15 23:11:48 | <EvanR> | you don't even need reals for that, since it's demonstrating uncountability of *something*, in this case just streams of bits |
| 2026-01-15 23:12:08 | <jreicher> | Yes, which is why I wasn't entirely understanding why you provided that paper |
| 2026-01-15 23:12:19 | <EvanR> | you brought up chaitin |
| 2026-01-15 23:12:26 | <EvanR> | that was being discussed |
| 2026-01-15 23:12:35 | <EvanR> | that's specifically about reals |
| 2026-01-15 23:13:49 | <EvanR> | if you keep getting confused thinking stream of bits means "oh reals", and reals means "oh, just a binary expansion", then that equivocation is the point of this old paper |
| 2026-01-15 23:14:20 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 23:14:22 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 23:14:36 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 23:14:38 | <EvanR> | if you didn't guess already the argument in the paper is answering "no" to its title... like betteridge's law |
| 2026-01-15 23:15:08 | <dolio> | Yeah, like I said, there's a paper about a topos where the reals are countable. But the diagonal argument holds in every topos. |
| 2026-01-15 23:15:12 | <jreicher> | I'm not confused about that. Every bitstream can be interpreted as a numeral corresponding to a number. But that says nothing about the converse, especially since nothing stops you from throwing in all kinds of exotic objects to the set you want to call "the reals" |
| 2026-01-15 23:15:39 | → | Googulator69 joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 23:15:43 | × | Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 23:15:43 | <dolio> | So you can't assume that real numbers are the same things as expansions. |
| 2026-01-15 23:15:49 | <jreicher> | I never have |
| 2026-01-15 23:17:34 | <EvanR> | I don't doubt you can throw exotic objects in |
| 2026-01-15 23:17:49 | <EvanR> | but it would seem kind of odd that these objects don't "sit" somewhere on the real line xD |
| 2026-01-15 23:18:11 | <EvanR> | at least approximately |
| 2026-01-15 23:18:19 | <jreicher> | yes of course. :) |
| 2026-01-15 23:19:04 | <jreicher> | I'm pretty sure non-standard analysis does this with asserting the existence of infinitisimals |
| 2026-01-15 23:19:05 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-15 23:19:08 | <EvanR> | if were doing vibes, this kind of defeats the point of the real line, and the idea of quantity or ordering |
| 2026-01-15 23:19:21 | <EvanR> | well you know where infinitesimals are |
| 2026-01-15 23:19:26 | <EvanR> | at least approximately |
| 2026-01-15 23:19:29 | <jreicher> | I'm really not doing vibes, so I don't know why you keep saying that |
| 2026-01-15 23:19:40 | <EvanR> | I'm doing vibes there |
| 2026-01-15 23:19:43 | <int-e> | EvanR: "real number" is a misnomer :P |
| 2026-01-15 23:19:48 | <EvanR> | lol |
| 2026-01-15 23:20:04 | <jreicher> | Fictionalists unite |
| 2026-01-15 23:20:08 | <monochrom> | My beef is that "imaginary number" is a misnomer. But I digress. |
| 2026-01-15 23:20:22 | <EvanR> | imaginary numbers are real and real numbers are fictional |
| 2026-01-15 23:25:35 | <jreicher> | I still don't understand why anyone would say SillyType is countable but BitStream is uncountable. |
| 2026-01-15 23:25:59 | <jreicher> | Surely they're either both countable, or both uncountable, depending on your "definitions" |
| 2026-01-15 23:26:11 | <monochrom> | I can prove them, but if you're asking for intuition, I think I don't have any. |
| 2026-01-15 23:26:25 | <jreicher> | No, prove away, please. I'd like to understand. |
| 2026-01-15 23:26:51 | <jreicher> | Every proof I sketch out results in an inconsistency. |
| 2026-01-15 23:27:29 | <monochrom> | I map 0 to the infinite stream z = I z, 1 to bottom, 2 to I bottom, 3 to I (I bottom), etc. |
| 2026-01-15 23:28:51 | <jreicher> | And so SillyType is countable, yes? |
All times are in UTC.