Quick and dirty intro to Lambda Calculus – Post #1

October 17, 2008 — bniemczyk

This is the first of a multi-part post about $\lambda$ -Calculus. I’m going to start with a description of the Untyped $\lambda$ -Calculus. Future articles will include Church Numerals and Typed $\lambda$ -Calculus.

Why?

$\lambda$ -Calculus is important because it has a close tie with functional programming. In fact most functional languages compile to some form of $\lambda$ -Calculus. You could say that $\lambda$ -Calculus is to functional programming what the Turing machine is to imperative programming.

The very basics

Everything is a function in $\lambda$ -Calculus but for the purposes of this post we will extend the core calculus with integers and basic integer operations. In a future post we will go into how integers can be represented as functions (for those unwilling to wait, check out Church Numerals).

Lets start with a sample expression:

$\lambda x . x+y$

This is called an abstraction. In this expression we call the x variable bound and the y variable free. There is one other operation called application. Application takes the form of:

$\lambda x . x+y [x := 3]$

$\lambda$ -Calculus evaluates expressions by simple substitution so the above expression simplifies to $3+y$ . One thing to note about this is that in the term $\lambda x . M$ where $M$ is another term, only free occurences of $x$ get replaced.

$\lambda x . \lambda x . x+z [x := 3]$ therefore simplifies to $\lambda x . x+z$ .

All functions are functions of one variable

$\lambda$ -Calculus does not allow abstractions that take multiple arguments. Instead you write functions that return functions which take the next variable.

$\lambda x . \lambda y . x + y$

simplifying this with $x = 3, y = 4$ we get:

$\lambda x . \lambda y . x + y [x := 3][y := 4]$

$\lambda y . 3 + y [y := 4]$

$3 + 4$

$7$

For conciseness, $\lambda x . \lambda y . M$ can be written as $\lambda xy . M$ but it is important to remember that this is a function that takes the value for x and returns a new function.

The Y combinator

It may have occured to you that recursion cannot be implemented with a simple substitution model and there are no looping constructs. How can this be Turing Complete? Recursion can be simulated by using a function $Y$ such that $Yf \equiv f (Yf)$ (ie. a fixed-point function), assume for the moment that such a function $Y$ exists.

If you wanted to represent the factorial function with recursion you could do it as:

$\text{Factorial }x \equiv \text{ if } x == 0 \text{ then } 1 \text{ else } x * \text{ Factorial }(x-1)$

Since terms are not named, and recursion is impossible, we have to write a function that takes (Yf) as a parameter.

$\lambda f . \lambda x . \text{ if } x == 0 \text{ then } 1 \text{ else } x * f (x - 1)$

we’ll call this expression $\text{ Fact }$ for brevity.

Since: $Yf \equiv f (Yf)$

$Y \text{Fact} \equiv \lambda x . \text{ if } x == 0 \text{ then } 1 \text{ else } x * f (x - 1)$ and f is bound to $Y \text{Fact}$ giving us recursion!