Small induction recursion

Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)

Abstract

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.
LanguageEnglish
Title of host publicationTyped Lambda Calculus and Applications
Subtitle of host publication11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings
EditorsMasahito Hasegawa
Place of PublicationBerlin
PublisherSpringer
Pages156-172
Number of pages17
ISBN (Print)9783642389450
DOIs
Publication statusPublished - 6 Jun 2013
Event11th International Conference, TLCA 2013 - Eindhoven, Netherlands
Duration: 26 Jun 201328 Jun 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume7941
ISSN (Print)0302-9743

Conference

Conference11th International Conference, TLCA 2013
CountryNetherlands
CityEindhoven
Period26/06/1328/06/13

Fingerprint

Containers
Polynomials

Keywords

  • data type
  • inductive-recursive definitions
  • morphisms
  • recursions
  • salient features
  • second level

Cite this

Hancock, P., McBride, C., Ghani, N., Malatesta, L., & Altenkirch, T. (2013). Small induction recursion. In M. Hasegawa (Ed.), Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings (pp. 156-172). (Lecture Notes in Computer Science; Vol. 7941). Berlin: Springer. https://doi.org/10.1007/978-3-642-38946-7_13
Hancock, Peter ; McBride, Conor ; Ghani, Neil ; Malatesta, Lorenzo ; Altenkirch, Thorsten. / Small induction recursion. Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. editor / Masahito Hasegawa. Berlin : Springer, 2013. pp. 156-172 (Lecture Notes in Computer Science).
@inproceedings{9e949bfa683e47f1983da6bb0edfa83d,
title = "Small induction recursion",
abstract = "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.",
keywords = "data type, inductive-recursive definitions, morphisms, recursions, salient features, second level",
author = "Peter Hancock and Conor McBride and Neil Ghani and Lorenzo Malatesta and Thorsten Altenkirch",
year = "2013",
month = "6",
day = "6",
doi = "10.1007/978-3-642-38946-7_13",
language = "English",
isbn = "9783642389450",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "156--172",
editor = "Masahito Hasegawa",
booktitle = "Typed Lambda Calculus and Applications",

}

Hancock, P, McBride, C, Ghani, N, Malatesta, L & Altenkirch, T 2013, Small induction recursion. in M Hasegawa (ed.), Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7941, Springer, Berlin, pp. 156-172, 11th International Conference, TLCA 2013, Eindhoven, Netherlands, 26/06/13. https://doi.org/10.1007/978-3-642-38946-7_13

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 proceedingConference 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 -

Hancock P, McBride C, Ghani N, Malatesta L, Altenkirch T. Small induction recursion. In Hasegawa M, editor, Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. Berlin: Springer. 2013. p. 156-172. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-38946-7_13