License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.22
URN: urn:nbn:de:0030-drops-180068
URL: https://drops.dagstuhl.de/opus/volltexte/2023/18006/
Frontull, Samuel ;
Moser, Georg ;
van Oostrom, Vincent
α-Avoidance
Abstract
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.
BibTeX - Entry
@InProceedings{frontull_et_al:LIPIcs.FSCD.2023.22,
author = {Frontull, Samuel and Moser, Georg and van Oostrom, Vincent},
title = {{\alpha-Avoidance}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {22:1--22:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18006},
URN = {urn:nbn:de:0030-drops-180068},
doi = {10.4230/LIPIcs.FSCD.2023.22},
annote = {Keywords: \lambda-calculus, variable capture, \alpha-conversion, developments, safe \lambda-calculus, undecidability}
}
