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.
@InProceedings{vaux:LIPIcs.CSL.2017.39, author = {Vaux, Lionel}, title = {{Taylor Expansion, lambda-Reduction and Normalization}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {39:1--39:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.39}, URN = {urn:nbn:de:0030-drops-76948}, doi = {10.4230/LIPIcs.CSL.2017.39}, annote = {Keywords: lambda-calculus, non-determinism, normalization, denotational semantics} }
Feedback for Dagstuhl Publishing