α-avoidance


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 need for α in different calculi. In particular, we show how α-paths characterise α-avoidance for several sub-calculi of the λ-calculus like (ⅰ) developments, (ⅱ) affine/linear λ-calculus, (ⅲ) the weak λ-calculus, (ⅳ) μ-unfolding and (ⅳ) 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.