Today we're going to talk about one of my favorite topics in Computer Science,
which is the Lambda Calculus. And in particular, we're going to talk about
three things: we're going to think what actually is it, why is it useful, and
where did it actually come from? So we're going to start with the last
question here - where did it actually come from? This is Alonzo Church, who was
a mathematician at Princeton University in the United States, and he
was the person who invented the Lambda Calculus. And what he was interested in
is what is the notion of a function from a computational perspective. And his
answer to this question is what we now know as the Lambda Calculus. And there's
an interesting piece of history here, which many people don't know.
So, it turns out that Alonzo Church was the PhD supervisor of someone very
famous in computer science -- Alan Turing. And of course Alan Turing,
amongst many other things which he did, he invented Turing machines -- which
Computerphile has done a number of videos on -- and Turing machines capture a basic
state-based model of computation. It's interesting that his PhD supervisor,
Alonzo Church, he captured a basic functional notion of computation with
his Lambda Calculus. And it turns out that these two, quite different notions,
one functional and one state-based, turn out to be equivalent -- and this is what's
called the Church-Turing hypothesis, or part of the Church-Turing hypothesis.
So for Church, a function was a black box, but you're not allowed to look inside.
And what it does is it takes some input, so maybe it takes a number like x, and it's
going to process it in some way, and it's going to produce an output. So maybe it
produces the output x + 1. So this would be a function that takes a single
input, a number called x, processes in some way, and then produces a single
output, which is the number x + 1. And we could have a slightly more
interesting example. Maybe we have a box with two inputs, x
and y, and we process them in some way, and maybe we produce their sum as the
output. So this would be a function which takes two inputs, x and y, processes
them in some way, and then produces their sum, x + y. And there's two important
things about functions in this sense. The first is that they're black boxes; you're
not allowed to look inside, and you can't see the mechanics of what's going on
inside that box, all you can do it put something in and observe what comes out
the other side. And the second important thing is that these functions are pure,
they have no internal state; so all that happens when you map x across to x + 1,
is the magic goes on inside the box, and there's no internal state, there's no
hidden information that we can use. And this is quite different from the notion of
computation that Alan Turing was interested in with his Turing machines -- he had
internal state -- there's no internal state, these are pure mathematical functions. Now
we can think how do you actually define functions in the Lambda Calculus. And
there is a very, very simple syntax for this, which I'll introduce to you now. So
let's think about the increment function in the Lambda Calculus. What you do is
you write down a lambda symbol -- so this is the Greek lower-case letter lambda, and
that says we're introducing a function at this point. And then you just write
down the name of the input, so that was x. And then you have a dot, and then
you say how the output is calculated in terms of the input, that's x + 1. So we
could do the same with addition, you just need two lambdas, and write lambda x,
dot, lambda y, dot, x + y. So this is the function that takes two inputs, x
and y, and then delivers the result x + y. And this is written down formally in
Church's Lambda Calculus exactly like this. So, when you've got a function,
what can you do with it? Well, all you can do is give it some input, let it do its
thing, and it will give you some output. So let's have a simple example of this.
If we take a function like increment, which was lambda x, x + 1, and we
apply it to a number like 5, what actually happens? It's a basic process of
substitution; we're essentially substituting the number 5 here into the body of
this lambda expression and then x becomes 5, so we get 5 + 1,
and then we get the result 6 on the other side. And this is basically all
there is to the Lambda Calculus. It's only got three things: it's got variables,
like x, y and z; and it's got a way of building functions -- this lambda notation;
and it's got a way of applying functions. This is the only three things that you
have in the setting. What is actually the point of the Lambda
Calculus? We've introduced this very simple notation, why should you be
interested in learning about it? I think there's three answers which I would give
to this. The first point I'd make is that the Lambda Calculus can encode any
computation. If you write a program in any programming language, which has ever
been invented, or ever will be invented, or really any sequential programming
language, it can in some way be encoded in the Lambda Calculus. And of course it
may be extremely inefficient when you do that, but that's not the point -- this is a
basic idea of computation, and we want to think how many and what kind of programs
can we encode this, and actually you can encode anything. And this is really the
kind of Church-Turing hypothesis which I mentioned. Alan Turing, you can encode
anything in his Turing machines, and in Church's Lambda Calculus, you can encode
anything. And actually these two systems are formally equivalent -- any Turing
machine program can be translated into an equivalent Lambda Calculus program, and
vice versa. They are formally equivalent. The
second point I would make is that Lambda Calculus can also be regarded as the
basis for functional programming languages like Haskell. So these are
becoming increasingly popular these days. And actually a very sophisticated
language like Haskell is compiled down to a very small core language, which is
essentially a glorified form of Lambda Calculus. So if you're interested in
functional programming languages like Haskell, or the ML family,
these are all fundamentally based on the Lambda Calculus -- it's just kind of a
glorified syntax on top of that. The third point which I would make, is that
the Lambda Calculus is actually now present in most major programming
languages. So this wasn't the case 10 or 15 years ago, but it is the case today. So if
you look at languages like Java, like C#, even Visual Basic, F#, and so
on, all of these languages now encode Lambda Calculus, or include Lambda
Calculus, as a fundamental component. So every computer scientist today needs to
know about Lambda Calculus. What I'd like to end up with is
a couple of little examples of what you can do with it. So, the Lambda Calculus has
basically got nothing in it: it's got variables, it's got a way of building functions, and it's
got a way of applying functions. It doesn't have any built-in data types
like numbers, logical values, recursion and things like that. So if you want to
do these things in the Lambda Calculus, you need to encode them. So I'll end
up showing you a simple encoding, and the encoding which I'm going to show you is
the logical values TRUE and FALSE. And the key to this is to think what do you
do with logical values in a programming language? And the basic observation is
that you use them to make a choice between doing two things -- you say if
something is TRUE do one thing, if something is FALSE do another thing, and
we're going to use this idea of making a choice between two things to actually
encode TRUE and FALSE. So the trick is for TRUE, you write down this lambda
expression. So what it does is it takes two things, x and y, and then it chooses
the first. And FALSE does the opposite. It's going to take two things, and it's
going to choose the second. So we've got two lambda expressions here, both of
which take two inputs, x and y, and one chooses the first one, x, and one chooses the
second one, y. So fair enough, what can we actually
do with this? Well, let's think how we could define a little logical operator.
So, NOT is the most simple logical operator which I could think of. It's going
to flip TRUE to FALSE, and FALSE to TRUE. It's logical negation. Based upon this
encoding, how could I actually define the NOT operator or the NOT function. It's
very easy to do. I will take in a logical value, or a Boolean as it normally called
in Computer Science, after George Boole, who first studied a kind of formal logic. So
we take a Boolean, which will be one of TRUE or FALSE, and here's what we do. We apply
it to FALSE, and we apply it TRUE. And I claim that this is a valid definition
for a NOT function. But I can very easily convince you that it's the case,
because I can do a little calculation. So, let's check, if we apply NOT to TRUE,
that we actually get FALSE. And in just a few steps, using the Lambda Calculus magic,
we'll find that this actually works out. So what can we do here?
Well the only thing we can do is start to expand
definitions. So, we know what the definition of NOT is. It was lambda b, b applied to
FALSE and TRUE, and then we just copy down the TRUE. So all I've done in the
first step here, is I've expanded my definition of NOT -- NOT was defined to be
this Lambda Calculus expression here. Now, I've got a function, which is this thing,
and it's applied to an input, so i can just apply it.
OK, and the function says if I take in a b, I just apply that b to FALSE and TRUE.
So, the thing I'm applying it to is TRUE here, so i just do the little
substitution. Rather than b, I write TRUE, and then I copy down the FALSE, and copy
down the TRUE, and I get down to here. And at this point, you might quite
rightly be thinking this looks like complete rubbish.
I've just written TRUE FALSE TRUE. What does that mean? It means absolutely
nothing. But it means something in the Lambda Calculus, because we continue to
expand. So, what we can do now, is expand the definition of TRUE. We said that TRUE
takes two things, and chooses the first one. So, let's expand it out. So, TRUE is
lambda x, lambda y, x. So, it chooses the first thing of two things, and then we just
copy down the two inputs, FALSE AND TRUE. And you can see what's going to
happen now -- we've got a function here which takes two things and chooses the first
thing. Here the first thing is FALSE, so when we apply the function, we just get
back FALSE. So what you see has happened here, in just
a few steps, we've shown how using this encoding of TRUE and FALSE, and not, we
can actually get the desired behavior. And it's very easy to check for yourself,
if you apply NOT to FALSE, you'll get TRUE. And I'd like to set you a little kind of
puzzle at this point -- think how you could define logical AND,
or logical OR, in this style as well. And I'm interested to see what kind
of definitions people come up with in the comments. So, the very last thing I'd
like to show you is this lambda expression here, which is a very famous
Lambda Calculus expression called the Y combinator, or the Y operator. And actually,
this is the key to doing recursion in the Lambda Calculus. So, as I mentioned,
Lambda Calculus has basically nothing in it, or it's only got three things in it:
variables x, y and z, and so on; a way of building functions; and a way of applying
functions. It's got no other control structures, no other data types, no anything.
So, if you want to do recursion, which is the basic mechanism for
defining things in terms of themselves -- again Computerphile's had videos on this --
you need to encode it. And it turns out that this expression here is the key to
encoding recursion in the Lambda Calculus. And this expression was
invented by someone called Haskell Curry, and this is the Haskell that gives
his name to the Haskell programming language. And he was a PhD student of
David Hilbert, who's a very famous mathematician. The last observation
I'd like to leave you with here, is something that's interested me for many
years. I think there's a connection between this piece of kind of abstract computer
science, or abstract mathematics, and biology. If you look at human DNA, you
have this double helix structure; you have two copies of the same thing,
side-by-side, and this is the key to allowing DNA to self-replicate. If you
look at the structure of this lambda expression here, we have two copies of
the same thing side-by-side. You have lambda x, f applied to x x, and exactly the
same here. This is the key to doing recursion, which is kind of related to
self-replication in a programming language, or in the Lambda Calculus. And
for me, I don't think this is a coincidence -- I think it's kind of
interesting philosophical observation. The Lambda Calculus has this kind of
very clever way of doing recursion, which would take a video on its own to explain
how it actually works, but you can look it up on Wikipedia. And there's a link here,
I think, to biology. Somebody actually found the Y Combinator
so interesting, that they've had it tattooed permanently on their arm, and
you can find a picture of this if you do a quick web search. What would people search for?
The Y combination -- the Y combinator in mathematics or computer science.
And tattoo I'm guessing. Yup!