2026-07-23T12:01:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7694 2024-03-06T10:40:48Z ddc:004 open_access

Taylor Expansion, lambda-Reduction and Normalization Vaux, Lionel lambda-calculus non-determinism normalization denotational semantics We introduce 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 introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of lambda-terms. We show that the reduction of resource vectors contains the image, through Taylor expansion, of beta-reduction in the algebraic lambda-calculus, i.e. lambda-calculus extended with weighted sums: in particular, Taylor expansion and normalization commute. We moreover exhibit a class of algebraic lambda-terms, having a normalizable Taylor expansion, subsuming both arbitrary pure lambda-terms, and normalizable algebraic lambda-terms. For these, we prove the commutation of Taylor expansion and normalization in a more denotational sense, mimicking the Böhm tree construction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lionel Vaux 2017 Is Part Of LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2017.39 urn:nbn:de:0030-drops-76948 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.39 eng https://creativecommons.org/licenses/by/3.0/legalcode