Formal identification of Free and Bound variables

We just saw how free and bound variables are similar (but different) to global and local variables. This section will look at how we formally (i.e. what are the steps that we must take) to identify if a variable is free or bound. This will serve us well when we try to evaluate large and complex functions later on. We’ll start with bound variables, and there are two possibilities. The first possibility is that we’re dealing with a simple expression (without any λ part):

X is bound in (E F) if x is bound in or F

That is, X is bound in that expression if it is bound in any part of it. The second possibility is that we are looking at a λ expression:

X occurs bound in (λx. E) if

  1. x==y and x occurs free in E
  2. or, x is bound in E

That is, if x is in the parameter list and does it appear in the body of the function, meaning that it can only appear bound if it is actually used.

This isn’t as complex as it sounds! Let’s work through an example. Is x bound in (λx. + x y)? This is a λ expression, so we apply the first test:

x is in the parameter list (λx)  and it does appear free in (+ x y)  as there is no λ part, so yes, x is bound in (λx. + x y).

Here are a few more examples. Is x bound in (λy. + x y)?

This is a λ expression we apply Test 1: Does x appear in the list of parameters? It doesn’t, so we apply Test 2: Is x bound in Eoccurs free in E so it fails both tests, meaning that x is not bound. How could be bound in in this case? We’ll address that in the next section.

How about some examples without a λ? (+ x 3) can be broken into (E F) of

  • E: +
  • F: x 3

We can see that is not free in E and that it is free in F, so it is free in (E F). What if we divided up the and differently?

  • E: + x
  • F:  3

This time is  free in E and  is not free in F, so we get the same answer, that is, it is free in (E F).

One important thing to note is that not free is not the same as bound. This is why free/bound isn’t the same as global/local. Consider this example:

(λx. + x x)

In this case, y is neither free nor bound.

Next up we’ll see how we can start to scale this up to more complex expressions.