Lambda Calculus

The LambdaCalculus is a system for describing computation using anonymous functions. It is very simple and is used more as a ModelOfComputation than as an actual ProgrammingLanguage. (Note that this page discusses the UntypedLambdaCalculus.)

Anonymous Functions

Most functions that you encounter in math are named functions. Often, their names are f or g. For example:

f(x) = x+5

where f is a function that takes a number x, and returns x+5.

Anonymous functions are functions without names. The notation for the above function is

\x.x+5

\ would be normally written as a lowercase Greek lambda, but it is represented as a reverse solidus in ASCII. The first x gives the name of the the variable to that will represent the parameter. The . separates the variable declaration from the body of the function. Finally x+5 represents the body of the function, what the function will actually compute.

Now \x.x+5 actually is [a written form of] the function. So it would be correct to say that f = \x.x+5, and it would be INCORRECT to say that f(x) = \x.x+5. It is also possible to use a different variable name to produce the same function. So \y.y+5 = \x.x+5. This equivalence is known as AlphaEquivalence.

So functions are created by using the \ symbol. Functions are used by function application. Normally in math, function application is written something like f(2). In the lambda calculus, we bracket differently, and function application is written as (f 2).

Function application associates to the left, so (f a b c) = (((f a) b) c).

Evaluation

When a function is applied, it is really for evaluation. For example:

(\x.x+5 2) -> 2+5

Here the -> means reduces to (in one step). Function application is performed by returning the body of the function with all occurrences of the variable (in this case x) with the parameter (in this case 2). (In the some cases BoundVariable?s may need to be renamed to avoid conflicting with FreeVariables in the parameter--a process known as AlphaConversion?)

Functions with Multiple Parameters

A binary function is represented by currying (See CurryingSchonfinkelling). The idea is to have a one parameter function that returns a one parameter function that returns the result. For example.

\x.\y.(x+y)/2

Represents a function that averages its two inputs. For example, let's average 5 and 7. First note that ((\x.\y.(x+y)/2) 5 7) = (((\x.\y.(x+y)/2) 5) 7) by the left associativity of function application.

((\x.\y.(x+y)/2) 5 7) -> ((\y.(5+y)/2) 7) -> (5+7)/2

Because of this functions can be partially evaluated. ((\x.\y.(x+y)/2) 5) is a function that takes one parameter and averages it with 5.

((\x.\y.(x+y)/2) 5) -> \y.(5+y)/2

Numbers and operators

Above I used numbers like 5 and 2, and operators like + and / to illustrate how anonymous functions are created and used. The actual lambda calculus doesn't have primitives for numbers and operators. It consists only of anonymous functions. It turns out that this is all that is needed to create a TuringComplete language that can represent all computation. The simplicity of the language is why it is useful to reason about computation, and why it is not good for actual programming.

All real programming languages, of course, provided canned versions of the numbers, booleans, and numerous other useful sets, so you don't have to construct them.

Data Types

Data types in the lambda calculus are represent by functions (because that is the only thing there is). For example we can create elements of the Boolean data as follows:

 true := \x.\y.x
 false := \x.\y.y

Here := means we are defining true to be short hand for \x.\y.x. It seems odd to define true as the function \x.\y.x. What does it do? From the above discussion we see that \x.\y.x can be thought of as a function of two parameters (x and y) that returns the first parameter (x). Similarly false is represented by a function of two parameters that returns the second parameters. But in order to understand how this represents true and false, we need to look at functions that use boolean parameters. The primitive function that deals with boolean is the IfThenElse? function. So we need a way of representing it.

if-then-else := \f.f

This definition seems wrong because we'd expect if-then-else to be a function of three parameters. But let's try using it anyway. We'd expect that (if-then-else true a b) ->* a and that (if-then-else false a b) ->* b (note: ->* means reduce to in many steps).

(if-then-else true a b) = ((\f.f) (\x.\y.x) a b) -> ((\x.\y.x) a b) -> ((\y.a) b) -> a

(if-then-else false a b) = ((\f.f) (\x.\y.y) a b) -> ((\x.\y.y) a b) -> ((\y.y) b) -> b

You may have noticed that if-then-else is just the identity function, and doesn't do anything. So we can really just write (true a b) and (false a b) instead.

Now let look at how to compute with this data type. We can define not as follows

not := \f.\x.\y.(f y x)

And we get

 (not true) = ((\f.\x.\y.(f y x)) (\x.\y.x)) = ((\f.\x.\y.(f y x)) (\a.\b.a)) -> \x.\y.((\a.\b.a) y x) -> \x.\y.((\b.y) x) -> \x.\y.y = false.

(Note: In the second step I renamed some bound variable to avoid FreeVariables conflicting with BoundVariable?s later in the derivations)

Other common functions on booleans can be defined as follows

 or := \f.\g.\x.\y.(f x (g x y))
 and := \f.\g.\x.\y.(f (g x y) y)

The definitions of 'and' and 'or' above were originally the other way around. There seemed to be some sort of consensus going that they were the wrong way around and I was able to confirm that using a quick implementation of all of the above in Haskell, so I switched them. -- CaleGibbard?

Recursive Data Types

We've seen how to do simple enumerable types like booleans. We can also represent recursive data types such as natural numbers. In this case, we define NaturalNumbers as ChurchNumerals

The normal primitive operation on NaturalNumbers is recursion. But if we were to define it we'd get the identity function like we did with Booleans. This is because in the lambda calculus the data is represented by their primitive operation. Other common operations on natural numbers can be defined

 + := (\f.\g.\x.\h.(f (g x h) h)
 * := (\f.\g.\x.\h.(f x \y.(g y h))

In general, an element of a data type is represented by a function of n parameters, where n is the number of constructors. And the nth parameter is treated like a function of m parameters, where m is the number of recursive parts needed by the nth constructor in the data type.

Booleans have 2 constructors, True and False. It is not recursive so the two parameters have are functions of 0 parameters. So the type of that booleans have is A => A => A.

Natural numbers have 2 constructors, Zero and Succ. The first constructor is not recursive, the second constructor expects 1 natural number parameters, so the type that natural numbers have is A => (A => A) => A.

  Zero = \x\y.y
  1 = \x\y.xy
  2 = \x\y.x(xy)
  ...
  n = \x\y.x(x...{n-2 times}...(xy)...)

  Succ = \x\y\z.y(xyz)

Lists can be represent by having data attached to the constructors. So a list of objects of type B would be functions having the type A => (B => A => A) => A.

 nil := \x.\f.x
 [1,2] := \x.\f.(f 1 (f 2 x))

Similarly we can represent binary trees as functions of the type A => (B => A => A => A) => A.

See TypedLambdaCalculus, which is a very different thing from the UntypedLambdaCalculus.

For a gentle and humorous introduction into LambdaCalculus, see http://www.jetcafe.org/~jim/lambda.html.

For a not-so-gentle but definitive reference, see Lambda Calculus: Its Syntax and Semantics, by HendrikBarendregt (ISBN 0444875085 ). There is also the paper "IntroductionToLambdaCalculus?" by Barendregt and ErikBarendsen?, available from CiteSeer at http://citeseer.nj.nec.com/barendregt94introduction.html

A beautiful survey of the evolution from mathematics to algorithms can be found in David Berlinski's AdventOfTheAlgorithm? (http://www.amazon.com/exec/obidos/tg/detail/-/0156013916/qid=1077569352/sr=1-1/ref=sr_1_1/104-1783056-3119151?v=glance&s=books) - recommended only for the poetically inclined, who already have a grasp on advanced subjects such as the lambda - a strenuous, but lovely text

The book TheCalculiOfLambdaConversion by AlonzoChurch

According to Amazon, the above book has 108 pages - can anyone with a copy of the book confirm this?

Also see FundamentalConceptsInProgrammingLanguages.

The CurryHowardCorrespondence? provides a link between Natural Deduction type SymbolicLogic and LambdaCalculus. Discovered in the 60s. See http://www.math.uminho.pt/~dil2004/jeslp-abstract-html/