{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T17:44:19Z","timestamp":1762623859307},"reference-count":19,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T00:00:00Z","timestamp":1491350400000},"content-version":"unspecified","delay-in-days":94,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin\u2013L\u00f6f type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.<\/jats:p>","DOI":"10.1017\/s0956796817000041","type":"journal-article","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T10:12:29Z","timestamp":1491387149000},"source":"Crossref","is-referenced-by-count":3,"title":["Finiteness and rational sequences, constructively"],"prefix":"10.1017","volume":"27","author":[{"given":"TARMO","family":"UUSTALU","sequence":"first","affiliation":[]},{"given":"NICCOL\u00d2","family":"VELTRI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,4,5]]},"reference":[{"key":"S0956796817000041_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"S0956796817000041_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003924"},{"key":"S0956796817000041_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90032-1"},{"key":"S0956796817000041_ref9","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/2808098.2808102","volume-title":"Proceedings of 11th ACM SIGPLAN Wksh. on Generic Programming, WGP '15","author":"Firsov","year":"2015"},{"key":"S0956796817000041_ref18","unstructured":"Spadotti R. (2016) Une th\u00e9orie m\u00e9canis\u00e9e des arbres r\u00e9guliers en th\u00e9orie des types d\u00e9pendants. PhD Thesis, Universit\u00e9 Toulouse 3 Paul Sabatier."},{"key":"S0956796817000041_ref5","first-page":"217","volume-title":"Scientific Contributions in Honor of Mirian Andr\u00e9s G\u00f3mez","author":"Coquand","year":"2010"},{"key":"S0956796817000041_ref3","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:4)2012"},{"key":"S0956796817000041_ref11","first-page":"173","volume-title":"Proceedings of 7th Symp. on Trends in Functional Programming, TFP 2006","author":"Ghani","year":"2006"},{"key":"S0956796817000041_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"S0956796817000041_ref10","volume-title":"Proceedings of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016","author":"Firsov","year":"2016"},{"key":"S0956796817000041_ref15","first-page":"230","volume-title":"Revised Lectures from 6th International School. on Advanced Functional Programming, AFP 2008","author":"Norell","year":"2009"},{"key":"S0956796817000041_ref2","first-page":"142","article-title":"Regular corecursion in Prolog","volume":"39","author":"Ancona","year":"2013","journal-title":"Comput. Lang. Syst. Struct."},{"key":"S0956796817000041_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90024-7"},{"key":"S0956796817000041_ref14","first-page":"61","volume-title":"Proceedings of 22nd European Symposium on Programming, ESOP 2013","author":"Jeannin","year":"2013"},{"key":"S0956796817000041_ref7","first-page":"175","volume-title":"Logic Colloquium '73","author":"Elgot","year":"1975"},{"key":"S0956796817000041_ref19","first-page":"137","volume-title":"Proceedings of 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP 2001","author":"Turbak","year":"2001"},{"key":"S0956796817000041_ref16","first-page":"187","volume-title":"Proceedings of 20th International Conference on Types for Proofs and Programs, TYPES 2014","author":"Parmann","year":"2014"},{"key":"S0956796817000041_ref17","first-page":"405","volume-title":"Proceedings of 6th International Conference on Interactive Theorem Proving, ITP 2015","author":"Spadotti","year":"2015"},{"key":"S0956796817000041_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(76)80003-7"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796817000041","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,27]],"date-time":"2022-07-27T06:22:09Z","timestamp":1658902929000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796817000041\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":19,"alternative-id":["S0956796817000041"],"URL":"https:\/\/doi.org\/10.1017\/s0956796817000041","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e13"}}