Document Open Access Logo

A Syntax for Mutual Inductive Families

Authors Ambrus Kaposi , Jakob von Raumer

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.23.pdf
  • Filesize: 0.53 MB
  • 21 pages

Document Identifiers

Author Details

Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
Jakob von Raumer
  • University of Nottingham, UK

Funding

  • Kaposi, Ambrus: I acknowledge the support of the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme funding scheme, Project no. ED_18-1-2019-0030 (Application-specific highly reliable IT solutions), and of the European Union, co-financed by the European Social Fund (EFOP-3.6.2-16-2017-00013, Thematic Fundamental Research Collaborations Grounding Innovation in Informatics and Infocommunication).
  • von Raumer, Jakob: I acknowledge the support of COST Action EUTypes CA15123.

Cite AsGet BibTex

Ambrus Kaposi and Jakob von Raumer. A Syntax for Mutual Inductive Families. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.23

Abstract

Inductive families of types are a feature of most languages based on dependent types. They are usually described either by syntactic schemes or by encodings of strictly positive functors such as combinator languages or containers. The former approaches are informal and give only external signatures, the latter approaches suffer from encoding overheads and do not directly represent mutual types. In this paper we propose a direct method for describing signatures for mutual inductive families using a domain-specific type theory. A signature is a context (roughly speaking, a list of types) in this small type theory. Algebras, displayed algebras and sections are defined by models of this type theory: the standard model, the logical predicate and a logical relation interpretation, respectively. We reduce the existence of initial algebras for these signatures to the existence of the syntax of our domain-specific type theory. As this theory is very simple, its normal syntax can be encoded using indexed W-types. To the best of our knowledge, this is the first formalisation of the folklore fact that mutual inductive types can be reduced to indexed W-types. The contents of this paper were formalised in the proof assistant Agda.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • inductive types
  • mutual inductive types
  • W-types
  • Agda

Metrics

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

Supplementary Materials

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers - constructing strictly positive types. Theoretical Computer Science, 342:3-27, September 2005. Applied Semantics: Selected Topics. Google Scholar
  2. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type and scope safe universe of syntaxes with binding: Their semantics and proofs. Proc. ACM Program. Lang., 2(ICFP):90:1-90:30, July 2018. URL: https://doi.org/10.1145/3236785.
  3. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, pages 293-310, Cham, 2018. Springer International Publishing. Google Scholar
  4. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. Journal of Functional Programming, 25, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  5. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In ACM SIGPLAN Notices, volume 51(1), pages 18-29. ACM, 2016. Google Scholar
  6. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, PLPV '07, pages 57-68, New York, NY, USA, 2007. ACM. URL: https://doi.org/10.1145/1292597.1292608.
  7. Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic, 13th International Workshop, CSL '99, pages 453-468, 1999. Google Scholar
  8. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards certified meta-programming with typed Template-Coq. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 20-39. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_2.
  9. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6.1, 1997. Google Scholar
  10. Henning Basold and Herman Geuvers. Type Theory based on Dependent Inductive and Coinductive Types. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of LICS '16, pages 327-336. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934514.
  11. Henning Basold, Herman Geuvers, and Niels van der Weide. Higher inductive types in programming. Journal of Universal Computer Science, 23:63-88, 2017. Google Scholar
  12. Marcin Benke, Peter Dybjer, and Patrik Jansson. Universes for generic programs and proofs in dependent type theory. Nord. J. Comput., 10(4):265-289, 2003. Google Scholar
  13. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free - parametricity for dependent types. Journal of Functional Programming, 22(02):107-152, 2012. URL: https://doi.org/10.1017/S0956796812000056.
  14. Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290314.
  15. James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 3-14, New York, NY, USA, 2010. ACM. URL: https://doi.org/10.1145/1863543.1863547.
  16. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  17. Peter Dybjer. Inductive families. Formal aspects of computing, 6(4):440-465, 1994. Google Scholar
  18. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65:525-549, 2000. Google Scholar
  19. Peter Dybjer and Hugo Moeneclaey. Finitary higher inductive types in the groupoid model. Electronic Notes in Theoretical Computer Science, 336:119-134, 2018. The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). URL: https://doi.org/10.1016/j.entcs.2018.03.019.
  20. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer, 1999. Google Scholar
  21. Peter Dybjer and Anton Setzer. Indexed induction-recursion. J. Log. Algebr. Program., 66(1):1-49, 2006. URL: https://doi.org/10.1016/j.jlap.2005.07.001.
  22. Marcelo Fiore, Andrew M. Pitts, and S. C. Steenkamp. Constructing Infinitary Quotient-Inductive Types. arXiv e-prints, page arXiv:1911.06899, November 2019. URL: http://arxiv.org/abs/1911.06899.
  23. Martin Hofmann. Conservativity of equality reflection over intensional type theory. In TYPES 95, pages 153-164, 1995. Google Scholar
  24. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  25. Ambrus Kaposi and András Kovács. A syntax for higher inductive-inductive types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:18, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.20.
  26. Ambrus Kaposi and András Kovács. Signatures and induction principles for higher inductive-inductive types. arXiv preprint https://arxiv.org/abs/1902.00297, 2019. URL: https://arxiv.org/abs/1902.00297.
  27. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proceedings of the ACM on Programming Languages, 3(POPL):2, 2019. Google Scholar
  28. Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, pages 1-50, 2019. URL: https://doi.org/10.1017/S030500411900015X.
  29. Fredrik Nordvall Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University, 2013. Google Scholar
  30. Ulf Norell. Dependently typed programming in Agda. In Advanced Functional Programming, pages 230-266. Springer, 2009. Google Scholar
  31. Nicolas Oury. Extensionality in the calculus of constructions, pages 278-293. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005. URL: https://doi.org/10.1007/11541868_18.
  32. Christine Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications (TLCA), number 664 in Lecture Notes in Computer Science, 1993. Google Scholar
  33. Kent Petersson and Dan Synek. A set constructor for inductive sets in martin-löf’s type theory. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings, volume 389 of Lecture Notes in Computer Science, pages 128-140. Springer, 1989. URL: https://doi.org/10.1007/BFb0018349.
  34. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
  35. Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. Eliminating reflection from type theory. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 91-103. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294095.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact