{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:02:14Z","timestamp":1765123334792,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452308"},{"type":"electronic","value":"9783030452315"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces<jats:italic>deep induction<\/jats:italic>, 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<jats:italic>all<\/jats:italic>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<jats:italic>truly<\/jats:italic>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.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_18","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"339-358","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Deep Induction: Induction Rules for\u00a0(Truly)\u00a0Nested\u00a0Types"],"prefix":"10.1007","author":[{"given":"Patricia","family":"Johann","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Polonsky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abbott, M.G., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theoretical Computer Science 342(2), pp. 3-27 (2005)","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T, Ghani, N., Hancock, P., McBride, C., Morris, P.: Indexed containers. Journal of Functional Programming 25 (2015)","DOI":"10.1017\/S095679681500009X"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Abbott, M. G., Altenkirch, T., Ghani, N.: Representing nested inductive types using W-types. In: Automata, Languages and Programming, pp. 59-71 (2004)","DOI":"10.1007\/978-3-540-27836-8_8"},{"key":"18_CR4","unstructured":"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."},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Abel, A.: Semi-continuous sized types and termination. Logical Methods in Computer Science 4(2) (2008)","DOI":"10.2168\/LMCS-4(2:3)2008"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Abel, A.: MiniAgda: Integrating sized and dependent types. In: Partiality and Recursion in Interactive Theorem Provers, pp. 18-32 (2010)","DOI":"10.4204\/EPTCS.43.2"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Blanchette, J. C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly Modular (Co)datatypes for Isabelle\/HOL. In: Interactive Theorem Proving, pp. 99-110 (2014)","DOI":"10.1007\/978-3-319-08970-6_7"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Bird, R., Meertens, L.: Nested datatypes. In: Mathematics of Program Construction, pp. 52-67 (1998)","DOI":"10.1007\/BFb0054285"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Bird, R., Paterson, R.: De Bruijn notation as a nested datatype. Journal of Functional Programming 9(1), pp. 77-91 (1999)","DOI":"10.1017\/S0956796899003366"},{"key":"18_CR10","unstructured":"Fu, P., Selinger, P.: Dependently typed folds for nested data types. ArXiv, https:\/\/arxiv.org\/abs\/1806.05230. 2018."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Ghani, N., Johann, P., Fumex, C.: Fibrational induction rules for initial algebras. In: Computer Science Logic, pp. 336-350 (2010)","DOI":"10.1007\/978-3-642-15205-4_27"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Ghani, N., Johann, P., Fumex, C.: Generic fibrational induction. Logical Methods in Computer Science 8(2) (2012)","DOI":"10.2168\/LMCS-8(2:12)2012"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Johann, P., Polonsky, A.: Higher-kinded data types: Syntax and semantics. In: Logic in Computer Science, pp. 1-13 (2019)","DOI":"10.1109\/LICS.2019.8785657"},{"key":"18_CR14","unstructured":"Johann, P. and Polonsky, A.: Accompanying Agda code for this paper. Available at https:\/\/cs.appstate.edu\/~johannp\/FoSSaCS19Code.html, 2019."},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Matthes, R.: An induction principle for nested datatypes in intensional type theory. Journal of Functional Programming 3 & 4, pp. 439-468 (2009)","DOI":"10.1017\/S095679680900731X"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1999)","DOI":"10.1017\/CBO9780511530104"},{"key":"18_CR17","unstructured":"Tassi, E.: Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. In: Interactive Theorem Proving, pp. 1-18 (2019)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T15:48:27Z","timestamp":1666367307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}