Capture-Avoiding and Hygienic Program Transformations (incl. Proofs)

TL;DR

This paper introduces name-fix, an algorithm that automatically prevents variable capture in program transformations by systematically renaming variables, ensuring hygiene and correctness across various transformation systems.

Contribution

The paper presents a generic, graph-based algorithm called name-fix that guarantees capture-avoiding transformations and can be applied to multiple programming languages and transformation scenarios.

Findings

name-fix effectively eliminates variable capture in generated programs

It guarantees hygiene for a broad class of transformations

Demonstrated applicability in substitution, inlining, lambda lifting, and language compilers

Abstract

Program transformations in terms of abstract syntax trees compromise referential integrity by introducing variable capture. Variable capture occurs when in the generated program a variable declaration accidentally shadows the intended target of a variable reference. Existing transformation systems either do not guarantee the avoidance of variable capture or impair the implementation of transformations. We present an algorithm called name-fix that automatically eliminates variable capture from a generated program by systematically renaming variables. name-fix is guided by a graph representation of the binding structure of a program, and requires name-resolution algorithms for the source language and the target language of a transformation. name-fix is generic and works for arbitrary transformations in any transformation system that supports origin tracking for names. We verify the correctness of name-fix and identify an interesting class of transformations for which name-fix provides hygiene. We demonstrate the applicability of name-fix for implementing capture-avoiding substitution, inlining, lambda lifting, and compilers for two domain-specific languages.