Lambda Calc: bound and free variables?

Question

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?

Answer 1

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.

Answer 2

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.