Abstract
This paper introduces deep induction, and shows that it is the notion of induction most appropriate to nested types and other data types defined over, or mutually recursively with, (other) such types. Standard induction rules induct over only the top-level structure of data, leaving any data internal to the top-level structure untouched. By contrast, deep induction rules induct over all of the structured data present. We give a grammar generating a robust class of nested types (and thus ADTs), and develop a fundamental theory of deep induction for them using their recently defined semantics as fixed points of accessible functors on locally presentable categories. We then use our theory to derive deep induction rules for some common ADTs and nested types, and show how these rules specialize to give the standard structural induction rules for these types. We also show how deep induction specializes to solve the long-standing problem of deriving principled and practically useful structural induction rules for bushes and other truly nested types. Overall, deep induction opens the way to making induction principles appropriate to richly structured data types available in programming languages and proof assistants. Agda implementations of our development and examples, including two extended case studies, are available.
Chapter PDF
Similar content being viewed by others
References
Abbott, M.G., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theoretical Computer Science 342(2), pp. 3-27 (2005)
Altenkirch, T, Ghani, N., Hancock, P., McBride, C., Morris, P.: Indexed containers. Journal of Functional Programming 25 (2015)
Abbott, M. G., Altenkirch, T., Ghani, N.: Representing nested inductive types using W-types. In: Automata, Languages and Programming, pp. 59-71 (2004)
Abel, A.: Type-based termination: A polymorphic lambda-calculus with sized higher-order types. Ph.D. Dissertation, Ludwig Maximilians University Munich. https://dblp.org/rec/bib/phd/de/Abel2007. 2007.
Abel, A.: Semi-continuous sized types and termination. Logical Methods in Computer Science 4(2) (2008)
Abel, A.: MiniAgda: Integrating sized and dependent types. In: Partiality and Recursion in Interactive Theorem Provers, pp. 18-32 (2010)
Blanchette, J. C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly Modular (Co)datatypes for Isabelle/HOL. In: Interactive Theorem Proving, pp. 99-110 (2014)
Bird, R., Meertens, L.: Nested datatypes. In: Mathematics of Program Construction, pp. 52-67 (1998)
Bird, R., Paterson, R.: De Bruijn notation as a nested datatype. Journal of Functional Programming 9(1), pp. 77-91 (1999)
Fu, P., Selinger, P.: Dependently typed folds for nested data types. ArXiv, https://arxiv.org/abs/1806.05230. 2018.
Ghani, N., Johann, P., Fumex, C.: Fibrational induction rules for initial algebras. In: Computer Science Logic, pp. 336-350 (2010)
Ghani, N., Johann, P., Fumex, C.: Generic fibrational induction. Logical Methods in Computer Science 8(2) (2012)
Johann, P., Polonsky, A.: Higher-kinded data types: Syntax and semantics. In: Logic in Computer Science, pp. 1-13 (2019)
Johann, P. and Polonsky, A.: Accompanying Agda code for this paper. Available at https://cs.appstate.edu/~johannp/FoSSaCS19Code.html, 2019.
Matthes, R.: An induction principle for nested datatypes in intensional type theory. Journal of Functional Programming 3 & 4, pp. 439-468 (2009)
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1999)
Tassi, E.: Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. In: Interactive Theorem Proving, pp. 1-18 (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Johann, P., Polonsky, A. (2020). Deep Induction: Induction Rules for (Truly) Nested Types. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)