The lambda calculus is a very simple system with profound and far reaching things to say about computer science and math. While there are many more complicated versions, I'm going to describe the original, sometimes called the untyped lambda calculus. The whole point of the LC is to investigate functions and the application of functions to arguments, so lets start of by thinking about functions in math. While normally in math we might say f(x) = x for a function that returns its argument, in the LC functions are so common that they don't even get their own name- they are all named lambda. Since there is no lambda character I will use "\" as it is pretty close. The function f(x) = x would be written as \x.x in the LC. The function f(x, y) = x would be written simply as \xy.x and f(x,y) = x+y would be \xy.x+y. The basic form here is a lambda, a list of variables, and a body.
Parenthesis can be added for clarity, as in (\xy.x+y). Later on perhaps we will talk about what "+" means here and how we can get rid of it and do everything with functions, but for now lets informally assume that things like "+" work the way you expect them to.
As with normal functions if we have some values and a function we can apply the values as arguments to the function, for f(x) = x, f(23) we would write (\x.x)23. The 23 is the argument and instead of parenthesis we just put the function and the values next to each other. The result of (\x.x)23 is 23, as (\x.x) just returns its argument unchanged. Another example might be (\xy.x*y)2 3 (2 gets assigned to x and 3 gets assigned to y) which would result in the expression 2*3 which evaluates to 6.
Notice that the function (\xy.x), for example, has two arguments. In the LC this function is exactly the same as (\x.(\y.x)), the function that takes an argument and returns a function that takes an argument and returns the first argument. This is called currying after Haskell Curry. If we apply only one argument (\x.(\y.x))3 then we get the function (\y.3) which if a function that wants one argument, but no matter what you give it, it will return 3. In the normal notation (\y.3) is f(y) = 3.
It is pretty intuitive that f(x) = x is the same thing as f(y) = y. In the LC it is also true that (\x.x) is the same as (\y.y). Making this explicit brings us to the first rule. The first rule of the lambda calculus is you do not talk about the lambda calculus. I mean, the first rule of the lambda calculus is alpha conversion. This is the "a rose by any other name would smell as sweet" rule and it says that we can replace any variable name with any other name as long as we replace it everywhere it occurs and we don't use a name we have already used. To be clear, its a little more complex then that, but the details aren't as important as the idea.
This post is getting long, but I want to go over the one last rule. We have seen that you can rename variables, and I was sneaky and I didn't mention that when we where applying arguments to functions we where using the most important rule- beta reduction which removes a lambda (we can introduce lambda too, as in given a term like x introducing a lambda would make the term (\y.x). This is called beta abstraction). The last rule is just as simple as the first two. Eta reduction says that a term like this (\x.(\y.y)x), which takes an argument and applies it to another function, is the same as (\y.y). This is like f(x) = x+1, g(x) = f(x). The function g is completely superfluous and we can just use f instead. We can also take a function and wrap it up like so- (\x.x+1) becomes (\y.(\x.x+1)y).
So! Thats all I'm going to say for now. We have introduced the notation and the three rules alpha, beta and eta. There is a great deal more to say just to introduce the LC but hopefully it is not so mysterious now, especially as it is so much like normal math (which is no coincidence of course). In case you are wondering, those really are the only rules. Really. The only objects are variables and lambda terms (terms are just valid sequences of symbols). Modulo some details you now understand one of the fundamental pieces of computer science, as the LC is a system capable of expressing all computable things- it is a system of universal computation. And that is pretty neat.
No comments:
Post a Comment