Merging Inductive Relations
Merging Inductive Relations
复制标题
合并归纳关系
DOI：
10.1145/3591292
复制
发表时间：
2023
影响因子：
--
通讯作者：
Lampropoulos, Leonidas
中科院分区：
文献类型：
--
作者：
Prinz, Jacob;Lampropoulos, Leonidas
归纳关系提供了一种强大且富有表现力的编写程序规范的方式，同时促进组合推理。 它们被证明助理用户广泛使用，使其成为诸如 QuickChick 等证明工程工具特别有吸引力的目标，QuickChick 是 Coq 的基于属性的测试工具，可以自动导出满足归纳关系的值的生成器。 然而，虽然这样的生成器通常是高效的，但存在一种罕见但似乎不可避免的情况，即它们的性能大大降低：当多个归纳关系约束同一个数据时。在本文中，我们介绍了一种算法，用于合并两个共享索引的归纳定义属性。该算法找到两个关系之间的共享结构，并创建一个可证明等价于两者的合取的合并关系。 我们通过一系列案例研究证明，合并关系可以将自动生成的性能提高几个数量级，并且通过消除嵌套归纳和繁琐的低级簿记的需要来简化机械化证明。
Inductive relations offer a powerful and expressive way of writing program specifications while facilitating compositional reasoning. Their widespread use by proof assistant users has made them a particularly attractive target for proof engineering tools such as QuickChick, a property-based testing tool for Coq which can automatically derive generators for values satisfying an inductive relation. However, while such generators are generally efficient, there is an infrequent yet seemingly inevitable situation where their performance greatly degrades: when multiple inductive relations constrain the same piece of data.In this paper, we introduce an algorithm for merging two such inductively defined properties that share an index. The algorithm finds shared structure between the two relations, and creates a single merged relation that is provably equivalent to the conjunction of the two. We demonstrate, through a series of case studies, that the merged relations can improve the performance of automatic generation by orders of magnitude, as well as simplify mechanized proofs by getting rid of the need for nested induction and tedious low-level book-keeping.
登录
查看更多内容
做出随机判断：根据类型系统的定义自动生成类型良好的术语
DOI：
--
发表时间：
2015
期刊：
European Symposium on Programming
影响因子：
--
作者：
B. Fetscher;Koen Claessen;Michal H. Palka;John Hughes;R. Findler
通讯作者：
R. Findler
使用装饰品编程
影响因子：
1.1
作者：
Hsiang;J. Gibbons
通讯作者：
J. Gibbons
伊莎贝尔的新快速检查 - 一站式随机、详尽和符号测试
DOI：
10.1007/978-3-642-35308-6_10
发表时间：
2012
期刊：
影响因子：
--
作者：
Lukas Bulwahn
通讯作者：
Lukas Bulwahn
一阶测试数据的属性定向生成
DOI：
--
发表时间：
2007
期刊：
Symposium on Trends in Functional Programming
影响因子：
--
作者：
Fredrik Lindblad
通讯作者：
Fredrik Lindblad
Agda 中的依赖类型编程
DOI：
--
发表时间：
2009
期刊：
ACM SIGPLAN International Workshop on Types In Languages Design And Implementation
影响因子：
--
作者：
U. Norell
通讯作者：
U. Norell