一句话：提出等式约束树自动机（ECTA）以紧凑表示子项选择相互纠缠的程序空间，并据此实现高性能 Haskell 合成器 Hectare。
程序合成与基于重写的优化等问题往往需要在天文数字规模的程序空间中搜索。已有方法依赖版本空间代数、有限树自动机、e-graph 等专用数据结构来紧凑表示这些空间，但它们本质上都利用了子项的独立性，因而无法高效表示子项选择相互纠缠的复杂程序空间。本文提出等式约束树自动机（equality-constrained tree automata, ECTA），一种可紧凑表示带纠缠子项的大规模程序空间的新数据结构，并给出从 ECTA 中抽取程序的高效算法，实现为性能良好的 Haskell 库 ecta。基于该库，作者构建了面向 Haskell 的类型驱动程序合成器 Hectare。实验表明，Hectare 显著优于最先进的合成器 Hoogle+，平均加速达 8 倍，而其实现代码量却小一个数量级。
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.
@article{paperbot1487,
title = {Searching entangled program spaces},
author = {James Koppel and Zheng Guo and Edsko de Vries and Armando Solar-Lezama and Nadia Polikarpova},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547622}
}