Newest at the top
| 2024-04-29 22:29:39 +0200 | <tomsmeding> | (which I why I responded :p) |
| 2024-04-29 22:29:33 +0200 | <tomsmeding> | I don't myself, but I have a highlight on 'accelerate' here on irc |
| 2024-04-29 22:29:19 +0200 | <shapr> | neato |
| 2024-04-29 22:29:11 +0200 | <tomsmeding> | I share my office at the university with two PhDs who work on accelerate almost full-time :p |
| 2024-04-29 22:28:35 +0200 | <shapr> | tomsmeding: oh, I didn't know you did your master's thesis on accelerate |
| 2024-04-29 22:27:01 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-04-29 22:26:51 +0200 | <shapr> | I can't do much in <15 minutes |
| 2024-04-29 22:26:38 +0200 | <tomsmeding> | which is not anything deep; egraphs are just more complex, I also cannot write a red-black tree in <15 minutes |
| 2024-04-29 22:26:02 +0200 | <tomsmeding> | I cannot at all say the same for egraphs |
| 2024-04-29 22:25:54 +0200 | <tomsmeding> | I can write a passable UF implementation in <15 minutes |
| 2024-04-29 22:25:26 +0200 | <dolio> | Trickier than union-find? |
| 2024-04-29 22:25:08 +0200 | <tomsmeding> | yes |
| 2024-04-29 22:24:58 +0200 | flounders | (~flounders@24.246.176.178) |
| 2024-04-29 22:24:55 +0200 | <monochrom> | We also need a monoid-good group. :) |
| 2024-04-29 22:24:03 +0200 | <tomsmeding> | aren't we in there? |
| 2024-04-29 22:23:59 +0200 | <tomsmeding> | :D |
| 2024-04-29 22:23:54 +0200 | <tomsmeding> | egraphs are trickier, but also more powerful |
| 2024-04-29 22:23:54 +0200 | <monochrom> | Yeah I'm being sarcastic. Oh we missed the opportunity to form a function-programming-good group too! Oh wait... >:) |
| 2024-04-29 22:23:38 +0200 | <tomsmeding> | though you can implement UF in like <20 lines of code if you're careful |
| 2024-04-29 22:23:16 +0200 | <tomsmeding> | the same cannot be said for egraphs |
| 2024-04-29 22:23:12 +0200 | <tomsmeding> | I think most academically trained programmers know of the existence of UF |
| 2024-04-29 22:22:43 +0200 | <monochrom> | Hrm, I guess people who liked union-find missed the opportunity to form a union-find-good group. |
| 2024-04-29 22:22:41 +0200 | <tomsmeding> | all of the commutative properties that are uninteresting but will come out of that |
| 2024-04-29 22:22:24 +0200 | <tomsmeding> | after you filter out the useless stuff |
| 2024-04-29 22:22:18 +0200 | <tomsmeding> | this discovered equivalence approach is not an automated testing method, but if you're lucky the synthesised equivalences could I guess be sufficiently abstract that it might genuinely tell you something useful |
| 2024-04-29 22:21:38 +0200 | <shapr> | :-) |
| 2024-04-29 22:21:31 +0200 | <tomsmeding> | some people working on egraphs and saying that they're good |
| 2024-04-29 22:21:15 +0200 | <tomsmeding> | e-graphs-good |
| 2024-04-29 22:21:11 +0200 | <tomsmeding> | it's an interesting way to do things, I hadn't thought about that |
| 2024-04-29 22:21:09 +0200 | <monochrom> | What is the egg group? |
| 2024-04-29 22:20:40 +0200 | <shapr> | probably :-) |
| 2024-04-29 22:20:23 +0200 | <tomsmeding> | a human looks at those discovered equivalences and thinks hard about whether they make sense? |
| 2024-04-29 22:20:20 +0200 | <shapr> | then it uses those to build an equivalence graph |
| 2024-04-29 22:20:08 +0200 | <tomsmeding> | and then? |
| 2024-04-29 22:20:01 +0200 | <tomsmeding> | I see |
| 2024-04-29 22:19:59 +0200 | <shapr> | yup |
| 2024-04-29 22:19:56 +0200 | <tomsmeding> | based on seeing whether your compiler produces the same output for them? |
| 2024-04-29 22:19:47 +0200 | <shapr> | brute force from what I read |
| 2024-04-29 22:19:44 +0200 | <shapr> | based on trying a bunch of things |
| 2024-04-29 22:19:38 +0200 | <tomsmeding> | based on what? :p |
| 2024-04-29 22:19:33 +0200 | <shapr> | I think in source programs |
| 2024-04-29 22:19:26 +0200 | <tomsmeding> | source programs? target programs? |
| 2024-04-29 22:19:21 +0200 | <tomsmeding> | equivalences in what |
| 2024-04-29 22:19:13 +0200 | <shapr> | the egg group has a tool that discovers equivalences for you |
| 2024-04-29 22:19:08 +0200 | <tomsmeding> | if you have semantics (interpreters) for source and target languages you can do model testing (a subset of PBT), i.e. generate source programs and test that interpret_src == interpret_tgt . compile |
| 2024-04-29 22:18:18 +0200 | <tomsmeding> | maybe if your languages are easy toy languages writing an interpreter for them is easy |
| 2024-04-29 22:17:55 +0200 | <tomsmeding> | which is not much easier than writing a compiler in the first place |
| 2024-04-29 22:17:45 +0200 | <tomsmeding> | but then you need to define full semantics again |
| 2024-04-29 22:17:32 +0200 | <tomsmeding> | s/, and an external proof that/and then test that/ |
| 2024-04-29 22:17:23 +0200 | <tomsmeding> | er |