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

Question

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?

Answer 1

wrong in assuming that bound and free are full complements

Yes. Each occurrence of a variable is either bound or free, but not both. But a variable is considered free if it has any free occurrences, and it's bound if it has any bound occurrences; it can be both at once.

Answer 2

A variable $x$ in a λ-term is bound, wherever it is contained, as a subterm, of any λ-term of the form $λx·(⋯)$, otherwise it is free. If it is bound, then it is bound to the $λx$ of the smallest such term it is contained in. If the smallest such term be written as $λx·T$, then (by definition) that particular occurrence of the variable will be free in the λ-term $T$. Thus, the variable $x$ is bound in $λx·(λx·yx)y$, and it is bound to the $λx$ of the subterm $λx·yx$, and is free in the term $yx$. It is not bound to the $λx$ of the larger subterm $λx·(λx·yx)y$, though it is - overall - bound in that term (to the innermost $λx$), nor (therefore) is it free in $(λx·yx)y$.