{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:38:22Z","timestamp":1753889902494,"version":"3.41.2"},"reference-count":21,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,19]],"date-time":"2012-06-19T00:00:00Z","timestamp":1340064000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper provides an induction rule that can be used to prove properties of\ndata structures whose types are inductive, i.e., are carriers of initial\nalgebras of functors. Our results are semantic in nature and are inspired by\nHermida and Jacobs' elegant algebraic formulation of induction for polynomial\ndata types. Our contribution is to derive, under slightly different\nassumptions, a sound induction rule that is generic over all inductive types,\npolynomial or not. Our induction rule is generic over the kinds of properties\nto be proved as well: like Hermida and Jacobs, we work in a general fibrational\nsetting and so can accommodate very general notions of properties on inductive\ntypes rather than just those of a particular syntactic form. We establish the\nsoundness of our generic induction rule by reducing induction to iteration. We\nthen show how our generic induction rule can be instantiated to give induction\nrules for the data types of rose trees, finite hereditary sets, and\nhyperfunctions. The first of these lies outside the scope of Hermida and\nJacobs' work because it is not polynomial, and as far as we are aware, no\ninduction rules have been known to exist for the second and third in a general\nfibrational framework. Our instantiation for hyperfunctions underscores the\nvalue of working in the general fibrational setting since this data type cannot\nbe interpreted as a set.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:12)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":6,"title":["Generic Fibrational Induction"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Neil","family":"Ghani","sequence":"first","affiliation":[]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[]},{"given":"Clement","family":"Fumex","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,19]]},"reference":[{"key":"10.2168\/LMCS-8(2:12)2012_am09","doi-asserted-by":"crossref","unstructured":"T. Altenkirch and P. Morris. Indexed Containers. Proceedings, Logic in Computer Science, pp. 277-285, 2009.","DOI":"10.1109\/LICS.2009.33"},{"key":"10.2168\/LMCS-8(2:12)2012_bdm97","doi-asserted-by":"crossref","unstructured":"R. S. Bird and O. De Moor. Algebra of Programming. Prentice Hall, 1997.","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"10.2168\/LMCS-8(2:12)2012_bm98","doi-asserted-by":"crossref","unstructured":"R. Bird and L. Meertens. Nested Datatypes. Proceedings, Mathematics of Program Construction, pp. 52-67, 1998.","DOI":"10.1007\/BFb0054285"},{"issue":"2-3","key":"10.2168\/LMCS-8(2:12)2012_ch88","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand and G. Huet.","year":"1988","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(2:12)2012_coq","unstructured":"The Coq Proof Assistant. Available at coq.inria.fr"},{"issue":"2","key":"10.2168\/LMCS-8(2:12)2012_dyb00","doi-asserted-by":"crossref","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"P. Dybjer.","year":"2000","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"10.2168\/LMCS-8(2:12)2012_gaa05","first-page":"3","volume":"341","author":"N. Ghani, M. Abbott, and T. Altenkirch.","year":"2005","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(2:12)2012_gj08","doi-asserted-by":"crossref","unstructured":"N. Ghani and P. Johann. Foundations for Structured Programming with GADTs.Proceedings, Principles of Programming Languages, pp. 297-308, 2008.","DOI":"10.1145\/1328897.1328475"},{"key":"10.2168\/LMCS-8(2:12)2012_gjf10","doi-asserted-by":"crossref","unstructured":"N. Ghani and P. Johann and C. Fumex. Fibrational Induction Rules for Initial Algebras.Proceedings, Computer Science Logic, pp. 336-350, 2010.","DOI":"10.1007\/978-3-642-15205-4_27"},{"issue":"2","key":"10.2168\/LMCS-8(2:12)2012_hj98","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1006\/inco.1998.2725","volume":"145","author":"C. Hermida and B. Jacobs.","year":"1998","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(2:12)2012_jac93","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/0304-3975(93)90169-T","volume":"107","author":"B. Jacobs.","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(2:12)2012_jac99","unstructured":"B. Jacobs.Categorical Logic and Type Theory. North Holland, 1999."},{"key":"10.2168\/LMCS-8(2:12)2012_jg07","doi-asserted-by":"crossref","unstructured":"P. Johann and N. Ghani. Initial Algebra Semantics is Enough!Proceedings, Typed Lambda Calculus and Applications, pp. 207-222, 2007.","DOI":"10.1007\/978-3-540-73228-0_16"},{"key":"10.2168\/LMCS-8(2:12)2012_law70","doi-asserted-by":"crossref","unstructured":"F. W. Lawvere. Equality in Hyperdoctrines and Comprehension Scheme as an Adjoint Functor.Applications of Categorical Algebra, pp. 1-14, 1970.","DOI":"10.1090\/pspum\/017\/0257175"},{"issue":"3-4","key":"10.2168\/LMCS-8(2:12)2012_mat09","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1017\/S095679680900731X","volume":"19","author":"R. Matthes.","year":"2009","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(2:12)2012_men91","unstructured":"N. P. Mendler. Predicative type universes and primitive recursion.Proceedings, Logic in Computer Science, pp. 173-184, 1991."},{"key":"10.2168\/LMCS-8(2:12)2012_mor07","unstructured":"P. Morris.Constructing Universes for Generic Programming. Dissertation, University of Nottingham, 2007."},{"issue":"1","key":"10.2168\/LMCS-8(2:12)2012_mog91","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi.","year":"1991","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(2:12)2012_nps90","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith.Programming in Martin-L\u00f6f's Type Theory. Oxford University Press, 1990."},{"key":"10.2168\/LMCS-8(2:12)2012_pav90","unstructured":"D. Pavlovic.Predicates and Fibrations. Dissertation, University of Utrecht, 1990."},{"key":"10.2168\/LMCS-8(2:12)2012_she04","doi-asserted-by":"crossref","unstructured":"T. Sheard. Languages of the Future.SIGPLAN Notices39 (10), pp. 116-119, 2004.","DOI":"10.1145\/1052883.1052897"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/717\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/717\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:30Z","timestamp":1681242870000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/717"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,19]]},"references-count":21,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:12)2012","relation":{"references":[{"id-type":"doi","id":"10.1017\/s095679680900731x","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1206.0357","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.0357","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,6,19]]},"article-number":"717"}}