{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T17:51:01Z","timestamp":1760982661150,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,3,17]],"date-time":"2008-03-17T00:00:00Z","timestamp":1205712000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A fully-automated algorithm is developed able to show that evaluation of a\ngiven untyped lambda-expression will terminate under CBV (call-by-value). The\n``size-change principle'' from first-order programs is extended to arbitrary\nuntyped lambda-expressions in two steps. The first step suffices to show CBV\ntermination of a single, stand-alone lambda;-expression. The second suffices to\nshow CBV termination of any member of a regular set of lambda-expressions,\ndefined by a tree grammar. (A simple example is a minimum function, when\napplied to arbitrary Church numerals.) The algorithm is sound and proven so in\nthis paper. The Halting Problem's undecidability implies that any sound\nalgorithm is necessarily incomplete: some lambda-expressions may in fact\nterminate under CBV evaluation, but not be recognised as terminating.\n  The intensional power of the termination algorithm is reasonably high. It\ncertifies as terminating many interesting and useful general recursive\nalgorithms including programs with mutual recursion and parameter exchanges,\nand Colson's ``minimum'' algorithm. Further, our type-free approach allows use\nof the Y combinator, and so can identify as terminating a substantial subset of\nPCF.<\/jats:p>","DOI":"10.2168\/lmcs-4(1:3)2008","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:26:10Z","timestamp":1212499570000},"source":"Crossref","is-referenced-by-count":7,"title":["Call-by-value Termination in the Untyped lambda-calculus"],"prefix":"10.46298","volume":"Volume 4, Issue 1","author":[{"given":"Neil D.","family":"Jones","sequence":"first","affiliation":[]},{"given":"Nina","family":"Bohr","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,3,17]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/915\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/915\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:02Z","timestamp":1681243142000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/915"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3,17]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(1:3)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0801.0882","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0801.0882","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1145\/2837614.2837667","asserted-by":"subject"},{"id-type":"doi","id":"10.1145\/2914770.2837667","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,3,17]]},"article-number":"915"}}