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