# 3.5. The Substitution-Based Model of Evaluation¶

## 3.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:** When substituting \(a\) for \(p\) in \(\lambda x.E\), that is,
\(subst(a,p,b)\) where \(b\) is a \(\lambda\)
abstraction,
there are three sub-cases to consider:

**Case 2a:**\(p\) and \(x\) are one and the same variable, say \(v\) \(subst(a,v,\lambda v.E)\) should return \(\lambda v.E\). For example, \(subst(\lambda z.z, x, \lambda x.x)\) returns \(\lambda x.x\)**Case 2b:**\(p\) and \(x\) are two distinct variables and \(x\) does not occur free in \(a\), \(subst(a,p,\lambda x.E)\) should return \(\lambda x.subst(a,p,E)\). For example, \(subst((w \; z), y, \lambda x.y)\) returns \(\lambda x.(w \; z)\)**Case 2c:**\(p\) and \(x\) are two distinct variables but \(x\) does occur free in \(a\), then \(\lambda x.E\) should be alpha-converted so that Case 2b becomes applicable. For example, \(subst((w \; x), y, \lambda x.x)\) should return \(\lambda a.(w \; x)\) where \(a\) is a appropriate variable chosen during the alpha-conversion process

**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))\).

## 3.5.2. Identifying Substitution Cases¶

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.

## 3.5.3. Performing the Substitution Algorithm¶

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.