论文标题
COQ表示之间的务实同构证明：向Lambda期限申请
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
论文作者
论文摘要
有几种方法可以用类型理论（例如Coq的依赖性类型理论）正式代表数据家族，例如lambda术语。数学表示非常紧凑，通常依赖于依赖类型的使用，但是在实践中它们往往很难处理。相反，基于较大（和简单的）数据结构与限制属性相结合的实现更容易处理。 在这项工作中，我们研究了几个与lambda术语有关的家庭，其中包括lambda术语骨骼，可闭合的motzkin树，与封闭的lambda术语相对应，以及一个开放式lambda术语的参数化家族。对于这些家庭中的每个家庭，我们都定义了两个不同的表示，表明它们是同构的，并提供了从一个表示转换为另一个表示的工具。所有这些数据型及其相关的转换均在COQ证明助手中实现。此外，我们使用QuickChick插件为每个表示形式实现随机生成器。
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are very compact ones and usually rely on the use of dependent types, but they tend to be difficult to handle in practice. On the contrary, implementations based on a larger (and simpler) data structure combined with a restriction property are much easier to deal with. In this work, we study several families related to lambda terms, among which Motzkin trees, seen as lambda term skeletons, closable Motzkin trees, corresponding to closed lambda terms, and a parameterized family of open lambda terms. For each of these families, we define two different representations, show that they are isomorphic and provide tools to switch from one representation to another. All these datatypes and their associated transformations are implemented in the Coq proof assistant. Furthermore we implement random generators for each representation, using the QuickChick plugin.
