Lionel Vaux - Normalizing the Taylor expansion of non-deterministic {\lambda}-terms, via parallel reduction of resource vectors

lmcs:4297 - Logical Methods in Computer Science, July 31, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:9)2019
Normalizing the Taylor expansion of non-deterministic {\lambda}-terms, via parallel reduction of resource vectorsArticle

Authors: Lionel Vaux ORCID

    It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $\lambda$-terms that this operation commutes with normalization: the expansion of a $\lambda$-term is always normalizable and its normal form is the expansion of the Böhm tree of the term. We generalize this result to the non-uniform setting of the algebraic $\lambda$-calculus, i.e. $\lambda$-calculus extended with linear combinations of terms. This requires us to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's techniques rely heavily on the uniform, deterministic nature of the ordinary $\lambda$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of Böhm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $\lambda$-term is not always normalizable. Our solution is to provide a fine grained study of the dynamics of $\beta$-reduction under Taylor expansion, by introducing 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, and resource vectors are the target of the Taylor expansion of $\lambda$-terms. We show the reduction of resource vectors contains the image of any $\beta$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose. We moreover identify a class of algebraic $\lambda$-terms, encompassing both normalizable algebraic $\lambda$-terms and arbitrary ordinary $\lambda$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of Böhm trees to this setting.


    Volume: Volume 15, Issue 3
    Published on: July 31, 2019
    Accepted on: May 28, 2019
    Submitted on: February 20, 2018
    Keywords: Computer Science - Logic in Computer Science,F.3.2
    Funding:
      Source : OpenAIRE Graph
    • Realizability for classical logic, concurrency, references and rewriting; Funder: French National Research Agency (ANR); Code: ANR-11-BS02-0010
    • Computing with Quantitative Semantics; Funder: French National Research Agency (ANR); Code: ANR-12-JS02-0006

    Consultation statistics

    This page has been seen 1685 times.
    This article's PDF has been downloaded 329 times.