Summary: When substitutions and bindings interact, there is a risk of undesired side effects if the substitution is applied naïvely. The \(\lambda\)-calculus captures this phenomenon concretely, as \(\beta\)-reduction may require the renaming of bound variables to avoid variable capture. In this paper we introduce \(\alpha\)-paths as an estimation for \(\alpha\)-avoidance, roughly expressing that \(\alpha\)-conversions are not required to prevent variable capture. These paths provide a novel method to analyse and predict the potential need for \(\alpha\) in different calculi. In particular, we show how \(\alpha\)-path characterises \(\alpha\)-avoidance for several sub-calculi of the \(\lambda\)-calculus like (i) developments, (ii) affine/linear \(\lambda\)-calculi, (iii) the weak \(\lambda\)-calculus, (iv) \( \mu\)-unfolding and (iv) finally the safe \(\lambda\)-calculus.
Furthermore, we study the unavoidability of \(\alpha\)-conversions in untyped and simply-typed \(\lambda \)-calculi and prove undecidability of the need of \(\alpha\)-conversions for (leftmost-outermost reductions) in the untyped \(\lambda\)-calculus. To ease the work with \(\alpha\)-paths, we have implemented the method and the tool is publicly available.
For the entire collection see [Zbl 1518.68012].