Variations on Inductive-Recursive Definitions

Authors Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg, Stephan Spahn



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.63.pdf
  • Filesize: 468 kB
  • 13 pages

Document Identifiers

Author Details

Neil Ghani
Conor McBride
Fredrik Nordvall Forsberg
Stephan Spahn

Cite As Get BibTex

Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg, and Stephan Spahn. Variations on Inductive-Recursive Definitions. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 63:1-63:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.MFCS.2017.63

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
(U, T) = \mu [c] : Fam D is exhibited as the initial algebra of [c].

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

Subject Classification

Keywords
  • Type Theory
  • induction-recursion
  • initial-algebra semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. TCS, 342(1):3 - 27, 2005. Google Scholar
  2. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. Journal Functional Programming, 25, 2015. Google Scholar
  3. James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In ICFP 2010, pages 3-14, 2010. Google Scholar
  4. Peter Dybjer. Inductive families. Formal aspects of computing, 6(4):440-465, 1994. Google Scholar
  5. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), 2000. Google Scholar
  6. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In TLCA, pages 129-146. Springer Verlag, 1999. Google Scholar
  7. Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124(1-3):1-47, 2003. Google Scholar
  8. Peter Dybjer and Anton Setzer. Indexed induction-recursion. Journal of logic and algebraic programming, 66(1):1-49, 2006. Google Scholar
  9. Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Types for Proofs and Programs, pages 210-225, 2004. Google Scholar
  10. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154:153-192, 2013. Google Scholar
  11. Neil Ghani and Peter Hancock. Containers, monads and induction recursion. Mathematical Structures in Computer Science, 26(1):89-113, 2016. Google Scholar
  12. Peter Hancock. Private communication. Google Scholar
  13. Per Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. Google Scholar
  14. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Google Scholar
  15. Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13(3):386-402, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail