{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:38:03Z","timestamp":1753889883875,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T00:00:00Z","timestamp":1564531200000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T00:00:00Z","timestamp":1564531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T00:00:00Z","timestamp":1564531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-11-BS02-0010"],"award-info":[{"award-number":["ANR-11-BS02-0010"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-12-JS02-0006"],"award-info":[{"award-number":["ANR-12-JS02-0006"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $\\lambda$-terms that this operation commutes with normalization: the expansion of a $\\lambda$-term is always normalizable and its normal form is the expansion of the B\\&amp;quot;ohm tree of the term. We generalize this result to the non-uniform setting of the algebraic $\\lambda$-calculus, i.e. $\\lambda$-calculus extended with linear combinations of terms. This requires us to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's techniques rely heavily on the uniform, deterministic nature of the ordinary $\\lambda$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of B\\&amp;quot;ohm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $\\lambda$-term is not always normalizable. Our solution is to provide a fine grained study of the dynamics of $\\beta$-reduction under Taylor expansion, by introducing a notion of reduction on resource vectors, i.e. infinite linear combinations of resource $\\lambda$-terms. The latter form the multilinear fragment of the differential $\\lambda$-calculus, and resource vectors are the target of the Taylor expansion of $\\lambda$-terms. We show the reduction of resource vectors contains the image of any $\\beta$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose. We moreover identify a class of algebraic $\\lambda$-terms, encompassing both normalizable algebraic $\\lambda$-terms and arbitrary ordinary $\\lambda$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of B\\&amp;quot;ohm trees to this setting.<\/jats:p>","DOI":"10.23638\/lmcs-15(3:9)2019","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:36:27Z","timestamp":1743701787000},"source":"Crossref","is-referenced-by-count":0,"title":["Normalizing the Taylor expansion of non-deterministic {\\lambda}-terms, via parallel reduction of resource vectors"],"prefix":"10.23638","volume":"Volume 15, Issue 3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9466-418X","authenticated-orcid":false,"given":"Lionel","family":"Vaux","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2019,7,31]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/1706.04700v6","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/1706.04700v6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:36:28Z","timestamp":1743701788000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/4297"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,31]]},"references-count":0,"URL":"https:\/\/doi.org\/10.23638\/lmcs-15(3:9)2019","relation":{"has-preprint":[{"id-type":"arxiv","id":"1706.04700v5","asserted-by":"subject"},{"id-type":"arxiv","id":"1706.04700v4","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1706.04700","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1706.04700","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2019,7,31]]},"article-number":"4297"}}