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

$\endgroup$
  • 1
    $\begingroup$ You never $\alpha$-convert free variables. Only bound variables can be $\alpha$-converted. $\endgroup$ – chi Jan 28 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 at 13:03
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$$

$\endgroup$
  • $\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 at 9:43
  • $\begingroup$ @chi Fair; edited $\endgroup$ – Draconis Jan 28 at 16:04
3
$\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$.

$\endgroup$
  • $\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 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 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 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 at 17:44

Your Answer

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

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