Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations of Functional Programs
Thomas Koehler, Phil Trinder, Michel Steuwer

TL;DR
This paper introduces sketch-guided equality saturation, a technique that enables scalable and efficient optimization of complex functional programs by incorporating programmer-provided sketches to guide rewrite sequences.
Contribution
It presents novel encoding methods for polymorphically typed lambda calculi and a semi-automatic sketch-guided approach to scale equality saturation for complex optimizations.
Findings
Efficient lambda calculus encoding reduces runtime and memory by orders of magnitude.
Unguided equality saturation struggles with complex optimizations, only finding simple ones.
Sketch-guided approach finds all seven complex matrix multiplication optimizations quickly and with minimal resources.
Abstract
Generating high-performance code for diverse hardware and application domains is challenging. Functional array programming languages with patterns like map and reduce have been successfully combined with term rewriting to define and explore optimization spaces. However, deciding what sequence of rewrites to apply is hard and has a huge impact on the performance of the rewritten program. Equality saturation avoids the issue by exploring many possible ways to apply rewrites, efficiently representing many equivalent programs in an e-graph data structure. Equality saturation has some limitations when rewriting functional language terms, as currently naive encodings of the lambda calculus are used. We present new techniques for encoding polymorphically typed lambda calculi, and show that the efficient encoding reduces the runtime and memory consumption of equality saturation by orders of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Logic, programming, and type systems · Software Engineering Research
