Random Generators for Dependent Types
Random Generators for Dependent Types
复制标题
相关类型的随机生成器
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
M. Takeyama
中科院分区：
文献类型：
--
作者：
P. Dybjer;Qiao Haiyan;M. Takeyama
我们展示了如何在相依类型理论中为几类不同的归纳定义类型编写满射随机生成元。我们讨论非索引(简单)类型和索引族类型。特别是，我们展示了如何使用索引归纳定义和逻辑程序之间的关系：类型族的索引归纳定义对应于逻辑程序，而生成族中某一类型的对象对应于求解对逻辑程序的查询。作为一个例子，我们展示了如何通过随机化Prolog搜索算法来编写命题逻辑中定理的满射随机生成器。
We show how to write surjective random generators for several different classes of inductively defined types in dependent type theory. We discuss both non-indexed (simple) types and indexed families of types. In particular we show how to use the relationship between indexed inductive definitions and logic programs: the indexed inductive definition of a type family corresponds to a logic program, and generating an object of a type in the family corresponds to solving a query for the logic program. As an example, we show how to write a surjective random generator for theorems in propositional logic by randomising the Prolog search algorithm.