{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article10081","name":"Variations on Inductive-Recursive Definitions","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\r\n(U, T) = \\mu [c] : Fam D is exhibited as the initial algebra of [c].\r\n\r\nThis 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.","keywords":["Type Theory","induction-recursion","initial-algebra semantics"],"author":[{"@type":"Person","name":"Ghani, Neil","givenName":"Neil","familyName":"Ghani"},{"@type":"Person","name":"McBride, Conor","givenName":"Conor","familyName":"McBride"},{"@type":"Person","name":"Nordvall Forsberg, Fredrik","givenName":"Fredrik","familyName":"Nordvall Forsberg"},{"@type":"Person","name":"Spahn, Stephan","givenName":"Stephan","familyName":"Spahn"}],"position":63,"pageStart":"63:1","pageEnd":"63:13","dateCreated":"2017-12-01","datePublished":"2017-12-01","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Ghani, Neil","givenName":"Neil","familyName":"Ghani"},{"@type":"Person","name":"McBride, Conor","givenName":"Conor","familyName":"McBride"},{"@type":"Person","name":"Nordvall Forsberg, Fredrik","givenName":"Fredrik","familyName":"Nordvall Forsberg"},{"@type":"Person","name":"Spahn, Stephan","givenName":"Stephan","familyName":"Spahn"}],"copyrightYear":"2017","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2017.63","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume6286","volumeNumber":83,"name":"42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)","dateCreated":"2017-12-01","datePublished":"2017-12-01","editor":[{"@type":"Person","name":"Larsen, Kim G.","givenName":"Kim G.","familyName":"Larsen"},{"@type":"Person","name":"Bodlaender, Hans L.","givenName":"Hans L.","familyName":"Bodlaender"},{"@type":"Person","name":"Raskin, Jean-Francois","givenName":"Jean-Francois","familyName":"Raskin"}],"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article10081","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6286"}}}