Alpha - A Tool For Alpha Avoidance
The tool provides an implementation of an alpha avoidance tool, based on th detection of alpha paths. Alpha paths form an adaption of legal paths (Asperti and Guerrini, 1999). The tool uses these paths as computation basis to decide whether alpha-conversion in lambda terms is required to guarantee correct beta-reduction. Depending on whether such paths can be found or not (up to a variable depth), the tool gives one of the following results:
- alpha free: no alpha paths were found and thus no alpha conversion is required.
- alpha can be avoided: alpha-paths were found but are removable; in this case, the tools prints an alpha-equivalent term for which the calculation is alpha-free.
- alpha is unavoidable: an unremovable alpha path has been found; capture avoiding substitution is required to guarantee the correct implementation of beta-reduction.
- maybe, if no alpha-paths have been found, but the computation has not been terminated (the maximum depth has been reached). Note that the problem is inherently undecdiable.
Alpha is developed by members of the Theoretical Computer Science group.
Changelog
2023-02-09: v1.0
This version presents the first version of Alpha, an alpha avoidance tool, based on the computation of alpha paths. Alpha paths constitute an adaption of legal path to detect variable capture in lambda terms; they also form a strict generalisation of chains considered for the mu-calculus, cf. (Endrullis et al. 2011) The tool is accessible via the command line or its web interface.
Contact
Alpha is currently under development by: