Skip main navigation

£199.99 £139.99 for one year of Unlimited learning. Offer ends on 28 February 2023 at 23:59 (UTC). T&Cs apply

Find out more

Introduction to the Lambda calculus

In this article we introduce the basic formalism underlying functional programming, the lambda calculus
Excerpt from
© University of Glasgow

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.

= const
| var
| exp exp
| var -> exp


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

    • In (backslash x rightarrow x+1), the occurrence of (x) in
      (x+1) is bound by the (backslash x).

    • In (y*3), the occurrence or (y) 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 (a) 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

Alpha conversion

  • Alpha conversion lets you change the name of a function parameter

  • 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

 (x -> exp1) exp2

is evaluated as (exp1[exp2/x])


 (x -> 2*x + g x) 42

is evaluated as (2*42 + g ;42)

Eta conversion

  • Eta conversion says that a function is equivalent to a lambda
    expression that takes an argument and applies the function to the
(x -> f x) 

is equivalent to (f)

Example (recall that ((*3)) is a function that multiplies its argument
by 3)

(x -> (*3) x) 

is equivalent to ((*3))

Try applying both of these to 50:

(x -> (*3) x) 50 

is the same as ((*3) ;50)

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 ((y)), it can be “factored out”.

© University of Glasgow
This article is from the free online

Functional Programming in Haskell: Supercharge Your Coding

Created by
FutureLearn - Learning For Life

Our purpose is to transform access to education.

We offer a diverse selection of courses from leading universities and cultural institutions from around the world. These are delivered one step at a time, and are accessible on mobile, tablet and desktop, so you can fit learning around your life.

We believe learning should be an enjoyable, social experience, so our courses offer the opportunity to discuss what you’re learning with others as you go, helping you make fresh discoveries and form new ideas.
You can unlock new opportunities with unlimited access to hundreds of online short courses for a year by subscribing to our Unlimited package. Build your knowledge with top universities and organisations.

Learn more about how FutureLearn is transforming access to education