On substitution, replacement, and the notion of a function

Copyright Notice

The following manuscript

EWD 949: On substitution, replacement, and the notion of a function

is a draft of Chapters 2 and 3 of

E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, 1990.

Permission to reproduce the manuscript here has been granted by Springer-Verlag New York.

On substitution, replacement, and the notion of a function.

with respect to substitution and replacement, two extreme attitudes seem to prevail. Either the mechanisms are deemed so simple that the author uses them without any explanation or statement of the rules, or the author tries to give a precise statement of the most general rules and ends up with 200 pages of small print in which all simplicity has been lost. Neither is entirely satisfactory for the purposes of this monograph.

The first extreme has to be rejected in view of our stated goal of presenting fairly "calculated" arguments. The "mindless" manipulation of uninter- preted formulae that is implied by "letting the symbols do the work" is clearly impossible without a sufficiently clear view of the permissible manipulations.

The second extreme has to be rejected because this is not a treatise on formal logic and would probably provide much more than needed for the limited scope of the theory we have set out to develop.

In this section we shall try to sail between scylla and charibdis by mainly confining our selves to the identification of the sources of complication, as an awareness of them should suffice to protect the human formula manipulator from making the "silly" mistakes.

It all starts innocently enough. Given

(0)

1 3 = 5 + 8

and

(1)

x > 1 3

we all feel pretty confident in concluding

(2)

x > 5 + 8

；

the equality (0) tells us that in (1) we may replace 13 by $5 + 8$ without changing (1)'s value. We are, however, courting trouble as soon as we view the transition from (0) to (2) purely as a matter of string manipulation.

(3)

y < 1 3 1

and

(4)

z = q - 1 3

，

we should conclude neither

(5)

y < 5 + 8 1

from (0) and (3), nor

(6)

z = 9 - 5 + 8

from (0) and (4). The moral of the story is that there is more to it than just the manipulation of strings of characters.

Though strings of characters are what we write down and see, the only strings we are interested in are formulae that satisfy a formal grammar. The role of this grammar goes beyond defining which strings represent well-formed formulae, it also defines how a well-formed formula may be parsed. Indicating permissible

parings with parentheses, we would get

$\left( {2}^{1}\right) \times > \left( {5 + 8}\right)$ $y < \left( {5 + \left( {81}\right) }\right)$ $\left( {6}^{\prime }\right) = \left( {\left( q - 5\right) + 8}\right)$

Comparing (2') with (5') and (6') reveals what went wrong. "Replacing equals by equals" should be a reversible operation, i.e. from (0) and (2) we should be able to conclude (1), as, indeed, we are. Whereas in (2') $5 + 8$ occurs as syntactic unit of an admissible parse, in (5') and (6') it does not. The moral of the story is that, apart from the internal structures of the subexpressions exchanged, the two formulae equated should admit the same parsings. The consequences of this requirement obviously depend on the grammar adopted: with a grammar with operators of different binding power, for instance, a parenthesis pair may have to be introduced.

Remark We don't require the grammar to be unambiguous. For instance, the associativity of the addition might be rendered grammatically in a production rule like

$<$ sum> $\because$ <addendum> Sum> (End of Remark.)

*

We get another complication with grammars in which variables may have a limited scope, such as the dummy i in the quantied expression

EWD 949-3

(Ai: Q.i) . Here the outer parenthesis pair delineates the scope of the dummy i , which is therefore said to be "local to this expression"; a variable that occurs in the text of an expression, but is not local to it or to one of its subexpressions is said to be "global to that expression". (For "local" and "global", also the terms "bound" and "free" respectively are used.) Sometimes it is convenient to regard "global to an expression" as "local to that expression's environment".

Variables are place holders in the sense that their main purpose is to get something substituted for them. More precisely: when we substitute something for a variable, each occurrence of that variable is replaced by that same something. Identifying different variables by different identifiers is a means for indicating which places have to be filled with the same something in the case of substitution. From

[ 2 \cdot X = X + X ] \qquad \mathrm {f o r a n y} X

we may thus derive

[ 2 \cdot Y = Y + Y ] \qquad a n d

[ 2 \cdot (Y - Z) = (Y - Z) + (Y - Z) ]

whereas the "conclusion"

[ 2 \cdot (Y - Z) = (Y - Z) + X ]

is unjustified, not all occurrences of $X$ having been replaced.

In the absence of local variables, all variables are global and life is simple. There are as many variables as we have identifiers, they are in one-to-one corresspondence to each other to the extent that we hardly need to distinguish between the variable and the identifier identifying it.

But consider now an expression like

(7) $\left( {A,i : {P}{i}}\right) \vee \left( {E,j : {Q}{j}}\right)$

In this expression we have four variables: $P,Q$ , i and j. The first two are global, i.e. expres- sion (7) is deemed to occur in an environ- ment that may have more occurrences of $P$ and Q,and substitution of something for P (or Q) is deemed to apply to all occurrences of $P$ (or Q),both in (7) and in its environ- ment. As long as the environment of an expression like (7) is left open,for each of the variables global to that expression the set of its occurrences is open-ended.

The other two, i and j , are sealed off, so to speak: their sets of occurrences are closed. The first one, introduced after the quantifier A , is local to the first disjunct, and the second one, introduced after E is local to the second disjunct. Their occurrences are by definition confined to their respective scopes as delineated by the parenthesis pairs.

In the environment of (7), $P$ and $Q$ play different roles: $P$ refers to the term in the universally quantified expression and $Q$ to the

term in the existentially quantified expression. In contrast, the variables i and j play in the environment no role at all. As a result it should not be very relevant for the environment which identifiers have been used to denote these local variables. In fact, instead of (7), we could equally well have written

(Ai: Pi) (Ek: Q.k)

or even

$\left( q\right) \left( {A,i : P,i}\right) \vee \left( {E,i : Q,i}\right)$

Since a variable local to an expression plays by definition no role in that expression's environ-. ment, we can always choose a fresh identificant to denote it. In (9) we have carried that freedom to its ultimate consequence and have used the same identificant for both local variables. No confusion arises as it is still quite clear which variable is universally quantified and which is existentially quantified.

Note that we have taken a major step. The one-to-one correspondence is no longer between variable and identifier, but between variable and identifier together with its scope.

It is customary to go one step further.

(10) $\left( {A,i : {P}{i} \vee \left( {{E}{j} : {Q}_{j}}\right) }\right)$

In view of (9), we would like to permit

(11) $\left( {A,i : {P}{i}v\left( {{E}{i} : Q}_{i}}\right) }\right)$

as well. In fact we do.

Scopes, being delineated by matching parenthe- thesis pairs, are either disjoint, as in (7), (8), and (9), or nested, as in (10). But what about (11)? Well, the scopes are still nested: the inner scope pertains to the existentially quan-tified variable, the outer scope to the universally quantified variable. More precisely, for any occurrence of a variable we find the scope of that variable by looking for the smallest scope (i) that introduces the identifier used to denote the variable and (ii) whose delineating parentheses surround the occurrence. A consequence of this rule is that, in (11), the double usage of the identifier i has created a "hole" in its outer scope: the scope of the universally quantified i extends in principle -as in (10)- from the outer opening parenthesis until the outer closing parenthesis, but in (11), over "(Ei:: Q.i)", though within the outer parenthesis pair, the identifier i does not refer to the universally quantified variable, but to the existentially quantified one.

The things to remember are

(ii) that no identifier may occur outside its scope , and (ii) we are always free to replace, all through its scope, all occurrences of a local variable we assume that the reader remembers this and shall often not mention explicitly its specific consequences. For instance, in the

presentation of the axiom

[ (\underline {{A}} _ {i}: Q \vee P _ {i}) \equiv Q \vee (\underline {{A}} _ {i}: P _ {i}) ]

we feel free to omit the standard caveat "provided i is not global to Q"; we should remember that we are free to view i as a fresh ideni. Pier and that, were i global to Q , its oc- currence in the second Q would be outside its scope. Hence we prefer to consider the caveat as "obvious".

Remark That last desire is perhaps very naive in view of the amount of effort logicians have spent on explaining "bound" versus "free" variables. They consider perhaps more complicated manipulations than we do. From the moment that we decided to delineate the scopes of local variables explicitly by an obligatory parenthesis pair and to adopt a syntax that leaves no doubt as to which local variable(s) a scope pertains - and this decision was taken many years ago - we never made an error due to clashing identifiers. One manipulates in the constant awareness that each local variable could have been identified by a fresh identifier; it is a permanent supervision not unlike the physicist's awareness that his formulae should be invariant under change of units or of coordinate system. (End of Remark.)

We have to say a word or two about functions because, depending on the ways permitted for their definitions, it may be ques-

fionable whether they are well-defined at all. Fortunately, our functions will be simple.

First of all, they will be total functions of arguments of familiar types, such as boolean or integer - which we deem well-understood - and structures thereof. Their values will be of similarly simple types: a new function is always a mapping from a previously introduced domain to a previously introduced domain.

Aaside A, say, integer function that accepts itself as argument, is of a type $\alpha$ that satisfies the type equation

\alpha = \alpha \rightarrow i n t

with such a recursively defined type it is no longer obvious whether a function definition makes sense or can lead to a contradiction. Such functions, fortunately, fall outside the scope of this monograph. (End of Aaside.)

Secondly, our ways of defining functions are very simple. They are only two. Firstly we define functions by means of expressions (in their arguments), built from previously defined primitives. An example would be the definition of square as a mapping of type int → int) by

s q u a r e. x = x ^ {2}

Furthermore we shall define functions as

EWD949-9

parameter(s). In that case we take upon our- selves to prove that such an equation has for any value of the parameter(s) a unique solution.

Note We could have defined square.x as the solution of

y: (y = x ^ {2})

• here the prefix $y$ : denotes that the following boolean expression is considered an equation in the unknown $y\ldots$ The above equation, however, is somewhat special in the sense that the task of solving it is empty. (End of Note.)

Our main use of the notion of a function will be that, for $p$ a function, we appeal to

(x 0 = x 1) ⇒ (f. x 0 = f. x 1)

a rule for which we give credil to Leibniz by naming it after him. Since the argument might be a structure and since the function value might be a structure, the above should be formulated as

[ x 0 = x 1 ] ⇒ [ f. x 0 = f. x 1 ]

But now a slight problem emerges, that is most easily shown with a simple example. Let us define the function $\rho$ , mapping two boolean structures on a boolean structure, all three on the same space, by

[ f. X. Y \equiv [ X ] \wedge Y ]

Leibniz's rule gives us immediately

EWD 949-10

\begin{array}{l} [ X _ {0} \equiv X _ {1} ] ⇒ [ f. X _ {0}. Y \equiv f. X _ {1}. Y ] \ [ Y _ {0} \equiv Y _ {1} ] ⇒ [ f. X. Y _ {0} \equiv f. X. Y _ {1} ] \ \end{array}

Both conclusions are correct; the trouble with the last one is that it follows from the stronger

[ (Y _ {0} \equiv Y _ {1}) ⇒ (f. X. Y _ {0} \equiv f. X. Y _ {1}) ]

which is also correct, whereas the similar strength- ening of the first conclusion would be incorrect. Evidently, the ways in which $f$ depends on its two arguments are fundamentally different.

To denote the difference, we call $f_{X,Y}$ a spatial function of $X$ and a punctual function of $Y$ . We shall return to the distinction later.

Austin, 21 April 1986

prof. dr. Edsger W. Dyrkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1111 United States of America