Signatures and Induction Principles for Higher Inductive-Inductive Types
Signatures and Induction Principles for Higher Inductive-Inductive Types
复制标题
更高电感-电感类型的签名和感应原理
DOI：
10.23638/lmcs-16(1:10)2020
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
A. Kovács
中科院分区：
文献类型：
--
作者：
A. Kaposi;A. Kovács
高归纳型（HIITs）从两个方面概括了依赖型理论的归纳型。一方面，它们允许同时定义多个排序，这些排序可以在彼此之上建立索引。另一方面，它们支持相等构造函数，从而推广了同伦类型论的高归纳类型。利用这两种特性的例子是柯西实数和类型理论的良好类型语法，其中转换规则作为等式构造函数给出。本文利用一个小类型理论——签名理论，提出了hiit的一般定义。该理论中的上下文通过列出构造函数来编码HIIT。通过使用语法逻辑关系转换的变体，我们还计算了hiit的归纳和递归概念。建立完整的范畴语义和构造初始代数是未来的工作。HIIT签名理论在Agda中正式形式化，并进行了语法翻译。我们还提供了一个Haskell实现，它将签名作为输入，并将翻译结果作为有效的Agda代码输出。
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
DOI：
10.1145/2837614.2837638
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Thorsten Altenkirch;A. Kaposi
通讯作者：
Thorsten Altenkirch;A. Kaposi
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter
整数作为更高归纳类型
DOI：
10.1145/3373718.3394760
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Altenkirch T
通讯作者：
Altenkirch T