License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/8118/
Go to the corresponding LIPIcs Volume Portal

Ghani, Neil ; McBride, Conor ; Nordvall Forsberg, Fredrik ; Spahn, Stephan

Variations on Inductive-Recursive Definitions

pdf-format:
LIPIcs-MFCS-2017-63.pdf (0.5 MB)

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},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/8118},
  URN =		{urn:nbn:de:0030-drops-81184},
  doi =		{10.4230/LIPIcs.MFCS.2017.63},
  annote =	{Keywords: Type Theory, induction-recursion, initial-algebra semantics}
}

Keywords: Type Theory, induction-recursion, initial-algebra semantics
Collection: 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)
Issue Date: 2017
Date of publication: 01.12.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI