Computing correctly with inductive relations-猫眼课题宝

利用归纳关系正确计算

DOI：

10.1145/3519939.3523707

发表时间：

2022

期刊：

Programming Language Design and Implementation

影响因子：

通讯作者：

中科院分区：

文献类型：

作者：

Paraskevopoulou, Zoe;Eline, Aaron;Lampropoulos, Leonidas

归纳关系是机械化证明开发中编写规范的主要方式。与纯功能性规范相比，它们具有更强的表达能力，并促进了更多的组合推理。然而，归纳关系也有一个显着的缺点：它们不能用于computation.In本文中，我们提出了一个统一的框架提取三种不同类型的计算内容从归纳定义的关系：半决策程序，枚举，和随机生成器。我们展示了如何三个不同的实例化相同的算法可以用来生成所有三类的计算定义内的逻辑的Coq证明助理。对于每个派生的计算，我们也得到机械化的证明，它是健全的和完整的原始归纳关系，使用Ltac2，Coq的新的元编程facility.We实现我们的框架上的QuickChick测试工具Coq的顶部，并证明它涵盖了大多数情况下的利益提取计算的归纳关系中发现的软件基础系列。最后，我们评估的实用性和效率，我们的方法与小的案例研究，随机属性为基础的测试和证明计算反射。

Inductive relations are the predominant way of writing specifications in mechanized proof developments. Compared to purely functional specifications, they enjoy increased expressive power and facilitate more compositional reasoning. However, inductive relations also come with a significant drawback: they can’t be used for computation.In this paper, we present a unifying framework for extracting three different kinds of computational content from inductively defined relations: semi-decision procedures, enumerators, and random generators. We show how three different instantiations of the same algorithm can be used to generate all three classes of computational definitions inside the logic of the Coq proof assistant. For each derived computation, we also derive mechanized proofs that it is sound and complete with respect to the original inductive relation, using Ltac2, Coq’s new metaprogramming facility.We implement our framework on top of the QuickChick testing tool for Coq, and demonstrate that it covers most cases of interest by extracting computations for the inductive relations found in the Software Foundations series. Finally, we evaluate the practicality and the efficiency of our approach with small case studies in randomized property-based testing and proof by computational reflection.