Searching entangled program spaces

• DOI: 10.1145/3547622
• Publication Date: 2022-08-31T19:39:26Z
• Authors: James Koppel; Zheng Guo; Edsko de Vries; Armando Solar-Lezama; Nadia Polikarpova
• Keywords: FOS: Computer and information sciences; Computer Science - Programming Languages; 0202 electrical engineering, electronic engineering, information engineering; 02 engineering and technology; Programming Languages (cs.PL)

Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures—version-space algebras, finite tree automata, or e-graphs—to compactly represent such spaces. At their core, all these data structures exploit independence of subterms; as a result, they cannot efficiently represent more complex program spaces, where the choices of subterms are entangled.

We introduce equality-constrained tree automata (ECTAs), a new data structure, designed to compactly represent large spaces of programs with entangled subterms. We present efficient algorithms for extracting programs from ECTAs, implemented in a performant Haskell library, ecta. Using the ecta library, we construct Hectare, a type-driven program synthesizer for Haskell. Hectare significantly outperforms a state-of-the-art synthesizer Hoogle+—providing an average speedup of 8×—despite its implementation being an order of magnitude smaller.