Contextual Equality Saturation
summary
Extends equality saturation so rewriting can occur under local branch assumptions, replacing costly swap laws with contextual rewriting rules that match a conditional source and a structural occurrence and rewrite in one step. Introduces cyclic e-graphs with contextual annotations to record paths from condition to branch and to fail fast when no match exists. Prototype implements both strategies for equivalence checking on synthesized benchmarks and runs about ~30% faster while keeping soundness.
AI-written summary · about
chapters (10)
- 0:00Contextual equality saturation
- 1:06Equality saturation basics
- 3:15Program reasoning with equality
- 3:56Conditional transformations problem
- 6:46Swapping rules limitations
- 8:32Contextual rewriting rules
- 10:59Efficient rule application
- 12:24Experimental evaluation
- 13:07Future research
- 13:57Q&A
related talks
30megg: Fast and Extensible Equality Saturation
26mTowards Efficient Model Comparison Using Automated Program Rewriting
01h 06m“Value Semantics: It ain't about the syntax!, Part II"
44mUnconditional Code
01h 16mVerifying, Inferring and Exploiting Code Commutativity
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
15mStrategic Tree Rewriting in Attribute Grammars
01h 05mVerifying Infinitely Many Programs at Once