2026-07-22T15:45:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4192 2024-03-06T10:34:51Z ddc:004 open_access

A characterization of the Taylor expansion of lambda-terms Boudes, Pierre He, Fanny Pagani, Michele Lambda-Calculus Böhm trees Differential Lambda-Calculus Linear Logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pierre Boudes and Fanny He and Michele Pagani 2013 Is Part Of LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2013.101 urn:nbn:de:0030-drops-41925 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.101 eng https://creativecommons.org/licenses/by/3.0/legalcode