Newest at the top
| 2026-03-12 19:24:48 +0100 | <ski> | (well, the version i was pondering was dependently typed, but you could also have non-dependently typed versions) |
| 2026-03-12 19:24:23 +0100 | <ski> | .. in my imagined functional language, from a while ago, you can write stuff like `m - n : Nat | m ?< n : () -| m : Nat , n : Nat', where either `m - n' or `m ?< n' is well-defined |
| 2026-03-12 19:23:54 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:23:31 +0100 | Googulator22 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:23:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:22:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:21:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:21:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:20:16 +0100 | qqq | (~qqq@185.54.22.246) |
| 2026-03-12 19:18:37 +0100 | kupi | (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2026-03-12 19:18:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:18:06 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-03-12 19:18:05 +0100 | qqq | (~qqq@185.54.22.246) (Ping timeout: 245 seconds) |
| 2026-03-12 19:18:02 +0100 | <ski> | "preimage"/"inverse image", where you start with a subset of the codomain))) |
| 2026-03-12 19:17:56 +0100 | <ski> | (also stuff like <https://en.wikipedia.org/wiki/Brzozowski_derivative> (for formal languages, and regexen). figure out how this relates to an appropriate galois connection, and how it *differs* from <https://en.wikipedia.org/wiki/Quotient_of_a_formal_language>, while it relates to "universal image" (as opposed to "existential image"/"(direct) image") of a function on a subset of its domain (cf. |
| 2026-03-12 19:17:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:17:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:16:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:16:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:15:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:13:17 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-03-12 19:13:07 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:12:20 +0100 | <ski> | exercise for the reader : figure out an appropriate galois connection for division in relational algebra, and determine what the result of dividing by the empty relation here amounts to |
| 2026-03-12 19:12:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:12:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:11:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:11:08 +0100 | <ski> | yea, i was thinking of stuff like recursive functions (a la Kleene) |
| 2026-03-12 19:10:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:10:51 +0100 | <Wygulmage> | *shudder* |
| 2026-03-12 19:10:42 +0100 | <ski> | (i've seen people define "reciprocal" of zero as zero, for similar reasons ..) |
| 2026-03-12 19:10:41 +0100 | <Wygulmage> | But of course it doesn't work for `Int`. |
| 2026-03-12 19:10:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:10:19 +0100 | <ski> | in total programming environments, people often use monus, instead of minus, just to get it totally defined |
| 2026-03-12 19:09:12 +0100 | jeremyn | (~jeremy@user/jeremyn) jeremyn |
| 2026-03-12 19:08:47 +0100 | <ski> | (and ⌜m ∸ o⌝ can be described as ⌜max 0 (m − o)⌝) |
| 2026-03-12 19:08:42 +0100 | <Wygulmage> | And conveniently it's closed for natural numbers, unlike subtraction. |
| 2026-03-12 19:07:55 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 19:07:55 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 19:07:55 +0100 | arandombit | (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 19:07:54 +0100 | <ski> | for natural numbers, monus is also called cut-off / saturated / truncated subtraction |
| 2026-03-12 19:07:37 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:07:19 +0100 | <ski> | for natural numbers (and subsets), the latter is actually an equality |
| 2026-03-12 19:06:58 +0100 | <ski> | (n + o) ∸ o ≤ n |
| 2026-03-12 19:06:44 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:06:44 +0100 | <ski> | and |
| 2026-03-12 19:06:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:06:42 +0100 | <ski> | m ≤ (m ∸ o) + o |
| 2026-03-12 19:06:27 +0100 | <ski> | two consequences (unit & counit) of that galois connection / adjunction are |