Bound vs. free variables in the lambda (λ) calculus

---

This mini article is part of a series of articles on the lambda calculus and is also available as a YouTube video.

1. What is the lambda (λ) calculus?
2. (This article) Bound vs. free variables in the lambda (λ) calculus
3. Delta (δ) rules in the lambda (λ) calculus
4. Beta (β) reduction in the lambda (λ) calculus
5. Alpha (α) conversion in the lambda (λ) calculus
6. Eta (η) conversion in the lambda (λ) calculus
7. Summary of the lambda calculus (λ) evaluation rules
8. Lambda calculus (λ) reduction orders and normal form
9. The Church-Rosser theorem and the lambda (λ) calculus

---

Before we move on to look at evaluation rules within the lambda calculus, we need to make a pit stop and cover a specific concept – that is “free” and “bound” variables.

Each occurrence of a variable within a lambda expression is said to be either bound or free.

Consider the following lambda abstraction:

\[(\lambda x.(+\  x \ y)) \ 4\]

A “binding” links a variable name to a value, and so in this expression the variable named x is bound to the value 4. This is because the lambda abstraction defines the variable name in the abstraction as x (it is defined in the λx). In contrast, within this particular expression we cannot see any λy, and so the variable y is not bound to a value. It is said to occur “free” in the expression.

Pretty simple, right? As you will see later, differentiating between bound and free variables is extremely important in the lambda calculus. Let’s move on to looking at the delta rules in the lambda calculus next.