Changing Bound and Local Variables

1. An Example from Programming

Consider the following three snippits of C++ (or Java) code:

Snippit 1:

int addThem(int x, int y, int z) {
   int p, q;
   p = x + y;
   q = p + z;
   return q;
}

Snippit 2:

int addThem(int x, int y, int z) {
   int r, s;
   r = x + y;
   s = r + z;
   return s;
}

Snippit 3:

int addThem(int x, int y, int z) {
   int p, y;
   p = x + y;
   y = p + z;
   return y;
}

In Snippit 1, x, y, and z are formal parameters, and p and q are local variables. p and q are defined only within the function addThem. A similar observation applies to Snippit 2. Compare Snippit 1 to Snippit 2. You will see that they perform exactly the same computation.

Now compare Snippit 1 to Snippit 3. As in Snippit 2, we have changed the names of the local variables, but now we have a naming conflict: we are using y in two different ways! Snippit 3 is not equivalent to Snippit 1 or Snippit 2.

2. An Example of a Definition

Now consider what it means for a number to be even. Compare the following three statements:

Definition 1: An integer n is said to be even if there exists an integer k such that n = 2k.

Definition 2: An integer n is said to be even if there exists an integer p such that n = 2p.

Definition 3: An integer n is said to be even if there exists an integer n such that n = 2n.

Compare definitions 1 and 2. They say the same thing! In definition 1, k is a local variable, just like the local variables p and q in Snippit 1. The scope of the variable k is the second part of the definition. We can write Definitions 1 and 2 more formally in the following way:
   n is even if and only if (∃k)(n = 2k)
   n is even if and only if (∃p)(n = 2p)
The scope of the variable k is (n = 2k). The scope of the variable p is (n = 2p).

Now look at "definition" 3. It makes no sense at all! As with Snippit 3, we have violated the rule against using a symbol to mean two different things at the same time.

You may have observed that when I write formal logical expressions, I always enclose the quantifier in parentheses as in (∃k), and also enclose the scope of the quantifier in parentheses. This practice eliminates lots of possibilities for confusion. In logical expressions, local variables are usually called bound variables. Local variables in programs, and bound variables in expressions, are just two different manifestations of the same concept.

We can summarize what we have learned here in two rules:

RULE 1: Never use a variable to mean two different things at the same time.

RULE 2: A local (or bound) variable can always be changed to any other variable without changing the meaning, provided that doing so, we do not violate Rule 1.

3. Sometimes we MUST change a bound or local variable.

Let's examine the following "proof" of the statement, "The sum of two even numbers is even.":

Let m and n be two even numbers. Since m is even, by the definition there is an integer k such that m = 2k. Since n is even, by the definition there is an integer k such that n = 2k. Then m + n = 2k + 2k = 2(k + k). This shows that m + n is even.

In this "proof", we used our first form of the definition of even twice. But let's take an example: suppose m = 14 and n = 18. Since m = 2k, we have k = 7; and since n = 2k, we have k =9. Something is clearly wrong here. The problem is that we have violated Rule 1: we have used k to mean two different things.

Now lets rewrite the above "proof" using the first form of the definition of even for m and the second form for n. Here is what we get:

Let m and n be two even numbers. Since m is even, by the definition there is an integer k such that m = 2k. Since n is even, by the definition there is an integer p such that n = 2p. Then m + n = 2k + 2p = 2(k + p). This shows that m + n is even.

And this proof is correct.