Program synthesis by type-guided abstraction refinement
Program synthesis by type-guided abstraction refinement
复制标题
通过类型引导的抽象细化进行程序合成
DOI：
10.1145/3371080
复制
发表时间：
2020
影响因子：
--
通讯作者：
Polikarpova, Nadia
中科院分区：
文献类型：
--
作者：
Guo, Zheng;James, Michael;Justo, David;Zhou, Jiaxiao;Wang, Ziteng;Jhala, Ranjit;Polikarpova, Nadia
我们考虑的问题，类型导向的组件为基础的合成，给定一组（类型化）组件和一个查询类型，目标是合成aterm居住的查询。基于直觉逻辑中的证明搜索的经典方法不能扩展到现代语言的标准库，后者跨越数百或数千个组件。最近为Java提出的基于图可达性的方法确实可以扩展，但仅适用于单态数据和组件：多态数据和组件无限地扩展了必须搜索的图的大小，使合成变得难以处理。我们介绍了类型引导抽象细化（TYGAR），一种新的方法，可扩展的类型导向合成多态数据库和组件。我们的主要观点是，我们可以通过构建一个抽象类型的图来克服爆炸，抽象类型代表了一组潜在的无界具体类型。我们展示了如何使用图的可达性来搜索抽象类型上的候选项，并介绍了一种新的算法，该算法使用病态候选项的不可类型性证明来迭代地细化抽象，直到找到一个良好类型的结果。我们已经在H+中实现了TYGAR，H+是一个以一组Haskell库和一个查询类型作为输入的工具，并返回一个Haskell术语，该术语使用所提供的库中的函数来实现查询类型。我们对多态性的支持允许H+处理高阶函数和类型类，并由于参数性而实现更精确的查询。我们使用一组流行的Haskell库对44个查询进行了H+评估，其中共有291个组件。H+在44个查询中的32个查询的前五个结果中返回一个有趣的解决方案。我们的研究结果表明，TYGAR允许H+快速返回良好类型的术语，首次解决方案的平均时间仅为1.4秒。此外，我们观察到，从迭代细化穷举的收益更明显的更难查询。
We consider the problem of type-directed component-based synthesis where, given a set of (typed) components and a querytype, the goal is to synthesize atermthat inhabits the query. Classical approaches based on proof search in intuitionistic logics do not scale up to the standard libraries of modern languages, which span hundreds or thousands of components. Recent graph reachability based methods proposed for Java do scale, but only apply to monomorphic data and components: polymorphic data and components infinitely explode the size of the graph that must be searched, rendering synthesis intractable. We introducetype-guided abstraction refinement(TYGAR), a new approach for scalable type-directed synthesis over polymorphic datatypes and components. Our key insight is that we can overcome the explosion by building a graph overabstract typeswhich represent a potentially unbounded set of concrete types. We show how to use graph reachability to search for candidate terms over abstract types, and introduce a new algorithm that usesproofs of untypeabilityof ill-typed candidates to iterativelyrefinethe abstraction until a well-typed result is found.We have implemented TYGAR in H+, a tool that takes as input a set of Haskell libraries and a query type, and returns a Haskell term that uses functions from the provided libraries to implement the query type. Our support for polymorphism allows H+ to work with higher-order functions and type classes, and enables more precise queries due to parametricity. We have evaluated H+ on 44 queries using a set of popular Haskell libraries with a total of 291 components. H+ returns an interesting solution within the first five results for 32 out of 44 queries. Our results show that TYGAR allows H+ to rapidly return well-typed terms, with the median time to first solution of just 1.4 seconds. Moreover, we observe that gains from iterative refinement over exhaustive enumeration are more pronounced on harder queries.
登录
查看更多内容
DOI：
10.1007/978-3-540-73589-2_2
发表时间：
2007-07
期刊：
--
影响因子：
--
作者：
Jeremy G. Siek;Walid Taha
通讯作者：
Jeremy G. Siek;Walid Taha
抽象渐进式打字
DOI：
--
发表时间：
2016
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Ronald Garcia;Alison M. Clark;É. Tanter
通讯作者：
É. Tanter
影响因子：
--
作者：
Xinyu Wang;Işıl Dillig;Rishabh Singh
通讯作者：
Xinyu Wang;Işıl Dillig;Rishabh Singh
神灵
DOI：
10.2307/j.ctv1ccbggs.36
发表时间：
2019
期刊：
Hand Over Mouth Music
影响因子：
--
作者：
D. Alvarez
通讯作者：
D. Alvarez
理论与实践中的模块化、高阶基数分析
DOI：
10.1145/2535838.2535861
发表时间：
2014
期刊：
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Ilya Sergey;Dimitrios Vytiniotis;S. Jones
通讯作者：
S. Jones