Introduction to the Lambda calculus
Introduction to the Lambda Calculus

The lambda calculus was developed in the 1930s by Alonzo Church (1903–1995), one of the leading developers of mathematical logic.

The lambda calculus was an attempt to formalise functions as a means of computing.
Significance to computability theory

A major (really the major) breakthrough in computability theory was the proof that the lambda calculus and the Turing machine have exactly the same computational power.

This led to Church’s thesis — that the set of functions that are effectively computable are exactly the set computable by the Turing machine or the lambda calculus.

The thesis was strengthened when several other mathematical computing systems (Post Correspondence Problem, and others) were also proved equivalent to lambda calculus.

The point is that the set of effectively computable functions seems to be a fundamental reality, not just a quirk of how the {Turing machine, lambda calculus} was defined.
Significance to programming languages

The lambda calculus has turned out to capture two aspects of a function:

A mathematical object (set of ordered pairs from domain and range), and

An abstract black box machine that takes an input and produces an output.


The lambda calculus is fundamental to denotational semantics, the mathematical theory of what computer programs mean.

Functional programming languages were developed with the explicit goal of turning lambda calculus into a practical programming language.

The ghc Haskell compiler operates by (1) desugaring the source program, (2) transforming the program into a version of lambda calculus called System F, and (3) translating the System F to machine language using graph reduction.
Abstract syntax of lambda calculus

We will work with the basic lambda calculus “enriched” with some constants and primitive functions (strictly speaking, that is not necessary).

The language has constants, variables, applications, and functions.
exp
= const
 var
 exp exp
 \ var > exp
Variables

Each occurrence of a variable in an expression is either bound or free

In , the occurrence of in is bound by the .

In , the occurrence or is free. It must be defined somewhere else, perhaps as a global definition.


In general, an occurrence of a variable is bound if there is some enclosing lambda expression that binds it; if there is no lambda binding, then the occurrence if free.
We need to be careful: the first occurrence of is free but the second occurrence is bound.
a + (\ a > 2^a) 3  > a + 2^3
Being free or bound is a property of an occurrence of a variable, not of the variable itself!
Conversion rules

Computing in the lambda calculus is performed using three conversion rules.

The conversion rules allow you to replace an expression by another (“equal”) one.

Some conversions simplify an expression; these are called reductions.
Alpha conversion

Alpha conversion lets you change the name of a function parameter consistently.

But you can’t change free variables with alpha conversion!

The detailed definition of alpha conversion is a bit tricky, because you have to be careful to be consistent and avoid “name capture”. We won’t worry about the details right now.
(\x > x+1) 3
(\y > y+1) 3
Beta conversion

Beta conversion is the “workhorse” of lambda calculus: it defines how functions work.

To apply a lambda expression an argument, you take the body of the function, and replace each bound occurrence of the variable with the argument.
(\x > exp1) exp2
is evaluated as
Example:
(\x > 2*x + g x) 42
is evaluated as
Eta conversion
 Eta conversion says that a function is equivalent to a lambda expression that takes an argument and applies the function to the argument.
(\x > f x)
is equivalent to
Example (recall that is a function that multiplies its argument by 3)
(\x > (*3) x)
is equivalent to
Try applying both of these to 50:
(\x > (*3) x) 50
is the same as
Removing a common trailing argument
There is a common usage of Eta conversion. Suppose we have a definition like this:
f x y = g y
This can be rewritten as follows:
f = \x > (\y > g y)
f = \x > g = f x = g
Thus the following two definitions are equivalent:
f x y = g y
f x = g
In effect, since the last argument on both sides of the equation is the same (), it can be “factored out”.
© University of Glasgow