Next: Part 2: Syntax of the Lambda Calculus, Up: Contents
The lambda calculus was developed in 1936 by Lorenzo Church, and is a
mathematical system for defining computable functions (i.e., a model of
computation). Church’s lambda calculus is equivalent in power to the Turning
machine, although Church and Turing both developed their respective models of
computation independently. Church was originally attempting to create a formal
system to serve as the basis of mathematics in general, which he eventually gave
up on, but nevertheless Church’s invention has had far-reaching applications in
computer science, mathematics, and linguistics since its development.
Lambda calculus is a functional language, and like all functional languages, it
is based on the theory of mathematical functions. It has the power of expressing
all computations in terms of functions. It has certain attributes about it,
which make it very convenient for applications such as artificial intelligence,
proof systems, and logic programming. Lambda calculus treats functions and data
uniformly, has very few side effects, and has a very simple but concise
notation. Lambda calculus serves as a model for purely functional languages.
While the applications of the lambda calculus are seen very often today in
programming languages, lambda calculus was developed in the area of mathematical
logic. It is used in a process called Combinatory Logic, which reduces logic to
the simplest possible primitive basis. As you learn the lambda calculus in this
tutorial, you will see how this is easily possible as an application.
Today's applications of the lambda calculus are widely seen in many programming
languages. In the 1950's, LISP was developed as one of the first functional
programming languages, with the lambda calculus at its core, and is used
frequently even today in the development of artificial intelligence. The
language ML (MetaLanguage) incorporates the lambda calculus to develop its
strict type system. More generally, all programming languages, whether
functional or iterative, today owe their type system, largely taken for granted,
to the lambda calculus.
In this tutorial we will be introducing some of the key topics concerning the
lambda calculus. We will start with the basic syntax of the lambda calculus and
it’s general notation. Having given a basic introduction, we will move on to
explain the two different types of expression evaluation strategies. From here
we will cover the three sets of reduction rules (alpha-, beta-, and
eta-reductions), which are necessary to simplify lambda expressions. Finally, we
will cover the notion of Church numerals, which show how lambda expressions can
be used to represent numbers.