2026-07-21T20:32:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18006 2024-03-06T11:00:50Z ddc:004 open_access

α-Avoidance Frontull, Samuel Moser, Georg van Oostrom, Vincent λ-calculus variable capture α-conversion developments safe λ-calculus undecidability When substitutions and bindings interact, there is a risk of undesired side effects if the substitution is applied naïvely. The λ-calculus captures this phenomenon concretely, as β-reduction may require the renaming of bound variables to avoid variable capture. In this paper we introduce α-paths as an estimation for α-avoidance, roughly expressing that α-conversions are not required to prevent variable capture. These paths provide a novel method to analyse and predict the potential need for α in different calculi. In particular, we show how α-path characterises α-avoidance for several sub-calculi of the λ-calculus like (i) developments, (ii) affine/linear λ-calculi, (iii) the weak λ-calculus, (iv) μ-unfolding and (iv) finally the safe λ-calculus. Furthermore, we study the unavoidability of α-conversions in untyped and simply-typed λ-calculi and prove undecidability of the need of α-conversions for (leftmost-outermost reductions) in the untyped λ-calculus. To ease the work with α-paths, we have implemented the method and the tool is publicly available. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Samuel Frontull and Georg Moser and Vincent van Oostrom 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.22 urn:nbn:de:0030-drops-180068 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.22 eng https://creativecommons.org/licenses/by/4.0/legalcode