The last step in this section is to formalise what we’ve been doing. This is useful because it helps us describe the precise steps that were taken in a reduction sequence, which is very valuable when we need to share our work with someone else.
We’ve been using \(\beta\) reductions for a while now, so let’s give them a formal description:
\( (\lambda x. E)\; a\; \overrightarrow\beta \; E\; [a/x]\)All this means is that we want to replace all the free occurrences of x with a in the expression E. Remember, we’ve been doing this for a while now, so there’s nothing new here, we’re just giving a name to something we’re already familiar with. Here’s a simple example:
(λq. + q q) 3
A \(\beta\) reduction will perform a \(\beta\) conversion of q by replacing all free occurrences of it in the body (+ q q) with 3. So, in this case:
- E is (+ q q)
- x is q (it’s the thing being replaced)
- a is 3 (it’s the thing bring brought in)
And that’s it! Yes, it looks highly mathematical, but it’s actually nice and straightforward and is something we’ve done so much we can virtually do it in our sleep.
Another process that we’ve been doing all along, this time without even naming it, is \(\delta\) conversion. This is the process of applying a built-in operator (such as +, *, etc.) to its arguments, such as (* 4 3) giving 12. It usually follows a \(\beta\) reduction, as that’s typically when all the arguments are available. If we started with (λx. ( – x 1)) 3, for example, we would do the following:
- \( \overrightarrow\beta (-\; 3\; 1) \)
- \( \overrightarrow\delta 2 \)
\(\beta\) reduction brings the values in and \(\delta\) reductiion evaluates them. The result after full evaluation is said to be in Normal Form, meaning that there are no more redexes left.
We’ll do one final formal notation. This one isn’t an operation we have used yet, but it should make sense. This one is \(\alpha\) conversion, and it changes the name of a variable as in:
(λa. + a a) \(\overleftrightarrow\alpha\)(λb. + b b)
Notice that this is a bidirectional arrow, meaning that this is a two way process, so we can go from (λa. + a a) to (λb. + b b) and back again. The reason for this is that these are the same function — yes, the names are different, but the operation is the same, because each takes a single parameter and doubles it. This is another example of syntax versus semantics; we can change the names of the variables without changing the meaning of the function.
We can’t just arbitrarily change names, though. Consider (λx. ( + x y)) which as x as a bound variable and y as a free variable. If we perform on \(\alpha\) conversion on x to change it to y the result is (λy. ( + y y)) which is not the same function, because now we can’t tell which y is which. However, how about this one:
(λx. + x (λy. + y 1) 2)
If we \(\alpha\) convert on x to change it to y we get (λy. + y (λy. + y 1) 2), which, although there are two variables called y, we can easily tell them apart because we know which is bound by which lambda. That is, the inner y [the (λy. + y 1)] is bound to the inner lambda, while the outer y is bound to the outer lambda.
Let’s formalise this in the same way we did the other processes:
\( (\lambda x. E)\; \overleftrightarrow\alpha \;(\lambda y. E)\; [y/x]\) IF y does not already exist free in E.
All this means is that it is okay to change the name of x to y as long as y doesn’t appear free in the function body, which is how we ensure we don’t get stuck in a situation where we have two different variables with the same name.
Here’s an example of where we might want to use \(\alpha\) conversion. We have this function: (λf. (λx. f (f x)). This will accept a function for the parameter f, pass it into its nested function, which then takes a value for its parameter x and then applies f to x. Nothing too mysterious there, but look at what happens if we try to apply this to a variable x.
(λf. (λx. f (f x)) x
\( \overrightarrow\beta\) (λx. x (x x))
Well, that’s all gone horribly wrong, hasn’t it? Now we have two different variables called x. If we underline the ones brought in during the \(\beta\) reduction it is a bit clearer: (λx. x (x x)), but the problem is that there is no way to tell which is which. If we instead perform an \(\alpha\) conversion on the inner lambda, things would be a lot clearer:
(λf. (λx. f (f x)) x \(\overleftrightarrow\alpha\) (λf. (λy. f (f y)) x
\(\overleftrightarrow\beta\) (λy. x (x y)