Positive inductive-recursive definitions

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

Abstract

We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.
LanguageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science
Subtitle of host publication5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings
EditorsReiko Heckel, Stefan Milius
Place of PublicationBerlin
Pages19-33
Number of pages15
DOIs
Publication statusPublished - 8 Aug 2013
Event5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 - Warsaw, Poland
Duration: 3 Sep 20136 Sep 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume8089
ISSN (Print)0302-9743

Conference

Conference5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013
CountryPoland
CityWarsaw
Period3/09/136/09/13

Fingerprint

Algebra

Keywords

  • data type
  • generalisation
  • inductive-recursive definitions
  • initial algebras
  • natural transformations
  • nested data
  • new theory
  • set-theoretic models

Cite this

Ghani, N., Malatesta, L., & Nordvall Forsberg, F. (2013). Positive inductive-recursive definitions. In R. Heckel, & S. Milius (Eds.), Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings (pp. 19-33). (Lecture Notes in Computer Science; Vol. 8089). Berlin. https://doi.org/10.1007/978-3-642-40206-7_3
Ghani, Neil ; Malatesta, Lorenzo ; Nordvall Forsberg, Fredrik. / Positive inductive-recursive definitions. Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings. editor / Reiko Heckel ; Stefan Milius. Berlin, 2013. pp. 19-33 (Lecture Notes in Computer Science).
@inproceedings{1a218f78367645f483d79e7f3774e44a,
title = "Positive inductive-recursive definitions",
abstract = "We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.",
keywords = "data type, generalisation, inductive-recursive definitions, initial algebras, natural transformations, nested data, new theory, set-theoretic models",
author = "Neil Ghani and Lorenzo Malatesta and {Nordvall Forsberg}, Fredrik",
year = "2013",
month = "8",
day = "8",
doi = "10.1007/978-3-642-40206-7_3",
language = "English",
isbn = "9783642402050",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "19--33",
editor = "Reiko Heckel and Stefan Milius",
booktitle = "Algebra and Coalgebra in Computer Science",

}

Ghani, N, Malatesta, L & Nordvall Forsberg, F 2013, Positive inductive-recursive definitions. in R Heckel & S Milius (eds), Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8089, Berlin, pp. 19-33, 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, Warsaw, Poland, 3/09/13. https://doi.org/10.1007/978-3-642-40206-7_3

Positive inductive-recursive definitions. / Ghani, Neil; Malatesta, Lorenzo; Nordvall Forsberg, Fredrik.

Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings. ed. / Reiko Heckel; Stefan Milius. Berlin, 2013. p. 19-33 (Lecture Notes in Computer Science; Vol. 8089).

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

TY - GEN

T1 - Positive inductive-recursive definitions

AU - Ghani, Neil

AU - Malatesta, Lorenzo

AU - Nordvall Forsberg, Fredrik

PY - 2013/8/8

Y1 - 2013/8/8

N2 - We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.

AB - We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.

KW - data type

KW - generalisation

KW - inductive-recursive definitions

KW - initial algebras

KW - natural transformations

KW - nested data

KW - new theory

KW - set-theoretic models

UR - http://link.springer.com/

UR - https://coalg.org/

U2 - 10.1007/978-3-642-40206-7_3

DO - 10.1007/978-3-642-40206-7_3

M3 - Conference contribution book

SN - 9783642402050

T3 - Lecture Notes in Computer Science

SP - 19

EP - 33

BT - Algebra and Coalgebra in Computer Science

A2 - Heckel, Reiko

A2 - Milius, Stefan

CY - Berlin

ER -

Ghani N, Malatesta L, Nordvall Forsberg F. Positive inductive-recursive definitions. In Heckel R, Milius S, editors, Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings. Berlin. 2013. p. 19-33. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-40206-7_3