Small Induction Recursion
Small Induction Recursion
复制标题
小归纳递归
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Thorsten Altenkirch
中科院分区：
文献类型：
--
作者：
P. Hancock;Conor McBride;Neil Ghani;Lorenzo Malatesta;Thorsten Altenkirch
数据类型理论有几种不同的方法。在最简单的层面上，多项式和容器给出了数据类型作为独立实体的理论。在第二个复杂性级别上，依赖多项式和索引容器处理更复杂的数据类型，其中数据具有可用于存储重要计算信息的关联索引。依赖多项式和索引容器的关键和显著特征是索引类型在数据之前定义。在最复杂的层次上，归纳递归允许我们同时定义数据和索引。
There are several different approaches to the theory of data types. At the simplest level, polynomials and containers give a theory of data types as free standing entities. At a second level of complexity, dependent polynomials and indexed containers handle more sophisticated data types in which the data have an associated indices which can be used to store important computational information. The crucial and salient feature of dependent polynomials and indexed containers is that the index types are defined in advance of the data. At the most sophisticated level, induction-recursion allows us to define data and indices simultaneously.
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter