# Is there a systematic way to know when to alpha-transform free variables?

So, using Church numerals, we define

$$3 = {\lambda} f. {\lambda}x.f(f(f(x)))$$,

and

$$4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$$.

We can then add with an expression like

$$3\ g\ (4\ g\ z)$$

And this reduces to:

$$(g (g (g (g (g (g (g\ z)))))))$$

... but why?

$$g$$ is a free variable in each expression, and my understanding is that you must $${\alpha}$$-convert free standing variables in unrelated expressions. Shouldn't we instead end up with something like

$$(g (g (g (g_2 (g_2 (g_2 (g_2\ z)))))))$$?

• You never $\alpha$-convert free variables. Only bound variables can be $\alpha$-converted. – chi Jan 28 '19 at 9:41
• @chi Thank you for that clarification! That was a real element of my misunderstanding. You should write that up into a partial answer so that it becomes part of the record for future visitors. – Ben I. Jan 28 '19 at 13:03

The answer here is the same as in the other question: one thing is missing here!

$$3 + 4 = \lambda g . \lambda z . 3 g (4 g z) = \lambda g . \lambda z . 7 g z$$

Note that $$g$$ is now a lambda parameter, not a free variable! So now if you want to apply this to something, it'll get substituted in the same everywhere:

$$7 q r = (\lambda g . \lambda z . 7 g z) q r = q q q q q q q r$$

• This could be misunderstood, though. Free variables are never renamed. Variable $g$ above occurs under a $\lambda$ so we could rename it if we wished: $\lambda g.\lambda z.\ 7 g z$ could be converted to $\lambda h.\lambda x.\ 7 h x$. – chi Jan 28 '19 at 9:43
• @chi Fair; edited – Draconis Jan 28 '19 at 16:04

Free variables never get $$\alpha$$-converted, only bound variables can.

In the term $$(\lambda x.\ xy)$$ we can rename the bound variable $$x$$ to any other variable (except $$y$$, since that would cause a name clash). For instance, we can obtain $$(\lambda z.\ zy)$$. Instead, we can never rename $$y$$, since that is free, not being under any $$\lambda y$$.

By contrast, in $$(\lambda y.\ \lambda x.\ xy)$$ we can $$\alpha$$-convert both variables to any other pair of (distinct) variables. This is because now they are both bound.

In the OP's example, $$g$$ is free, so no renaming is possible. At most, we can $$\alpha$$-convert $$f$$ and $$x$$, but not $$g$$.

• So, could you think about bound variables as local variables, and free variables as globals? Meaning that a free $g$ in one location would represent the same idea as another free $g$ elsewhere in the problem, while a bound $x$ would only have a designated meaning within its own function. – Ben I. Feb 1 '19 at 13:33
• @BenI. Yes, that's a rough way to think about it. In an expression/command/piece of syntax $e$, bound variables are exactly the variables which are declared/defined inside $e$ -- the "local" variables, if you want. The others must instead be defined "outside" $e$. E.g. in imperative code {int x=5; print(x+y);} we have x bound and y free. If we "insert" that snippet in a large context, e.g. {int y=4; if(true) { int x=5; print(x+y);}} now the free y is "captured" by the outer declaration, so y is now bound in this larger command. – chi Feb 1 '19 at 13:59
• @BenI. Note that in $\lambda$-calculus we do not have global definitions, so it's best to think of a free variable as "something which has to be defined from outside the $\lambda$-term". – chi Feb 1 '19 at 14:02
• Sure, that makes sense. I was using "global" a little carelessly, I meant it more as you said. :) – Ben I. Feb 1 '19 at 17:44