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.

翻译：我们提出一种新的合成算法，能够高效搜索包含局部变量（例如由lambda引入的变量）的程序。现有的自底向上合成算法无法评估含有自由局部变量的程序，因此无法有效缩减此类程序的搜索空间（例如使用标准观测等价性约简技术），导致合成速度缓慢。我们的算法能够缩减含局部变量程序的搜索空间。其核心思想——称为提升式解释——将程序解释过程从每次评估一个程序提升为同时评估语法中所有程序。提升式解释提供了一种机制，能够系统性地枚举局部变量的所有绑定上下文，从而实现对含局部变量程序的评估与空间约简。我们将该思想应用于网页自动化领域，由此实现的工具Arborist能够比WebRobot和Helena等最先进技术更高效地自动化处理范围更广的复杂任务。