Abstract
Dybjer and Setzer introduced the definitional principle of inductiverecursively 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 J c K : Fam D → Fam E , and ( U , T ) = μ J c K : Fam D is exhibited as the initial algebra of J c K . This paper considers the composition of DS definable functors: Given F : Fam C → Fam D and G : Fam D → Fam E , is G ◦ 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 inductiverecursive definitions, with UF ↪ → DS ↪ → 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 DybjerSetzer’s proof for DS .
Original language  English 

Title of host publication  Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science 
Place of Publication  Germany 
Number of pages  13 
DOIs  
Publication status  Published  30 Nov 2017 
Event  42nd International Symposium on Mathematical Foundations of Computer Science  Aalborg, Denmark Duration: 21 Aug 2017 → 25 Aug 2017 http://mfcs2017.cs.aau.dk/ 
Publication series
Name  Leibniz International Proceedings in Informatics 

Publisher  Schloss Dagstuhl – Leibniz Center for Informatics 
Conference
Conference  42nd International Symposium on Mathematical Foundations of Computer Science 

Abbreviated title  MFCS 2017 
Country  Denmark 
City  Aalborg 
Period  21/08/17 → 25/08/17 
Internet address 
Keywords
 type theory
 induction recursion
 initial algebra semantics
Fingerprint Dive into the research topics of 'Variations on inductiverecursive definitions'. Together they form a unique fingerprint.
Profiles

Fredrik Nordvall Forsberg
 Computer And Information Sciences  Lecturer B
 SICSA
Person: Academic, Research Only