{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:19Z","timestamp":1753894399281,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion\nof $\\lambda$-terms has been broadly used as a tool to approximate the terms of\nseveral variants of the $\\lambda$-calculus. Many results arise from a\nCommutation theorem relating the normal form of the Taylor expansion of a term\nto its B\\\"ohm tree. This led us to consider extending this formalism to the\ninfinitary $\\lambda$-calculus, since the $\\Lambda_{\\infty}^{001}$ version of\nthis calculus has B\\\"ohm trees as normal forms and seems to be the ideal\nframework to reformulate the Commutation theorem.\n  We give a (co-)inductive presentation of $\\Lambda_{\\infty}^{001}$. We define\na Taylor expansion on this calculus, and state that the infinitary\n$\\beta$-reduction can be simulated through this Taylor expansion. The target\nlanguage is the usual resource calculus, and in particular the resource\nreduction remains finite, confluent and terminating. Finally, we state the\ngeneralised Commutation theorem and use our results to provide simple proofs of\nsome normalisation and confluence properties in the infinitary\n$\\lambda$-calculus.<\/jats:p>","DOI":"10.46298\/lmcs-19(4:34)2023","type":"journal-article","created":{"date-parts":[[2023,12,20]],"date-time":"2023-12-20T21:30:07Z","timestamp":1703107807000},"source":"Crossref","is-referenced-by-count":0,"title":["Finitary Simulation of Infinitary $\\beta$-Reduction via Taylor Expansion, and Applications"],"prefix":"10.46298","volume":"Volume 19, Issue 4","author":[{"given":"R\u00e9my","family":"Cerda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lionel Vaux","family":"Auclair","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2023,12,20]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/12725\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/12725\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,20]],"date-time":"2023-12-20T21:30:07Z","timestamp":1703107807000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10308"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,20]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(4:34)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2211.05608v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2211.05608v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2211.05608","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2211.05608","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2023,12,20]]},"article-number":"10308"}}