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 .
LanguageEnglish
Title of host publicationProceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science
Place of PublicationGermany
Number of pages13
DOIs
Publication statusPublished - 30 Nov 2017
Event42nd International Symposium on Mathematical Foundations of Computer Science - Aalborg, Denmark
Duration: 21 Aug 201725 Aug 2017
http://mfcs2017.cs.aau.dk/

Publication series

NameLeibniz International Proceedings in Informatics
Publisher Schloss Dagstuhl – Leibniz Center for Informatics

Conference

Conference42nd International Symposium on Mathematical Foundations of Computer Science
Abbreviated titleMFCS 2017
CountryDenmark
CityAalborg
Period21/08/1725/08/17
Internet address

Fingerprint

Algebra
Chemical analysis

Keywords

  • type theory
  • induction recursion
  • initial algebra semantics

Cite this

Ghani, N., McBride, C., Nordvall Forsberg, F., & Spahn, S. (2017). Variations on inductive-recursive definitions. In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science [63] (Leibniz International Proceedings in Informatics ). Germany. https://doi.org/10.4230/LIPIcs.MFCS.2017.63
Ghani, Neil ; McBride, Conor ; Nordvall Forsberg, Fredrik ; Spahn, Stephan. / Variations on inductive-recursive definitions. Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science. Germany, 2017. (Leibniz International Proceedings in Informatics ).
@inproceedings{2dbf102fda6a4fb3ae1fbe5017d8f040,
title = "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 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 .",
keywords = "type theory, induction recursion, initial algebra semantics",
author = "Neil Ghani and Conor McBride and {Nordvall Forsberg}, Fredrik and Stephan Spahn",
year = "2017",
month = "11",
day = "30",
doi = "10.4230/LIPIcs.MFCS.2017.63",
language = "English",
series = "Leibniz International Proceedings in Informatics",
publisher = "Schloss Dagstuhl – Leibniz Center for Informatics",
booktitle = "Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science",

}

Ghani, N, McBride, C, Nordvall Forsberg, F & Spahn, S 2017, Variations on inductive-recursive definitions. in Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science., 63, Leibniz International Proceedings in Informatics , Germany, 42nd International Symposium on Mathematical Foundations of Computer Science, Aalborg, Denmark, 21/08/17. https://doi.org/10.4230/LIPIcs.MFCS.2017.63

Variations on inductive-recursive definitions. / Ghani, Neil; McBride, Conor; Nordvall Forsberg, Fredrik; Spahn, Stephan.

Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science. Germany, 2017. 63 (Leibniz International Proceedings in Informatics ).

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

TY - GEN

T1 - Variations on inductive-recursive definitions

AU - Ghani, Neil

AU - McBride, Conor

AU - Nordvall Forsberg, Fredrik

AU - Spahn, Stephan

PY - 2017/11/30

Y1 - 2017/11/30

N2 - 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 .

AB - 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 .

KW - type theory

KW - induction recursion

KW - initial algebra semantics

UR - http://mfcs2017.cs.aau.dk/

UR - http://www.dagstuhl.de/en/publications/lipics

U2 - 10.4230/LIPIcs.MFCS.2017.63

DO - 10.4230/LIPIcs.MFCS.2017.63

M3 - Conference contribution book

T3 - Leibniz International Proceedings in Informatics

BT - Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science

CY - Germany

ER -

Ghani N, McBride C, Nordvall Forsberg F, Spahn S. Variations on inductive-recursive definitions. In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science. Germany. 2017. 63. (Leibniz International Proceedings in Informatics ). https://doi.org/10.4230/LIPIcs.MFCS.2017.63