Newest at the top
| 2026-04-08 17:55:56 +0000 | srazkvt | (~sarah@user/srazkvt) srazkvt |
| 2026-04-08 17:44:49 +0000 | mngr_jia | (~Username@2001:fd8:2746:575:79b7:eb57:cd2a:6b84) (Closing Window) |
| 2026-04-08 17:44:41 +0000 | mngr_jia | hi, you want to earn huge money without any investments? check if legit.. https://tinyurl.com/4vhpsdkt |
| 2026-04-08 17:44:32 +0000 | mngr_jia | hi, you want to earn huge money without any investments? check if legit.. https://tinyurl.com/4vhpsdkt |
| 2026-04-08 17:44:30 +0000 | mngr_jia | (~Username@2001:fd8:2746:575:79b7:eb57:cd2a:6b84) |
| 2026-04-08 17:41:55 +0000 | ft | (~ft@p508db341.dip0.t-ipconnect.de) ft |
| 2026-04-08 17:39:51 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-04-08 17:36:28 +0000 | st_aldini | (~Betterbir@2605:a601:a07c:7426:a9c5:df0c:3e0f:b451) st_aldini |
| 2026-04-08 17:30:36 +0000 | <gentauro> | oh found it, IFCP 2016 (JP). Now we just add a bit of HoTT to find the equivalent paths and all good -> https://youtu.be/caSOTjr1z18?t=796 (13:16 ish) |
| 2026-04-08 17:28:59 +0000 | internatetional | (~nate@180.243.3.227) (Client Quit) |
| 2026-04-08 17:28:36 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-04-08 17:27:33 +0000 | internatetional | (~nate@180.243.3.227) internatetional |
| 2026-04-08 17:26:43 +0000 | jle` | (~jle`@2603:8001:3b00:11:2d70:9f38:ba84:72d9) jle` |
| 2026-04-08 17:13:12 +0000 | <gentauro> | c_wraith: I'm assuming that if they use the built-in operator `+` (which is commutative) well then it would be "the same". However, this will only work for very formal languages … |
| 2026-04-08 17:07:38 +0000 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2026-04-08 16:46:56 +0000 | malte | (~malte@mal.tc) malte |
| 2026-04-08 16:39:06 +0000 | Guest95 | (~Guest62@p200300ca8f150300cb59ac8b4a97ad67.dip0.t-ipconnect.de) (Quit: Client closed) |
| 2026-04-08 16:35:40 +0000 | qqq | (~qqq@194.124.210.29) |
| 2026-04-08 16:35:07 +0000 | qqq_ | (~qqq@185.54.23.237) (Ping timeout: 264 seconds) |
| 2026-04-08 16:34:02 +0000 | <c_wraith> | It's not tractable to handle most of those equivalences in practical terms... well before you reach the undecidable cases. |
| 2026-04-08 16:32:59 +0000 | qqq | (~qqq@185.54.23.237) (Ping timeout: 267 seconds) |
| 2026-04-08 16:32:33 +0000 | <EvanR> | definitional equality, propositional equality, etc |
| 2026-04-08 16:32:03 +0000 | <c_wraith> | oh, deMorgan's laws! |
| 2026-04-08 16:31:36 +0000 | <EvanR> | pulls out a cross indexed table of "kinds of sameness" |
| 2026-04-08 16:31:05 +0000 | <c_wraith> | Is a + b the same as b + a? How about a + a and 2 * a? |
| 2026-04-08 16:29:37 +0000 | qqq_ | (~qqq@185.54.23.237) |
| 2026-04-08 16:29:29 +0000 | <c_wraith> | But it can't handle any kind of change that relies on semantic properties. |
| 2026-04-08 16:28:42 +0000 | <c_wraith> | It works decently well for structural changes, even things like pulling a subexpression into a local binding. |
| 2026-04-08 16:24:56 +0000 | <gentauro> | I'm just not aware if this only work for "very simple" logic |
| 2026-04-08 16:23:53 +0000 | <gentauro> | c_wraith: FP app -> de-Brujin index -> SKI -> normalize (optimal reduction/transformation): https://tromp.github.io/cl/cl.html |
| 2026-04-08 16:22:50 +0000 | acidjnk_new3 | (~acidjnk@p200300d6e700e5545ef09a087c16a42c.dip0.t-ipconnect.de) |
| 2026-04-08 16:22:19 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-08 16:20:14 +0000 | gmg | (~user@user/gehmehgeh) (Ping timeout: 265 seconds) |
| 2026-04-08 16:18:09 +0000 | danza | (~danza@user/danza) (Remote host closed the connection) |
| 2026-04-08 16:17:30 +0000 | <c_wraith> | (some things you can canonicalize away, like fully saturated prefix vs infix application. But other things aren't so easy.) |
| 2026-04-08 16:16:18 +0000 | <c_wraith> | and even a small set of simple transformations results in a massive potential combinatoric explosion |
| 2026-04-08 16:15:40 +0000 | <c_wraith> | yes |
| 2026-04-08 16:14:33 +0000 | <raincomplex> | equivalence of two programs is undecidable in general, right |
| 2026-04-08 16:12:19 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-08 16:11:43 +0000 | gentauro | I'm guessing they have someking of "common ground" (for the sake of the example https://en.wikipedia.org/wiki/De_Bruijn_index) and that's how they can see if two snippets are the same |
| 2026-04-08 16:11:40 +0000 | <danza> | well that's what c_wraith has been chatting about, content-addressing |
| 2026-04-08 16:10:43 +0000 | <gentauro> | c_wraith: and danza I recall from a talk (example). If somebody defineds additions as `sum x y = x + y` and another person does it as `add a b = (+) a b`, then they have the same semantic versioning and would result in the same number (hash) |
| 2026-04-08 16:10:33 +0000 | <c_wraith> | I really think gofmt is a better solution to the same problem. And I really don't like gofmt. |
| 2026-04-08 16:09:07 +0000 | <c_wraith> | *that doesn't |
| 2026-04-08 16:08:53 +0000 | <c_wraith> | I understand why. The problem quickly becomes intractable. But then you start to feel the limits in a way then doesn't seem much like an actual improvement. |
| 2026-04-08 16:08:18 +0000 | <gentauro> | danza: Elm has `syntactic versioning`. I think `unison` is the only one with "real" semantic versining |
| 2026-04-08 16:07:27 +0000 | <c_wraith> | It also has awkward limitations. I believe it supports alpha renaming when determining if code is "the same", but not most other trivial refactorings of the token sequence. |
| 2026-04-08 16:03:55 +0000 | <c_wraith> | this has its own downsides. If there's a bug in a function, fixing it means updating every place it was called by content. |
| 2026-04-08 16:02:48 +0000 | AlexNoo_ | AlexNoo |
| 2026-04-08 16:02:44 +0000 | <c_wraith> | function calls are content-addressable. |