• Media type: E-Article; Electronic Conference Proceeding; Text
  • Title: Taylor Expansion, lambda-Reduction and Normalization
  • Contributor: Vaux, Lionel [Author]
  • imprint: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.CSL.2017.39
  • Keywords: non-determinism ; normalization ; lambda-calculus ; denotational semantics
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: 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.
  • Access State: Open Access