# When is a variable bound or free in a lambda application?

I am currently reading the book "An Introduction to Functional Programming through Lambda Calculus" (the 2011 edition) and am a bit puzzled by the definitions of free and bound variables with regards to function application.

The book states, in section 2.10, that a variable is bound in an expression if

1. the expression is an application $$(\langle function \rangle \langle argument \rangle)$$ and the variable is bound in $$\langle function \rangle$$ OR $$\langle argument \rangle$$, or
2. the expression is a function $$\lambda \langle name \rangle. \langle body \rangle$$ and the variable is named $$\langle name \rangle$$ or bound in $$\langle body \rangle$$.

Next, it states that a variable is free in an expression if

1. The expression is a single name and the variable has that name, or
2. the expression is an application $$(\langle function \rangle \langle argument \rangle)$$ and the variable is free in $$\langle function \rangle$$ OR $$\langle argument \rangle$$, or
3. the expression is a function $$\lambda \langle name \rangle.\langle body \rangle$$ and the variable is not named $$\langle name \rangle$$ and is free in $$\langle body \rangle$$.

What confuses me is the use of "or" in the definitions of both bound and free variables in applications. I figured that if a variable is not bound, it must be free, and if a variable is not free, it must be bound. So I would expect that if a variable is free, the point 1 in the definition of bound above is inverted, so with boolean logic $$\neg(A \lor B)$$ should become $$\neg A \land \neg B$$.

However, the book doesn't state that a variable is free if it is free in $$\langle function \rangle$$ AND $$\langle argument \rangle$$.

I checked Wikipedia for another reference and it states:

The set of free variables of a lambda expression, M, is denoted as FV(M) and is defined by recursion on the structure of the terms, as follows:

1. $$FV(x) = \{x\}$$, where $$x$$ is a variable

2. $$FV(\lambda x.M) = FV(M) \setminus \{x\}$$

3. $$FV(M N) = FV(M) \cup FV(N)$$

So the set of bound variables in (M N) should be the complement of $$FV(M) \cup FV(N)$$ which I believe would be $$FV(M)' \cap FV(N)'$$ where ' denotes the complement.

The book repeats this definition later in a summary of the chapter, so I'm hesitant to think it would be a typo. I'm thinking that either I'm

• wrong in assuming that bound and free are full complements or
• wrong in thinking that a variable with the same name in the function and argument expressions of an application is the same variable.

What is the correct interpretation here? As an example, in the application expression $$(\lambda x.x\ \ \lambda y.x)$$, is $$x$$ bound or free, or is it senseless to speak of "x" outside of the scope of either the function or argument expressions?

• Aha! So in the example I gave at the end, x is bound AND free, it just depends on which part you consider? If you alpha-converted it to replace the x in the function expression part with a, then x would be free in the application but no longer bound?
• @G_H Yes, exactly. Though I prefer to think of it in terms of bound x and free x really being two different variables with the same name (and if you have multiple $\lambda x$, each introduces a new variable). Jun 14, 2017 at 8:37