I am building a simple interpreter for untyped lambda calculus, currently trying to implement alpha-reduction.

According to this document on LC:

Alpha-reduction is used to modify expressions of the form "λx.M". It renames all the occurrences of x that are free in M to some other variable z that does not occur in M (and then λx is changed to λz).

It appears that I need to collect the information about the scope (free/bound) of variables prior to alpha-reducing the expression.

How should one go about this? My initial idea was to traverse the AST and produce something similar to a symbol table.

  • 1
    $\begingroup$ Usually "alpha conversion" is used because it doesn't really "reduce" anything. $\endgroup$ – Derek Elkins left SE Jun 5 '19 at 23:40
  • $\begingroup$ At any rate, why not try your idea and see what happens? $\endgroup$ – Derek Elkins left SE Jun 5 '19 at 23:41
  • $\begingroup$ Sounds like you are on the right track. $\endgroup$ – gallais Jun 6 '19 at 10:03
  • $\begingroup$ Your strategy looks fine. Sometimes it is convenient to define a capture-avoiding substitution operator first (you'll likely need that anyway), and reuse that for alpha-conversion. Note that, while the set of free variables is stable under alpha-conversion, the set of bound variables is not, so it should be handled with more care. If substitution is made to be capture-avoiding, you might never need to compute bound variables. $\endgroup$ – chi Jun 6 '19 at 12:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.