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?
Best Answer
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.