Neil Ghani ; Fredrik Nordvall Forsberg ; Lorenzo Malatesta - Positive Inductive-Recursive Definitions

lmcs:1154 - Logical Methods in Computer Science, March 27, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:13)2015
Positive Inductive-Recursive Definitions

Authors: Neil Ghani ; Fredrik Nordvall Forsberg ORCID-iD; Lorenzo Malatesta

    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.


    Volume: Volume 11, Issue 1
    Published on: March 27, 2015
    Accepted on: June 25, 2015
    Submitted on: February 14, 2014
    Keywords: Computer Science - Logic in Computer Science

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2103.00223
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.csl.2022.28
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2103.00223
    • 10.48550/arxiv.2103.00223
    • 10.4230/lipics.csl.2022.28
    • 2103.00223
    Generalized Universe Hierarchies and First-Class Universe Levels
    Kov��cs, Andr��s ;

    2 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 592 times.
    This article's PDF has been downloaded 510 times.