论文标题
搜索纠缠的程序空间
Searching Entangled Program Spaces
论文作者
论文摘要
许多问题域，包括程序综合和基于基于的优化的优化，都需要搜索天文学的程序空间。现有的方法通常依赖于构建专业数据结构（版本空间代数，有限树自动机或电子图表）来紧凑地表示这些程序。为了找到紧凑的表示，现有数据结构利用了中断的独立性；当子选择纠缠时，它们会炸毁。我们介绍了相等约束的树自动机（ECTA），这是对上述三个数据结构的概括，这些数据结构可以有效地代表具有纠缠较高的较大的程序。我们提出了从ECTA中提取程序的有效算法，该算法是在表演者Haskell库中实现的，\ texttt {ecta}。使用\ texttt {ecta}我们构造了haskell的类型驱动程序合成器。 \ textsc {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 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.
