2
$\begingroup$

I've been learning Lambda Calculus in my free time recently to try and learn how to make programming languages & interpreters. I am struggling a little bit with some inconsistencies on different texts on when to use $\alpha$-conversion to avoid capture in $\beta$-reduction.

For example, in Lectures on the Curry-Howard Isomorphism, it makes no mention of any capture restrictions in its definition of $\beta$-reduction. $$ \label{1}\tag{1} (\lambda x.P)\, Q \rightarrow_\beta P[x := Q] $$

However, in Write You A Haskell, it does

The fundamental issue with using locally named binders is the problem of name capture, or how to handle the case where a substitution conflicts with the names of free variables. We need the condition in the last case to avoid the naive substitution that would fundamentally alter the meaning of the following expression when y is rewritten to x.

$\label{2}\tag{2}[y/x](\lambda x.xy) \rightarrow \lambda x.xx$

By convention we will always use a capture-avoiding substitution. Substitution will only proceed if the variable is not in the set of free variables of the expression, and if it does then a fresh variable will be created in its place.

$\label{3}\tag{3}(\lambda x.e)\,a \rightarrow [x/a]e \quad\text{if}\quad x \notin fv(a)$

Which this piece makes sense to me that if you're substituting a free variable in the body of a lambda expression it can become captured, however the second part is what is throwing me off. The first part appears to be dealing specifically with substituting in lambda abstractions, where the second part dealing with "capture-avoiding substitution" is for any lambda expression.

So I'm not sure I understand why you would need to rename in the following case $$ \label{4}\tag{4} (\lambda x. x\ y)(\lambda y. y x) \rightarrow_\beta [x/x](x y) $$ According to $\ref{3}$, this wouldn't be allowed because $x \in FV(\lambda y. y x)$, but I don't see the problem with it and it seems pretty straightforward to reduce this to $y x$.

When I plug into a lambda calculus interpreter online with steps (such as this one), it agrees and reduces it down to $y x$ with no renaming.

Renaming seems to only apply if the body of the abstraction of the $\beta$-redex is itself another lambda abstraction, such as $$ \label{5}\tag{5} (\lambda x.\lambda y. x y)(\lambda x. x y) \rightarrow_\beta [x/(\lambda x.x y)](\lambda y. x y) $$ which seems to me also according to $\ref{3}$ would not require an alpha conversion because $x\notin FV(\lambda x.x y)$, however when I plug that into the same lambda calculus interpreter it does alpha convert.

One example that I worked out that makes perfect sense to me is the following (using the other notation/definition from Lectures on the Curry-Howard Isomorphism, side note: the differing notations confuse me also): $$ \label{6}\tag{6} \begin{align*} (\lambda y.\lambda x.x y)(\lambda z.x z) &\rightarrow_\beta (\lambda x.x y)[y := (\lambda z. x z)] \\ &\rightarrow_\alpha (\lambda a. (xy)[x := a][y := (\lambda z. x z)]) &\text{if}\quad x\in FV(\lambda z. x z)\,\text{and}\, y\in FV(x y) \\ &\rightarrow (\lambda a.(a y)[y := (\lambda z. x z)] \\ &\rightarrow (\lambda a.a (\lambda z. x z)) \end{align*} $$

and the condition makes sense because you need to rename $x$ if it's in the free variables of the substitution to avoid capture, and $y$ needs to be in the free variables of the body because you can only substitute free variables.

But then when I go back to the other examples I end up re-confusing myself on when I need to rename because it seems inconsistent.

In total, the question is

  1. What am I doing wrong in the examples that are confusing me using the Write You A Haskell ($\ref{3}$) definition?
  2. Am I correct that the renaming only applies when the $\beta$-redex abstraction body is itself another abstraction?
$\endgroup$

2 Answers 2

1
$\begingroup$

The rule from Write you a Haskell is incorrect. The correct rule is:

The reduction $(\lambda x . e) a \to_\beta [x/a]e$, where $x$ is a variable and $a$ and $e$ are terms, holds whenever the no free variable of $a$ is a bound variable in $e$. Here, $[x/a] e$ means a simple replacement of all occurences of $x$ in $e$ by $a$.

Whether $x$ is free in $a$ is completely irrelevant. What is relevant is that free occurences of a variable $t$ in the term $a$ do not become "captured" by $\lambda$-abstractions in $e$.

Your first reduction would thus proceed: $(\lambda x . x y) (\lambda y . y x) \to_\beta (\lambda y . y x) y \to_\beta yx$ with no further opportunities for reduction.

The reduction that confused you is that of $(\lambda x . \lambda y . xy) (\lambda x . xy)$. In this case, we see that $y$ is a free variable in $\lambda x . x y$ but $y$ is a bound variable in $\lambda y . xy$. Thus, it is not possible to do a $\beta$ reduction immediately: we must first do an $\alpha$-conversion. $(\lambda x . \lambda y . xy) (\lambda x . xy) \equiv_\alpha (\lambda x . \lambda z . xz) (\lambda x . xy) \to_\beta \lambda z . (\lambda x . xy) z \to_\beta \lambda z . zy$.

If you permitted an immediate $\beta$-reduction, you would get the following:

$(\lambda x . \lambda y . xy) (\lambda x . xy) \to_\beta \lambda y . (\lambda x . xy) y$

Notice that $y$ no longer occurs free. Continuing:

$\lambda y . (\lambda x . xy) y \to_\beta \lambda y . yy$

So we get that $\lambda z . zy \equiv \lambda y . yy$, which is clearly not what we expect intuitively. This is, of course, because we did an invalid $\beta$ reduction.

$\endgroup$
1
  • $\begingroup$ That's really unfortunate that it has the definition wrong, I was excited to build a language following it. Thank you for the clear explanation! $\endgroup$
    – Alex D
    Apr 2, 2021 at 1:14
1
$\begingroup$

Εven though the answer of Mr Mark Saving is complete, I would like to add something, since I am also studying the CHL isomorphism. There is a formality that is usually admitted, about the notion of pre-terms. By defining pre-terms as you would define regular λ-terms, you can then define α-conversion as an equivalence relation, with a "minimality clause" which enables inductive proofs on the equivalence classes. Finally, λ-terms are defined as these equivalence classes. It can be proved that substitution is always defined for these λ-terms, since α-conversion is assumed to be an automatic procedure.
I know you are looking at these from a programmer's POV, since you actually want to create a language, so there is no "automatic procedure". Despite that, I can send you a pdf of my work, where I try to create a theoretical background for efficient variable renaming. That is, if you are interested.

$\endgroup$
1
  • $\begingroup$ That'd be wonderful. I'm interested in the practical uses of course, but the theory interests me also. Thanks! $\endgroup$
    – Alex D
    Apr 5, 2021 at 16:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .