Indexed containers
Indexed containers
复制标题
DOI：
10.1017/s095679681500009x
复制
发表时间：
2015-01-01
影响因子：
1.1
通讯作者：
Morris, Peter
中科院分区：
文献类型：
--
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
我们表明，严格积极家庭的句法概念可以简化为核心类型理论，其中固定数量的构造函数利用了新颖的索引容器概念。结果，我们显示的索引容器为严格的积极家庭提供了正常的形式，与容器为严格的积极类型提供正常形式的方式相同。有趣的是，从容器到索引容器的这一步骤无需扩展核心类型理论。此处介绍的大多数构造都是使用AGDA系统正式化的。
We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.