{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:47Z","timestamp":1780994687077,"version":"3.54.1"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2016,2,9]],"date-time":"2016-02-09T00:00:00Z","timestamp":1454976000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2017,10]]},"abstract":"<jats:p>Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras and Elgot algebras. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when the coalgebra is well founded.<\/jats:p><jats:p>If the coalgebra is not well founded, then there can be multiple solutions. The standard semantics of recursive programs gives a particular solution, typically the least fixpoint of a certain monotone map on a domain whose least element is the totally undefined function; but this solution may not be the desired one. We have recently proposed programming language constructs to allow the specification of alternative solutions and methods to compute them. We have implemented these new constructs as an extension of OCaml.<\/jats:p><jats:p>In this paper, we prove some theoretical results characterizing well-founded coalgebras, along with several examples for which this extension is useful. We also give several examples that are not well founded but still have a desired solution. In each case, the function would diverge under the standard semantics of recursion, but can be specified and computed with the programming language constructs we have proposed.<\/jats:p>","DOI":"10.1017\/s0960129515000481","type":"journal-article","created":{"date-parts":[[2016,2,9]],"date-time":"2016-02-09T05:53:18Z","timestamp":1454997198000},"page":"1111-1131","source":"Crossref","is-referenced-by-count":3,"title":["Well-founded coalgebras, revisited"],"prefix":"10.1017","volume":"27","author":[{"given":"JEAN-BAPTISTE","family":"JEANNIN","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DEXTER","family":"KOZEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALEXANDRA","family":"SILVA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2016,2,9]]},"reference":[{"key":"S0960129515000481_ref5","unstructured":"CoCaml project. (December 2012). http:\/\/www.cs.cornell.edu\/Projects\/CoCaml\/."},{"key":"S0960129515000481_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80045-5"},{"key":"S0960129515000481_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.038"},{"key":"S0960129515000481_ref4","first-page":"84","volume-title":"Lecture Notes in Computer Science","author":"Capretta","year":"2009"},{"key":"S0960129515000481_ref2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:4)2006"},{"key":"S0960129515000481_ref3","unstructured":"Capretta V. (2007). An introduction to corecursive algebras. http:\/\/www.cs.ru.nl\/~venanzio\/publications\/brouwer_seminar_4_12_2007.pdf."},{"key":"S0960129515000481_ref7","volume-title":"A Logical Approach to Discrete Math","author":"Gries","year":"1994"},{"key":"S0960129515000481_ref20","volume-title":"Practical Foundations of Mathematics","author":"Taylor","year":"1999"},{"key":"S0960129515000481_ref12","doi-asserted-by":"crossref","unstructured":"Kozen D. (May 2011). Realization of coinductive types. In: Mislove M. and Ouaknine J. (eds.) Proceedings of the 27th Conf. Math. Found. Programming Semantics (MFPS XXVII), Pittsburgh, PA. Elsevier Electronic Notes in Theoretical Computer Science 148\u2013155.","DOI":"10.1016\/j.entcs.2011.09.024"},{"key":"S0960129515000481_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"key":"S0960129515000481_ref1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2007028"},{"key":"S0960129515000481_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129515000481_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(74)90032-2"},{"key":"S0960129515000481_ref17","volume-title":"Introduction to the Theory of Computation","author":"Sipser","year":"2006"},{"key":"S0960129515000481_ref11","first-page":"61","volume-title":"Lecture Notes in Computer Science","author":"Jeannin","year":"2013"},{"key":"S0960129515000481_ref16","volume-title":"Computational Complexity","author":"Papadimitriou","year":"1993"},{"key":"S0960129515000481_ref9","doi-asserted-by":"crossref","unstructured":"Hirschowitz T. , Leroy X. and Wells J.B. (2003). Compilation of extended recursion in call-by-value functional languages. In: PPDP 2003 160\u2013171.","DOI":"10.1145\/888251.888267"},{"key":"S0960129515000481_ref10","unstructured":"Jeannin J.-B. , Kozen D. and Silva A. (December 2012). CoCaml: Programming with coinductive types. Technical Report http:\/\/hdl.handle.net\/1813\/30798, Computing and Information Science, Cornell University."},{"key":"S0960129515000481_ref21","unstructured":"Tranc\u00f3n y Widemann B. (August 2011). Coalgebraic semantics of recursion on circular data structures. In: Cirstea C. , Seisenberger M. and Wilkinson T. (eds.) CALCO Young Researchers Workshop (CALCO-jnr 2011) 28\u201342."},{"key":"S0960129515000481_ref18","unstructured":"Sperber M. and Thiemann P. (September 1998). ML and the address operator. In: Proceedings of the ACM SIGPLAN Workshop on ML 152\u2013153."},{"key":"S0960129515000481_ref6","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"Dershowitz","year":"1990"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129515000481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T18:14:01Z","timestamp":1555438441000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129515000481\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,9]]},"references-count":21,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["S0960129515000481"],"URL":"https:\/\/doi.org\/10.1017\/s0960129515000481","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,9]]}}}