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.2013.101
URN: urn:nbn:de:0030-drops-41925
URL: https://drops.dagstuhl.de/opus/volltexte/2013/4192/
Boudes, Pierre ; He, Fanny ; Pagani, Michele
A characterization of the Taylor expansion of lambda-terms
| pdf-format: |
|
Abstract
The Taylor expansion of lambda-terms, as introduced by Ehrhard and Regnier, expresses a lambda-term as a series of multi-linear terms, called simple terms, which capture bounded computations. Normal forms of Taylor expansions give a notion of infinitary normal forms, refining the notion of Böhm trees in a quantitative setting.We give the algebraic conditions over a set of normal simple terms which characterize the property of being the normal form of the Taylor expansion of a lambda-term. From this full completeness result, we give further conditions which semantically describe normalizable and total lambda-terms.
BibTeX - Entry
@InProceedings{boudes_et_al:LIPIcs:2013:4192,
author = {Pierre Boudes and Fanny He and Michele Pagani},
title = {{A characterization of the Taylor expansion of lambda-terms}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {101--115},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4192},
URN = {urn:nbn:de:0030-drops-41925},
doi = {10.4230/LIPIcs.CSL.2013.101},
annote = {Keywords: Lambda-Calculus, B{\"o}hm trees, Differential Lambda-Calculus, Linear Logic}
}
| Keywords: | Lambda-Calculus, Böhm trees, Differential Lambda-Calculus, Linear Logic | |
| Seminar: | Computer Science Logic 2013 (CSL 2013) | |
| Issue date: | 2013 | |
| Date of publication: | 02.09.2013 |
