Skip main navigation

Introduction to the Lambda calculus

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

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

Reach your personal and professional goals

Unlock access to hundreds of expert online courses and degrees from top universities and educators to gain accredited qualifications and professional CV-building certificates.

Join over 18 million learners to launch, switch or build upon your career, all at your own pace, across a wide range of topic areas.

Start Learning now