# Lambda Calc: bound and free variables?

I'm trying to work through "Elements of Functional Languages" by Martin Henson. On p. 17 he says:

$v$ occurs free in $v$, $(\lambda v.v)v$, $vw$ and $(\lambda w.v)$ but not in $\lambda v.v$ or in $\lambda v.w$. And $v$ occurs bound in $\lambda v.v$ and in $(\lambda v.v)v$ but not in $v$, $vw$ or $(\lambda w.v)$. Note that free and bound variables are not opposites. A variable may occur free and bound in the same expression.

Can someone explain what this means?

-
Well, it means what it says; it gives examples for free and non-free variables, and for bound and non-bound variables. You should be more specific in saying what you don't understand. – Florian Mar 9 '12 at 17:33
Okay, what does v occurs free in v mean? I do understand that λv.anything typically means v is bound. But then what is (λv.v)v trying to say? – galaxybeing Mar 9 '12 at 17:44
$v$ occurs free in $v$ means that the variable $v$ occurs free in the expression $v$ (which only consists of one variable). Maybe this is what caused the confusion. – Florian Mar 9 '12 at 18:14
Thanks. Got it. – galaxybeing Mar 9 '12 at 23:45

Since you implied you're comfortable on the computer side of the house... it's talking about the scope of a variable. "$\lambda x.$" introduces a new scope which lasts for the length of the lambda expression, and $x$ is a local variable in that scope.

A free variable is one not local to the expression. e.g. in $\lambda x. xy$, $y$ is free.

Some syntaxes for lambda calculus allow a local variable to shadow a global one, just as in common programming languages. In $(\lambda x.x)x$, the lambda expression introduces a local variable $x$ which shadows the 'global' variable by the same name. I like to use colors when dealing with expressions like this, to help distinguish them: the expression is colored $(\lambda {\color{red}x}.{\color{red} x})\color{green}{x}$. The red and green $x$'s are different variables.

Note that this isn't lambda-calculus specific. Quantifiers ($\forall x:$, $\exists x:$) do the same thing. So does integral notation: $\int \ldots \, dx$ (Leibniz notation for derivatives too... sort of...). Such a thing is also usually implied when defining functions pointwise, as in

$$f(x) := x^2$$

As usually meant, $x$ is a variable local to the expression. And $f$ is a global variable! (or maybe a global constant, depending on the context and how one likes to set up the low-level details of syntax)

Do keep in mind that people aren't always consistent about distinguishing between syntactic details. Particularly on topics like whether $x^2$ is an expression that denotes a real number (the square of $x$) or an expression denoting a function in one indeterminate variable (the function that squares its input) to which $x$ is bound.

-
Thanks for the info. Q: What do you mean when you say f is a global variable? Also, (λx.x)x how did you know that the x outside the parens was a "different" variable x? Would there be a better place for a beginner to start to better understand Lambda Calc? – galaxybeing Mar 9 '12 at 23:50

In the more normal mathematical world, we might say something like:

Let $f(x)=x^n$.

In that case, $x$ is a bound variable. If we later wrote:

Let $g(y)=y^n$

Then $g$ would be the same as $f$.

On the other hand, if we said:

Let $h(x)=x^m$

We cannot assert that $h$ is the same as $f$, because $m$ and $n$ are "free" variables.

In $\lambda$-calculus, you have to be careful about which variables are free in an expression. After a while it becomes natural.

-
Yes, this is intuitive for me. Thanks. I guess I'm spazzing a bit early. But still, I'm shaky on what v occurs free in v is really saying. I'm a newbie at the math side of computers and apt to stumble around on these sorts of things. – galaxybeing Mar 9 '12 at 18:01