|Lambda Calculus For Programmers|
|Written by Mike James|
|Thursday, 19 October 2017|
Page 2 of 2
Reduction As Function Evaluation
By our new rule we can replace the x in x z with s, i.e. a b. The resulting new reduced expression is:
You can think of this as a function application.
The function is
and λx can be thought of as defining the function's parameter as being x and the expression following the dot is the function's body.
Hence when you write:
the function is evaluated by having the parameter x set to (a b) in the function body.
The only thing odd about this is that we don't usually write the parameter values after the function in this way. This, however, fits in with Reverse Polish Notation used in most functional languages.
A very common example is the identity function:
which, if you think about its form, simply substitutes the expression you apply it to for x which gives you the original expression again.
For example given:
then reduction means substitute (a b) for x in the function body which gives:
More than one parameter
You can have functions with more than one parameter by using more than one lambda. For example:
which means set z to the first expression (a b) and then set x to the second expression giving:
It is usual to abbreviate such multiple parameter functions by just writing a single lambda for all the parameters.
which means z and x are the parameters for the function body x z.
More than one function
Notice that you can have multiple function applications in a single expression. For example:
which is just two applications of the identify function is equivalent to
as applications are left associative. Applying the inner lambda, i.e. replace x by
after second reduction.
You can repeatedly reduce a lambda expression until there are no more lambdas, or until there are no more arguments to supply values to the lambdas.
Notice that it makes it easier to think about reduction to liken it to function evaluation, but you don't have to. You can simply see it as a game with symbols.
If you think of a Turing machine then what is initially written on the tape is a set of symbols that is converted to a final output as the machine runs. This is computation.
In the case of lambda expressions you start with an initial expression and apply functions to it using beta reduction which produces a new string of symbols. This too is computation.
Bound free and names
Variables that occur within lambda expressions next to a lambda are called bound variable - the others are free variables.
You can think of bound variables as the parameters of the function.
Now that we have beta reduction defined you can see that there is a sense in which it doesn't matter what you call a bound variable. For example:
is the identity function because (λx. x) e gives e. Obviously
is also the identify function.
So we can change the name of a parameter without changing the function. This is alpha reduction (or alpha conversion or alpha-renaming).
Exactly how you do the renaming and how you combine expressions that use the same names for variables can get a little complicated. The safest rule to follow is to change bound variable names so that they are different from any free variables in another expression and to make sure that free variables are have distinct names in different expressions.
For example don't write :
The rules for how to deal with name clashes can seem complicated at first but if you remember that each lambda expression is an entity in its own right and any variables names do not carry across from one entity to another you should find it fairly easy. You can think of it as function local variables if it helps.
You can now see what lambda expressions are all about even if some of the fine detail might be mysterious but what next?
The point is that lambdas provide a form of universal computation using just the symbols and the rule - no extra theoretical baggage needs to be brought into the picture. This is where is gets far too theoretical for some practical programmers. For example we don't just introduce integer values that can be stored in variables. Instead we invent symbols, well lambda expressions that behave just like the integers.
if you have never seen this sort of thing done before it can see very complicated but keep in mind that all we need are some symbols that behave like the integers.
One possible set of such symbols is:
and so on.
You can see the general structure we have a function of s and z and the number of s variables in the body of the function grows by one each time. In general the symbol that represents n has n s variables.
Ok so what have these strange lambda expressions got to do with integers?
The answer is that for a symbol to represent an integer it has to obey the basic properties of the integers - or rather we have to find some other symbols that behave in a way that mirrors the properties of the integers - i.e. addition, subtraction and so on.
One of the basic properties of the integers, more fundamental than arithmetic, is the successor function which gives you the very next integer- or in more familiar terms:
It is fairly easy to create a successor function as a lambda expression:
This may look like a mystery at first but try it out. Apply Succ to the zero symbol - i.e. let's succ it and see:
The first resolution is to substitute
In this expression we can make two more resolutions as the inner function (λsz. z) can be applied to b to give (λz. z)c which can be reduced to give c:
Notice that we can change the parameter names to s and z without changing the lambda expression.
You can try the same calculation for other integer symbols and you will find that it works. The reason it works is that the succ function as defined adds one more occurrence of the b variable to the integer.
From here you can continue to invent functions that add, multiply and so on. You can also define Booleans and logical operations, recursion, conditionals and everything you need to build a computational system.
For most this is two low level and abstract to follow though. After all if it takes this long to create the integers how long would it take to create the rest?
So our account of the lambda calculus finishes here, but you should be able to see that this simple system is capable of being used to construct a Turing machine, and a Turing machine can be constructed that is equivalent to a lambda expression and reduction.
The two are equivalent as far as computation goes.
The role of lambda in programming
Now we get to a difficult part.
Why is this very theoretical idea turning up in highly practical programming languages? It turns up in functional languages because the ideas fit together - the lambda calculus is a functional programming language. In other languages it turns up because it provides a simple way of defining anonymous functions that can be passed to other functions.
In languages such as Java and C# functions only occur as members of objects. There aren't such things as free floating functions that don't belong to some object. There hence cannot be anything like an anonymous function. To avoid adding functions as object in their own right you have to introduce something that looks like a lambda expression. A function head that defines the parameters and a function body that defines what to do with the parameters to obtain a return result. Notice that any lambda expression defined as part of a programming language goes well beyond what we have discussed here - in particular the variables are used as variables and store complex data types and the standard operations are defined. While it is true that all of these things could be reduced to formal lambda expressions this isn't of much interest to the practicing programmer - and nor should it be.
So the lambda expressions that you meet in object-oriented languages really don't have that much to do with the lambda calculus, and not that much to do with the grammar of lambda expressions. They are just anonymous functions that you can pass to another function and a way of avoiding the need to implement functions as objects.
A Programmers Guide To Theory
|Last Updated ( Thursday, 30 November 2017 )|