Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.39
URN: urn:nbn:de:0030-drops-76948
URL: https://drops.dagstuhl.de/opus/volltexte/2017/7694/
Vaux, Lionel
Taylor Expansion, lambda-Reduction and Normalization
| pdf-format: |
|
Abstract
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.
BibTeX - Entry
@InProceedings{vaux:LIPIcs:2017:7694,
author = {Lionel Vaux},
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 = {Valentin Goranko and Mads Dam},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7694},
URN = {urn:nbn:de:0030-drops-76948},
doi = {10.4230/LIPIcs.CSL.2017.39},
annote = {Keywords: lambda-calculus, non-determinism, normalization, denotational semantics}
}
| Keywords: | lambda-calculus, non-determinism, normalization, denotational semantics | |
| Seminar: | 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) | |
| Issue date: | 2017 | |
| Date of publication: | 16.08.2017 |
