Searching Entangled Program Spaces
summary
Introduces equality-constrained tree automata to compactly represent program spaces where subterm choices are entangled, and implements extraction and lazy, constraint-driven enumeration in the Haskell ecta library. Builds Hectare synthesizer on top of ecta and reports an average 8× speedup over Hoogle+ while using about an order of magnitude less code. Handles nonlinear equality constraints by deferring and merging choices, prunes aggressively because only ≈20% of generated runs satisfy constraints, and produces many valid typed programs efficiently.
AI-written summary · about
chapters (7)
- 0:00Introduction to Hectare
- 1:06Performance and motivation
- 2:13The EC-TA data structure
- 4:06Integrating type constraints
- 5:50Scaling with polymorphism
- 7:53Lazy enumeration algorithm
- 9:45Applications and future work
related talks
20mEquality Saturation and Joins
21mImproving Equality Saturation for EDA via Semantic E-Graphs
30megg: Fast and Extensible Equality Saturation
15mEquality Saturation Theory Exploration à la Carte
30mConstrained generation of well-typed programs
20mFast and Optimal Extraction for Sparse Equality Graphs
25mEGSTRA: E-Graph-Based Strategy for Test Suite Reduction and Abstraction
01h 07mErasure In Dependently Typed Programming