Rémy Cerda ; Lionel Vaux Auclair - Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications

lmcs:10308 - Logical Methods in Computer Science, December 20, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:34)2023
Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and ApplicationsArticle

Authors: Rémy Cerda ; Lionel Vaux Auclair

    Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of $\lambda$-terms has been broadly used as a tool to approximate the terms of several variants of the $\lambda$-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. This led us to consider extending this formalism to the infinitary $\lambda$-calculus, since the $\Lambda_{\infty}^{001}$ version of this calculus has Böhm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem. We give a (co-)inductive presentation of $\Lambda_{\infty}^{001}$. We define a Taylor expansion on this calculus, and state that the infinitary $\beta$-reduction can be simulated through this Taylor expansion. The target language is the usual resource calculus, and in particular the resource reduction remains finite, confluent and terminating. Finally, we state the generalised Commutation theorem and use our results to provide simple proofs of some normalisation and confluence properties in the infinitary $\lambda$-calculus.


    Volume: Volume 19, Issue 4
    Published on: December 20, 2023
    Accepted on: November 3, 2023
    Submitted on: November 15, 2022
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03B40 (Primary), 03F05 (Secondary),F.4.1

    Consultation statistics

    This page has been seen 524 times.
    This article's PDF has been downloaded 123 times.