When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2017.63
URN: urn:nbn:de:0030-drops-81184
URL: http://drops.dagstuhl.de/opus/volltexte/2017/8118/
 Go to the corresponding LIPIcs Volume Portal

### Variations on Inductive-Recursive Definitions

 pdf-format:

### Abstract

Dybjer and Setzer introduced the definitional principle of inductive-recursively defined families - i.e. of families (U : Set, T : U -> D) such that the inductive definition of U may depend on the recursively defined T --- by defining a type DS D E of codes. Each c : DS D E defines a functor [c] : Fam D -> Fam E, and (U, T) = \mu [c] : Fam D is exhibited as the initial algebra of [c]. This paper considers the composition of DS-definable functors: Given F : Fam C -> Fam D and G : Fam D -> Fam E, is G \circ F : Fam C -> Fam E DS-definable, if F and G are? We show that this is the case if and only if powers of families are DS-definable, which seems unlikely. To construct composition, we present two new systems UF and PN of codes for inductive-recursive definitions, with UF a subsytem of DS a subsystem of PN. Both UF and PN are closed under composition. Since PN defines a potentially larger class of functors, we show that there is a model where initial algebras of PN-functors exist by adapting Dybjer-Setzer's proof for DS.

### BibTeX - Entry

@InProceedings{ghani_et_al:LIPIcs:2017:8118,
author =	{Neil Ghani and Conor McBride and Fredrik Nordvall Forsberg and Stephan Spahn},
title =	{{Variations on Inductive-Recursive Definitions}},
booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
pages =	{63:1--63:13},
series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =	{978-3-95977-046-0},
ISSN =	{1868-8969},
year =	{2017},
volume =	{83},
editor =	{Kim G. Larsen and Hans L. Bodlaender and Jean-Francois Raskin},
publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},