$blog→errstr

do not commit

On Our Way to Reduction: Free Variables

| Comments

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)