Variations on inductive-recursive definitions
Ghani, Neil and McBride, Conor and Nordvall Forsberg, Fredrik and Spahn, Stephan; (2017) Variations on inductive-recursive definitions. In: Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science. Leibniz International Proceedings in Informatics . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, DNK. (https://doi.org/10.4230/LIPIcs.MFCS.2017.63)
Preview |
Text.
Filename: Ghani_etal_MPCS_2017_Variations_on_inductive_recursive.pdf
Accepted Author Manuscript License: Download (494kB)| Preview |
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 .
ORCID iDs
Ghani, Neil ORCID: https://orcid.org/0000-0002-3988-2560, McBride, Conor ORCID: https://orcid.org/0000-0003-1487-0886, Nordvall Forsberg, Fredrik ORCID: https://orcid.org/0000-0001-6157-9288 and Spahn, Stephan;-
-
Item type: Book Section ID code: 62321 Dates: DateEvent30 November 2017Published17 June 2017AcceptedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 09 Nov 2017 17:01 Last modified: 19 Nov 2024 01:22 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/62321