3
$\begingroup$

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)))))))$?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ You never $\alpha$-convert free variables. Only bound variables can be $\alpha$-converted. $\endgroup$
    – chi
    Jan 28, 2019 at 9:41
  • $\begingroup$ @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. $\endgroup$
    – Ben I.
    Jan 28, 2019 at 13:03

2 Answers 2

Reset to default
5
$\begingroup$

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

Your addition result should be:

$$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$$

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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$. $\endgroup$
    – chi
    Jan 28, 2019 at 9:43
  • $\begingroup$ @chi Fair; edited $\endgroup$
    – Draconis
    Jan 28, 2019 at 16:04
4
$\begingroup$

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$.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Ben I.
    Feb 1, 2019 at 13:33
  • $\begingroup$ @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. $\endgroup$
    – chi
    Feb 1, 2019 at 13:59
  • $\begingroup$ @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". $\endgroup$
    – chi
    Feb 1, 2019 at 14:02
  • $\begingroup$ Sure, that makes sense. I was using "global" a little carelessly, I meant it more as you said. :) $\endgroup$
    – Ben I.
    Feb 1, 2019 at 17:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.