An induction principle for nested datatypes in intensional type theory
An induction principle for nested datatypes in intensional type theory
复制标题
DOI：
10.1017/s095679680900731x
复制
发表时间：
2009-05-01
影响因子：
1.1
通讯作者：
Matthes, Ralph
中科院分区：
文献类型：
--
作者：
Matthes, Ralph
嵌套数据库是在所有类型上索引的数据库家族，这样构造函数可以关联不同的家族成员（与同构列表不同）。此外，构造函数的参数类型引用了由表达式给出的索引，其中家族名称可能出现。特别是在这种真正的嵌套情况下，遍历这些数据结构的函数的终止性远不是显而易见的。与A. Abel and I Uustalu（英语：Abel and I Uustalu）Comput.科学，333（1-2），2005年，第333页。3-66）提出的迭代方案，保证终止不是由结构要求，但只是多态性。它们是通用的，因为不需要底层数据类型“functor”的特定语法形式。然而，没有归纳原则的验证程序，从而获得，虽然他们是众所周知的初始代数油endofunctor范畴的代数模型。新的贡献是在内涵类型理论中（更具体地说，在归纳构造的演算中）表示嵌套数据集，它仍然是通用的，并且覆盖了真正的嵌套，保证了所有可表达程序的终止，并且具有所有的归纳原理，允许证明单调性证人（嵌套数据集的映射）的函数性和迭代定义的多态函数的自然属性。
Nested datatypes are families of datatypes that are indexed over all types such that the constructors may relate different family members (unlike the homogeneous lists). Moreover, the argument types of the constructors refer to indices given by expressions ill which the family name may occur. Especially ill this case of true nesting, termination of functions that traverse these data structures is far from being obvious. A joint paper with A. Abel and I Uustalu (Theor. Comput. Sci., 333 (1-2), 2005, pp. 3-66) proposed iteration schemes that guarantee termination not by structural requirements but just by polymorphic typing. They are generic in the sense that no specific syntactic form of the underlying datatype "functor" is required. However, there was no induction principle for the verification of the programs thus obtained, although they are well known in the Usual model of initial algebras oil endofunctor categories. The new contribution is a representation of nested datatypes in intensional type theory (more specifically, in the calculus of inductive constructions) that is still generic and covers true nesting, guarantees termination of all expressible programs, and has all induction principle that allows to prove functoriality of monotonicity witnesses (maps for nested datatypes) and naturality properties of iteratively defined polymorphic functions.