Lambda Calculus – Computerphile


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!

Leave a Reply

Your email address will not be published. Required fields are marked *