Universes for Generic Programs and Proofs in Dependent Type Theory
Universes for Generic Programs and Proofs in Dependent Type Theory
复制标题
依赖类型理论中的泛型程序和证明的宇宙
DOI：
10.5555/985799.985801
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Patrik Jansson
中科院分区：
文献类型：
--
作者：
Marcin Benke;P. Dybjer;Patrik Jansson
我们展示了如何在Martin-Lof类型理论中编写通用程序和证明。为此，我们考虑了Martin-Lof的逻辑类型逻辑框架的几个扩展。每个扩展名都有一个代码（签名）的宇宙，用于归纳定义的集合，并具有通用的形成，简介，消除和平等规则。这些扩展是在Dybjer和Setzer有限的诱导回复定义理论上建模的，该理论还具有集合的代码，以及通用形成，简介，消除和平等规则。在这里，我们考虑了几个较小的通用编程和通用代数兴趣宇宙。我们正式化了单排和多排序的项代数，以及迭代，广义，参数化和索引的归纳定义。我们还展示了如何将通用编程技术扩展到这些宇宙。此外，我们给出了通用平等测试的反射性和替代性的通用证据：本文中的大多数定义都是使用证明助手ALFA实施了依赖类型理论的。
We show how to write generic programs and proofs in Martin-Lof type theory. To this end we consider several extensions of Martin-Lof's logical framework for dependent types. Each extension has a universe of codes (signatures) for inductively defined sets with generic formation, introduction, elimination, and equality rules. These extensions are modeled on Dybjer and Setzer's finitely axiomatized theories of inductive-recursive definitions, which also have universes of codes for sets, and generic formation, introduction, elimination, and equality rules. Here we consider several smaller universes of interest for generic programming and universal algebra. We formalize one-sorted and many-sorted term algebras, as well as iterated, generalized, parameterized, and indexed inductive definitions. We also show how to extend the techniques of generic programming to these universes. Furthermore, we give generic proofs of reflexivity and substitutivity of a generic equality test: Most of the definitions in the paper have been implemented using the proof assistant Alfa for dependent type theory.