Abstract
This work investigates the relationship between the theory of small inductive recursive definitions and the theory of dependent polynomials and indexed containers. Our central result is that the expressiveness of small inductive recursive definitions is exactly the same as that of dependent polynomials and indexed containers. A second contribution of this paper is the definition of morphisms of small inductive recursive definitions. This allows us to extend our main result to an equivalence between the category of small inductive recursive definitions and the category of dependent polynomials/indexed containers. We comment on both the theoretical and practical ramifications of this result.
| Original language | English |
|---|---|
| Title of host publication | Typed Lambda Calculus and Applications |
| Subtitle of host publication | 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings |
| Editors | Masahito Hasegawa |
| Place of Publication | Berlin |
| Publisher | Springer |
| Pages | 156-172 |
| Number of pages | 17 |
| ISBN (Print) | 9783642389450 |
| DOIs | |
| Publication status | Published - 6 Jun 2013 |
| Event | 11th International Conference, TLCA 2013 - Eindhoven, Netherlands Duration: 26 Jun 2013 → 28 Jun 2013 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 7941 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 11th International Conference, TLCA 2013 |
|---|---|
| Country | Netherlands |
| City | Eindhoven |
| Period | 26/06/13 → 28/06/13 |
Fingerprint
Keywords
- data type
- inductive-recursive definitions
- morphisms
- recursions
- salient features
- second level
Cite this
}
Small induction recursion. / Hancock, Peter; McBride, Conor; Ghani, Neil; Malatesta, Lorenzo; Altenkirch, Thorsten.
Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. ed. / Masahito Hasegawa. Berlin : Springer, 2013. p. 156-172 (Lecture Notes in Computer Science; Vol. 7941).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book
TY - GEN
T1 - Small induction recursion
AU - Hancock, Peter
AU - McBride, Conor
AU - Ghani, Neil
AU - Malatesta, Lorenzo
AU - Altenkirch, Thorsten
PY - 2013/6/6
Y1 - 2013/6/6
N2 - 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.This work investigates the relationship between the theory of small inductive recursive definitions and the theory of dependent polynomials and indexed containers. Our central result is that the expressiveness of small inductive recursive definitions is exactly the same as that of dependent polynomials and indexed containers. A second contribution of this paper is the definition of morphisms of small inductive recursive definitions. This allows us to extend our main result to an equivalence between the category of small inductive recursive definitions and the category of dependent polynomials/indexed containers. We comment on both the theoretical and practical ramifications of this result.
AB - 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.This work investigates the relationship between the theory of small inductive recursive definitions and the theory of dependent polynomials and indexed containers. Our central result is that the expressiveness of small inductive recursive definitions is exactly the same as that of dependent polynomials and indexed containers. A second contribution of this paper is the definition of morphisms of small inductive recursive definitions. This allows us to extend our main result to an equivalence between the category of small inductive recursive definitions and the category of dependent polynomials/indexed containers. We comment on both the theoretical and practical ramifications of this result.
KW - data type
KW - inductive-recursive definitions
KW - morphisms
KW - recursions
KW - salient features
KW - second level
UR - http://link.springer.com/
U2 - 10.1007/978-3-642-38946-7_13
DO - 10.1007/978-3-642-38946-7_13
M3 - Conference contribution book
SN - 9783642389450
T3 - Lecture Notes in Computer Science
SP - 156
EP - 172
BT - Typed Lambda Calculus and Applications
A2 - Hasegawa, Masahito
PB - Springer
CY - Berlin
ER -