22.5.1. Substitution Algorithm¶

In this section, we continue our investigation of the semantics of the lambda calculus. Now that we understand the meaning of each one of the three types of lambda expressions (see Semantics of the Lambda Calculus), the meaning of free and bound variables (see Free and Bound Variables) and how bound variables can be systematically renamed (see Alpha-Conversion), we have all of the tools we need to explain the meaning of function calls in the lambda calculus. Note that, since functions are the only entities in the lambda calculus, interpreting a lambda calculus program boils down to executing function calls.

First, consider how you would execute the following function call in your head:

f(8)

You would first look up the definition of the function f, say:

var f = function(x) { return  2 * x - 5; };

Then you could compute the value of f(8) by computing the value of the body of f after substituting 8 for x in it, yielding 2*8 - 5 = 11. This intuitive approach to evaluating function calls naturally leads to a substitution-based model of interpretation. In this section, we discuss a well-known algorithm for performing substitutions in the lambda calculus.

Since both the body of a function and the argument of a function call can be arbitrary lambda expressions, we need an algorithm that can substitute any lambda expression \(a\) (the argument) for the variable \(p\) (the parameter of the function) in the lambda expression \(b\) (the body of the function). In this section, we forget about the interpretation of \(a\), \(p\) and \(b\) as components of a function call. Instead, we describe the algorithm in general terms, that is, as an algorithm to substitute \(a\) for \(p\) in \(b\), which we denote by:

where \(a\) and \(b\) are arbitrary lambda expressions and \(p\) is any variable.

Note that \(subst(a, p, b)\) means "substitute \(a\) for \(p\) in \(b\)" or equivalently, "replace \(p\) by \(a\) in \(b\). Whichever way you choose to phrase it, \(b\) is always the expression inside which we are performing the substitution, \(p\) is always the expression that gets taken out of \(b\) and \(a\) is always the expression that gets inserted into \(b\).

Now, back to the substitution algorithm. Since \(b\) is an arbitrary lambda expression, looking back at the BNF grammar for the lambda calculus, we see that we must consider three cases for \(b\), namely a variable, a lambda abstraction or an application expression. Therefore, our description of the algorithm is broken down into three numbered cases.

Case 1: If \(b\) is a variable, say \(x\), then \(subst(a, p, b)\) becomes \(subst(a, p,x)\). Recall that \(p\) and \(x\) are generic variables. So we need to distinguish two subcases. First, if \(p\) and \(x\) are the same variable, say \(v\), then \(subst(a,p,x)\) is really \(subst(a,v,v)\), whose value is \(a\), because that is what we get when we replace \(v\) by \(a\). We call this part of the algorithm Case 1a. Second, if \(p\) and \(x\) are two different variables, then \(subst(a,p,x)\) is equal to \(x\), because the variable \(p\) does not occur in \(x\) and no substitutions are needed or possible. We call this part of the algorithm Case 1b

Let's look at two examples of substitutions that belong to Case 1. First, in \(subst(\lambda x.x, u, v)\), \(v\) is a variable that is different from \(u\). Therefore, this example matches Case 1b, and the output of the algorithm is \(v\). On the other hand, \(subst(\lambda y.(y\ x), u, u)\) falls into Case 1a, since both \(p\) and \(b\) are equal to the same variable \(u\). So, the algorithm returns \(\lambda y.(y\ x)\).

Case 2: To be completed

Case 3: If \(b\) is an application expression, say \((e_1\ e_2)\), where \(e_1\) and \(e_2\) are arbitrary lambda expressions, then the value of \(subst(a,p,b)\), really \(subst(a,p,(e_1\ e_2))\), is \((subst(a,p,e_1)\ subst(a,p,e_2))\), that is, the application expression that is obtained by substituting \(a\) for \(p\) recursively in each component of the original application expression.

As an example, consider \(subst(\lambda y.(y\ x), u, (\lambda v.u\ u))\). Since the expression we are substituting into (i.e., the third one) is an application expression, the algorithm requires us to return the application that results from recursively substituting \(\lambda y.(y\ x)\) for \(u\) in both components of this application. Since we already performed these two substitutions in the examples listed above, the final result of the algorithm is \((\lambda v.\lambda y.(y\ x)\ \lambda y.(y\ x))\).

22.5.2. RP 15 part 2¶

The following exercise is good practice for identifying which case applies at each step of the substitution algorithm. To get credit for this randomized problem, you must solve it correctly three times in a row.

22.5.3. RP 15 part 3¶

The following exercise will test your ability to complete a full substitution by applying the algorithm scrupulously. To get credit for this randomized problem, you must solve it correctly three times in a row.