Variations on inductive-recursive definitions

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

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 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 inductive-recursive 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 Dybjer-Setzer’s proof for DS .
Original language English Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science Germany 13 https://doi.org/10.4230/LIPIcs.MFCS.2017.63 Published - 30 Nov 2017 42nd International Symposium on Mathematical Foundations of Computer Science - Aalborg, DenmarkDuration: 21 Aug 2017 → 25 Aug 2017http://mfcs2017.cs.aau.dk/

Publication series

Name Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz Center for Informatics

Conference

Conference 42nd International Symposium on Mathematical Foundations of Computer Science MFCS 2017 Denmark Aalborg 21/08/17 → 25/08/17 http://mfcs2017.cs.aau.dk/

Keywords

• type theory
• induction recursion
• initial algebra semantics