Equivalence by Canonicalization for Synthesis-Backed Refactoring
summary
Presents equivalence by canonicalization: run compiler-style syntactic transforms (deforestation, partial evaluation) on both direct and combinator sketches, then use higher-order unification to prove semantic equivalence. Implements the framework as Cobbler, targets Elm combinators and Python→NumPy, and evaluates on thousands of real programs. Median synthesis time is about 0.5s; human evaluators prefer refactorings for nonrecursive cases ~25% and lists ~50%; NumPy outputs beat vanilla Python by ~2x at very large inputs (≈1e8) and become faster by ~1e6.
AI-written summary · about
chapters (13)
- 0:00Equivalence by canonicalization
- 0:21Pattern matching vs combinators
- 2:27Formal problem statement
- 3:49Limitations of I/O examples
- 4:30Syntactic equivalence limits
- 6:58Component-based refactoring
- 8:00Canonicalization properties
- 10:49Generalizing equivalence for sketches
- 11:30Comparing canonicalization functions
- 12:31Practical evaluation with Cobbler
- 14:34Cobbler tips and performance
- 15:16Key takeaways
- 15:39Q&A
related talks
21mChecking Equivalence in a Non-strict Language
01h 05mFrom meta frameworks and transformations to distributed computing and more
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
31mLetting users do the undecidable: lessons from program synthesis
13mProgramming with a Read-Eval-Synth Loop
15mLanguage-Parametric Reference Synthesis
37mA Tour of Program Optimization