Federico Olimpieri ; Lionel Vaux Auclair - On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants

lmcs:6701 - Logical Methods in Computer Science, January 6, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:1)2022
On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximantsArticle

Authors: Federico Olimpieri ; Lionel Vaux Auclair ORCID

    We show that the normal form of the Taylor expansion of a $\lambda$-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a nondeterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier's approach can be preserved in this setting.


    Volume: Volume 18, Issue 1
    Published on: January 6, 2022
    Accepted on: July 30, 2021
    Submitted on: August 7, 2020
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1366 times.
    This article's PDF has been downloaded 660 times.