Searching Entangled Program Spaces

TL;DR

This paper introduces equality-constrained tree automata (ECTAs), a new data structure that efficiently represents large, entangled program spaces, enabling faster program synthesis in Haskell compared to existing methods.

Contribution

The paper presents ECTAs, a novel generalization of existing automata structures, along with algorithms and a Haskell library, to efficiently handle entangled subterms in program spaces.

Findings

ECTAs effectively represent entangled program spaces.

Hectare synthesizer outperforms Hoogle+ by 8x on average.

Implementation is significantly smaller yet more efficient.

Abstract

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 these programs. To find a compact representation, existing data structures exploit independence of subterms; they blow up when the choices of subterms are entangled. We introduce equality-constrained tree automata (ECTAs), a generalization of the three aforementioned data structures that can efficiently represent large spaces of programs with entangled subterms. We present efficient algorithms for extracting programs from ECTAs, implemented in a performant Haskell library, \texttt{ecta}. Using \texttt{ecta} we construct \textsc{Hectare}, a type-driven program synthesizer for Haskell. \textsc{Hectare} significantly outperforms a state-of-the-art synthesizer Hoogle+ -- providing an average speedup of 8x -- despite its implementation being an order of magnitude smaller.