高归纳-归纳类型的签名和归纳原理
摘要：高阶归纳递归类型（HIITs）在两个方面推广了依赖类型理论中的归纳类型。一方面，它们允许同时定义多个可以相互索引的排序。另一方面，它们支持等式构造器，从而推广了同伦类型理论中的高阶归纳类型。同时使用这两个特征的示例包括Cauchy实数和类型理论中的类型化语法，其中给出的转换规则作为等式构造器。在本文中，我们提出了使用小型类型理论（称为签名理论）对HIITs进行一般定义。在该理论中，上下文通过列出构造器来对HIIT进行编码。我们还通过使用语法逻辑关系翻译的变体来计算HIIT的归纳和递归的概念。完整的范畴语义的构建和初始代数的构造留待将来工作。HIIT签名理论已经在Agda中进行了形式化，并附带了语法翻译。我们还提供了一个Haskell实现，该实现将签名作为输入，并将翻译结果作为有效的Agda代码输出。
作者：Ambrus Kaposi, Andr''as Kov''acs
论文ID：1902.00297
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22