Positive inductive-recursive definitions

Research output: Contribution to journalArticle

Abstract

A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C 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(C) 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 and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.
LanguageEnglish
Article number13
JournalLogical Methods in Computer Science
Volume11
Issue number1
DOIs
Publication statusPublished - 27 Mar 2015

Fingerprint

Recursive functions
Algebra
Functor
Morphisms
Recursive Functions
Justify
Elimination
Restriction

Keywords

  • data types
  • type definition
  • code types

Cite this

@article{7e7aabb0fcb4486cbb5a7c3f970b0490,
title = "Positive inductive-recursive definitions",
abstract = "A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C 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(C) 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 and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.",
keywords = "data types, type definition, code types",
author = "Neil Ghani and {Nordvall Forsberg}, Fredrik and Lorenzo Malatesta",
year = "2015",
month = "3",
day = "27",
doi = "10.2168/LMCS-11(1:13)2015",
language = "English",
volume = "11",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "1",

}

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

In: Logical Methods in Computer Science, Vol. 11, No. 1, 13, 27.03.2015.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Positive inductive-recursive definitions

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Malatesta, Lorenzo

PY - 2015/3/27

Y1 - 2015/3/27

N2 - A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C 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(C) 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 and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.

AB - A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C 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(C) 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 and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.

KW - data types

KW - type definition

KW - code types

UR - http://www.lmcs-online.org/ojs/viewarticle.php?id=1556&layout=abstract

U2 - 10.2168/LMCS-11(1:13)2015

DO - 10.2168/LMCS-11(1:13)2015

M3 - Article

VL - 11

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

M1 - 13

ER -