Timeline for How to ensure coherent choices of representatives in an e-graph?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 26, 2023 at 22:25 | vote | accept | kaya3 | ||
| Sep 19, 2023 at 15:07 | answer | added | Erik Eidt | timeline score: 5 | |
| Sep 18, 2023 at 21:46 | answer | added | rpjohnst | timeline score: 5 | |
| Sep 18, 2023 at 17:04 | comment | added | Alexis King♦ | @rpjohnst That sounds like an answer, not a comment—please post it as one! | |
| Sep 18, 2023 at 16:29 | comment | added | Corbin |
In practice, you'd have a local type context, and you'd commit to one of the possible types prior to extraction; then, type-guided extraction is possible (at least egg supports this...) However, the only way to know which commitment is more efficient would be to perform two extractions and compare their cost, which would lead to combinatorial explosion. I can write a complete answer later, if nobody else gets to it.
|
|
| Sep 18, 2023 at 2:03 | comment | added | rpjohnst | Well, phrased the other way, it can be performed using e-graphs if and only if you can organize the language in such a way that these rewrites are "local" and preserve congruence. (If I knew of an obvious way to do this or reason that it was impossible, I would have written an answer- short of that, I'm just pointing to the relevant invariant.) | |
| Sep 17, 2023 at 20:03 | comment | added | kaya3 | @rpjohnst Sure ─ so how can this kind of optimisation be performed correctly using e-graphs? Or can it not? | |
| Sep 17, 2023 at 17:37 | comment | added | rpjohnst |
A valid e-graph has a "congruence invariant," which means that an equivalence between x and y must also imply an equivalence between f(x) and f(y). Performing these rewrites (set() => 0, set.add(x) => set | (1 << x), etc) each individually violates this invariant and so is incompatible with e-graphs in this form.
|
|
| Sep 17, 2023 at 9:58 | history | asked | kaya3 | CC BY-SA 4.0 |