Foundational aspects of syntax
Dale Armin Miller, Catuscia Palamidessi · ACM Computing Surveys · 1999
A large variety of computing systems, such as compilers, interpreters, static analyzers, and theorem provers, need to manipulate syntactic objects like programs, types, formulas, and proofs. A common characteristic of these syntactic objects is that they contain variable binders, such as quantifiers, scoping operators, and parameters. The presence of binders complicates formal specifications and symbolic processing. Consider, for example, a function definition of the form f(x) = let y = e in x + y: When analyzing or transforming a program containing the call f(e ), we might wish to replace f(e ) with the body of f in which x is substituted by e . But we cannot simply apply the substitution [x 7! e ] because a free variable could be captured. For example, if e is the expression y, naive substitution would yield the expression (let y = e in y + y), which is incorrect. Binders are often treated in traditional specifications by adding side conditions on var