一句话：提出 lifted interpretation，使自底向上合成能高效搜索含局部变量（如 lambda）的程序，并实现 Web 自动化工具 Arborist。
本文研究含局部变量（例如 lambda 引入的变量）的程序合成问题。已有自底向上合成算法无法评估带有自由局部变量的程序，因此难以利用观察等价等标准约简技术来缩小搜索空间，导致合成效率低下。作者提出一种新的合成算法，其核心思想是 lifted interpretation：将程序解释过程从一次评估一个程序，提升为同时评估文法生成的所有程序。该机制能够系统性地枚举局部变量的绑定上下文，从而支持对这类程序进行评估并约简搜索空间。作者将方法实例化到 Web 自动化领域，实现了工具 Arborist。实验表明，Arborist 能比 WebRobot、Helena 等前沿技术更高效地自动完成更广泛且更具挑战性的任务。
We propose a new synthesis algorithm that can efficiently search programs with local variables (e.g., those introduced by lambdas). Prior bottom-up synthesis algorithms are not able to evaluate programs with free local variables , and therefore cannot effectively reduce the search space of such programs (e.g., using standard observational equivalence reduction techniques), making synthesis slow. Our algorithm can reduce the space of programs with local variables. The key idea, dubbed lifted interpretation , is to lift up the program interpretation process, from evaluating one program at a time to simultaneously evaluating all programs from a grammar. Lifted interpretation provides a mechanism to systematically enumerate all binding contexts for local variables, thereby enabling us to evaluate and reduce the space of programs with local variables. Our ideas are instantiated in the domain of web automation. The resulting tool, Arborist , can automate a significantly broader range of challenging tasks more efficiently than state-of-the-art techniques including WebRobot and Helena.
@article{paperbot2595,
title = {Efficient Bottom-Up Synthesis for Programs with Local Variables},
author = {Xiang Li and Xiangyu Zhou and Rui Dong and Yihong Zhang and Xinyu Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632894}
}