## Introduction

The ability to reduce is one of the key components to the λ-calculus. However, you find it directly implemented in compiler optimizations for both functional and imperative languages and as inspiration in Google’s MapReduce.

However, there are some subtleties that must be addressed to go from our λ and λNB calculi to being able to implement reduction. In this post, I mathematically prove that reduction on the λ-calculus terms can be done.

## Define The λ-Calculus

As I described in my initial post
about the λ-calculus, it is a *very* simple definition:

```
t ::= terms:
x variable
λx.t abstraction
t t application
```

## Definition of a Set of Free Variables and Size

Free variables are defined as:

```
FV(x) = {x}
FV(λx.t1) = FV(t1) \ {x}
FV(t1 t2) = FV(t1) ∪ FV(t2)
```

Size is defined as:

```
size(true) = 1
size(false) = 1
size(0) = 1
size(succ t1) = size(t1) + 1
size(pred t1) = size(t1) + 1
size(iszero t1) = size(t1) + 1
size(if t1 then t2 else t3) = size(t1) + size(t2) + size(t3) + 1
```

## Proof that |FV(t)| ≤ size(t)

Unlike many statements in math, intuition and reality are in sync on this
statement. Of course the statement `{ ∀ t, FV(t) ≤ size(t) }`

is true. However,
it is important to formally prove this, since this is key to reduction.

By induction, by proving the following three cases, we can prove the statement
to be true for all `t`

:

### Case 1:

```
t = x
|FV(t)| = |{x}| = 1 = size(t)
```

### Case 2:

```
t = λx.t1
Inductively:
|FV(t1)| ≤ size(t1)
So:
|FV(t)| = |FV(t1) \ {x}| ≤ |FV(t1)| ≤ size(t1) < size(t)
```

### Case 3:

```
t = t1 t2
Inductively:
|FV(t1)| ≤ size(t1) and |FV(t2)| ≤ size(t2)
So:
|FV(t)| = |FV(t1) ∪ FV(t2)| ≤ |FV(t1)| + |FV(t2)| ≤ size(t1) + size(t2) < size(t)
```