IRCBrowse

2026/03/12

Newest at the top

2026-03-12 19:33:17 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:33:16 +0100Googulator22(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 19:33:10 +0100someb(~someb@24.42.43.79) ()
2026-03-12 19:32:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:32:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:31:56 +0100 <ski> someb : don't ask to ask, just ask
2026-03-12 19:31:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:31:41 +0100wbrawner(~wbrawner@129.146.105.153) wbrawner
2026-03-12 19:31:40 +0100 <ski> Wygulmage : the version i showed above
2026-03-12 19:31:02 +0100 <someb> anyone online?
2026-03-12 19:30:57 +0100 <someb> hello?
2026-03-12 19:30:39 +0100someb(~someb@24.42.43.79)
2026-03-12 19:29:55 +0100 <Wygulmage> (I'm reading up on Brzozowski derivatives and quotients of formal languages.)
2026-03-12 19:29:45 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-03-12 19:29:15 +0100 <Wygulmage> What would a non-dependently typed version look like?
2026-03-12 19:28:49 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:28:05 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:28:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:27:22 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:26:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:26:26 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
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 +0100Googulator53(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 19:23:31 +0100Googulator22(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:23:29 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:22:45 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:22:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:22:02 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:21:38 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:21:06 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:20:16 +0100qqq(~qqq@185.54.22.246)
2026-03-12 19:18:37 +0100kupi(uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2026-03-12 19:18:09 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:18:06 +0100peterbecich(~Thunderbi@71.84.33.135) peterbecich
2026-03-12 19:18:05 +0100qqq(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:17:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:16:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:16:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:15:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:13:17 +0100arandombit(~arandombi@user/arandombit) (Ping timeout: 268 seconds)
2026-03-12 19:13:07 +0100AlexNoo__(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:12:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:11:22 +0100AlexNoo(~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)