3½           3y           32            .

Is it a wonder that little children (many of whom have a most systematic mind) get confused by the mathematics they are taught? One would like the little kids to spend their time on learning the techniques of effective thought, but regrettably they spend a lot of it on familiarizing themselves with odd, irregular notational conventions whose wide adoption is their only virtue.

The much heavier price is that the invisible multiplication all but rules out the introduction of multiple-letter identifiers, thus creating the need of symbols of other alphabets (which —and Whitehead should have known that!— significantly contributed to the pain of typing mathematics). And when the multiple-letter identifiers could no longer be avoided, they were admitted at the price of ambiguity, as

sin (s + i + n)

illustrates.

Remark  I also think that Whitehead made another error of judgement. Brevity is much more effectively obtained by macroscopic measures such as avoiding duplication, case analysis and superfluous nomenclature, than by such microscopic measures as making the multiplication invisible. (End of Remark.)

I now avoid invisible infix operators almost entirely. I do remember a few texts dealing with theorems about strings in which concatenation was denoted by juxtaposition. I could afford that because at the beginning I had declared the types of my one-letter variables: x, y, z  were of type character,  X, Y, Z were of type  (possibly empty) character string: in xX, x would stand for the leading character of the string xX.

The most far-reaching consequence is the introduction of a visible infix operator for function application. I have given it the highest binding power and therefore I have chosen the smallest symbol I could think of: the infix dot “.” . So, instead of the traditional f (x)  I now write f. x .  I have started doing this very tentatively in 1984; I have stuck to the convention and I see more and more people adopting it. One of its attractions is the way in which it caters for λ-abstraction: in 1973 I wrote “wp(S, R)” for the weakest precondition such that statement S establishes postcondition R, but wp. S. R is much more attractive, wp. S now being the predicate transformer associated with statement S. Note that we have chosen the function application dot to be left associative:  wp. S. R is short for (wp. S ). R .

Remark The convention that function application is left-associative has been adopted almost universally. Note that the parentheses then necessary in

 f.(g. x)

can be eliminated by writing the above as

 f ◦g . x

and postulating that functional composition has a greater binding power than functional application. Please note that

 f ◦g ◦h . x

is semantically unambiguous, functional composition being associative. (End of Remark.)

*                *
*

Quantification

I had three major desires with respect to quantification, (i) unambiguous identification of the dummy, (ii) clear delineation of the scope, and (iii) range as a uniform ingredient.

ad(i)  The need for unambiguous dummy identification becomes clear when we consider the list of sets, which starts with the set of the first 10 squares:

 { i ² | i <10 },     { i ³ | i <10 },     { i ⁿ | i < 10 },    { i ⁿ | i < n }

where {i ⁱ⁺¹, i ⁱ⁺², i ⁱ⁺³, .... } would be a possible interpretation of the last set.

ad(ii)  It is already an ambiguity with the traditional summation; compare

3

3

3

3

∑

n2

,

1 +

∑

n2

,

∑

n2 + 1

,

∑

1 +n2

n=1

n=1

n=1

n=1

possible interpretations being, in order,   14,   15,   15 or 17,   17 or 3+n² .  But even logicians write

∀x P(x) ∧ Q

without making clear whether they mean

(∀x P(x)) ∧ Q    or    (∀x P(x) ∧ Q)

which differ if the range for x is empty.

ad(iii)   Although the properties of the underlying (symmetric and associative) operators may differ  —addition and multiplication are not idempotent and maximum and minimum may lack a neutral element— we would like a uniform format. There is, for instance, no reason why summation should have a dummy ranging over consecutive integers.

The format is based on our format for set notation. The set that we formerly described as

{ i ² | i < 10 }

is denoted by

〈 i : i < 10 : i ² 〉

where “i ” is the dummy —if there are more dummies, we separate them by commas—, “i < 10” is the range and “i ²” is the term. The semicolons around the range are only separators, the “angle brackets” delineate the scope of the dummies. The explicit enumeration of the dummies between 〈 and the first : acts like ALGOL 60’s declaration of the local variables of an inner block. The convention enables us to distinguish between

〈 i : i < n : i ⁿ 〉 ,    〈 n : i < n : i ⁿ 〉  and    〈 i, n : i < n : i ⁿ 〉 ;

The last one is the set of all powers for which the exponent exceeds the base, the first two are subsets thereof.

In ALGOL 60, the declaration of a local variable includes the type of that variable, and I see no logical objection against adopting that convention: we could have written

〈 i ∈ ℕ : i < 10 : i ²〉           ,

but we have never done so: I have always found it preferable to supply such information in the surrounding text.

Remark  It took many years before I introduced the angle brackets 〈 〉 ; all that time I used the standard parentheses ( ) . The transition to angle brackets for scope delineation was a great improvement. (End of Remark).

When a quantified operator is applied to the set

〈 i : r. i : t. i 〉   ,

we write it just after the opening angle bracket:

〈↑ i : r. i : t. i 〉   and   〈↓ i : r. i : t. i 〉  .

For the first two, the type of the term t. i must admit addition and multiplication, for the next two, universal and existential quantification respectively, the type of the term t. i had better be Boolean, while for the supremum and the infimum the surrounding text had better specify the partial order with respect to which these extremes have been defined.

From a logical point of view, universal and existential quantification don’t need a variable range parameter since it can be absorbed in the term:

〈∀ i : r. i : t. i 〉    ≡    〈∀ i : true :  r. i  ⇒  t. i 〉 

〈∃ i : r . i : t. i 〉    ≡    〈∃ i : true :  r. i  ∧  t. i 〉

But the range parameter allows more elegant formulae, such as the defining property of the supremum

〈↑ i : r. i : k. i 〉 ⊑ z   ≡   〈∀ i : r. i : k. i  ⊑ z 〉

The explicit range parameter is also welcome from a practical point of view. During many manipulations, the range can remain constant, as is for instance illustrated by de Morgan’s Law

¬〈∀ i : r. i : t. i 〉     ≡    〈∃ i : r. i : ¬t. i 〉

and we shall show below the notational exploitation of such range constancy.

*                *
* 

The proof format

When, for transitive  → , we conclude A → C from A → B and B → C  , we wish for brevity’s sake to write down the intermediate result B only once. We therefore present the calculation  in the following format

	A
→		{hint why A → B}
	B
→		{hint why B → C}
	C

We shall return to the role of the hints later; we now only report that it is absolutely essential that at least one line is available for each hint, so as to discourage economizing on them.

    Another, purely editorial way of reducing duplication is declaring something, once and for all, to hold for all intermediate results of a calculation rather then repeating it each time. We do this for the type specification of variables and the range of dummies. This is a special case of “embedding the calculation in a context”. To illustrate some of these matters, let me show a few ways of proving the following the following simple

Theorem 0.   For associative  •  , we have for all  x, y, z

x • y = y  ∧  y • z = z   ⇒    x • z = z

Proof 0.    This proof uses Leibniz’s Principle in the form

p = q   ∧   f. p    ⇒    f. q

and has the structure of a weakening chain of boolean expressions.

    We prove Theorem 0 by observing for any x, y, z and associative  •

	x • y  =  y   ∧   y • z  =  z
≡	{ predicate calculus }
	y • z  =  z   ∧   x • y  =  y   ∧   y • z   =   z
⇒	{ Leibniz }
	y • z  =  z   ∧   (x • y) • z   =   z
≡	{ • associative }
	y • z  =  z   ∧   x • ( y • z)   =   z
⇒	{ Leibniz }
	x • z  =  z

Here the calculation is embedded in the context of • being associative, a proof shape that is suggested by the formulation of theorem 0.

Proof 1   This proof uses Leibniz’s principle in the form

p = q   ⇒   f. p = f. q

We prove Theorem 0  by observing for associative • and x, y, z satisfying the antecedent

	x • z
=	{ y • z  =  z   from antecedent }
	x • ( y • z)
=	{ • associative}
	(x • y) • z)
=	{ x • y = y  from antecedent }
	y • z
=	{ y • z = z  from antecedent }
	z

(End of Proof 1)

In proof 1, we have been very —one could argue: too !— explicit in our hints: we could have started with

     x • z
=        { antecedent }
     x • ( y • z )

because the observed equality is obviously justified by   y • z = z   ,    which fortunately is one of the conjuncts of the antecedent. But personally I am in favour of making the hints as clear and helpful as possible. And in the style of   Proof 1 we can afford it, for we have embedded our calculation in a more elaborate context —viz. that of the antecedent— from which the hint selects a conjunct only when it is needed. This is more concise  than the style of proof 0, in which conjuncts —e.g.  y • z = z— are dragged along as long as they are needed. In the next example we’ll show another way of how “context” can be used to avoid repetition of the same subexpression.

We recall the defining property of the supremum  ↑  with respect to the complete partial order ⊑:

〈↑ i : r. i : k. i 〉⊑ z   ≡   〈∀i : r. i : k. i  ⊑ z 〉    for all z

Part of the Theorem of Knaster-Tarski states that with  h  defined by

h = 〈↑ y :  y ⊑ f. y : y 〉

we have

h ⊑ f. h

if f is monotonic with respect to ⊑ ,  i.e.,

p ⊑ q   ⇒   f. p ⊑ f. q    for all p, q .

(In another language: “f-application is ⊑- preserving”.)

Proof   In this proof   y ⊑ f.y   is understood to be the range of the dummy y.

To begin with we conclude from the definitions of ↑ and h that h’s defining property is that

(0)         h ⊑ z    ≡  〈∀y :: y ⊑ z 〉   for all z .

And now we observe

	h ⊑ f. h
≡	{ (0) with z := f. h }
	〈∀y :: y ⊑ f. h 〉
⇐	{ ⊑ transitive ; ∀ monotonic }
	〈∀y :: y ⊑ f.y  ∧ f.y  ⊑ f. h 〉
≡	{∀ distributes over ∧}
	〈∀y :: y ⊑ f. y 〉   ∧   〈∀y :: f. y  ⊑ f. h 〉
≡	{ range is y ⊑ f.y, predicate calculus }
	〈∀y :: f. y ⊑ f. h 〉
⇐	{ f monotonic; ∀ monotonic }
	〈∀y :: y ⊑ h 〉
≡	{ (0) with z := h }
	h ⊑ h
≡	{ ⊑ reflexive }
	true

Remark As an aside I would like to point out that the second step, which strengthens

y ⊑ f. h

to

y  ⊑ f. y  ∧  f. y  ⊑ f. h

is absolutely standard. In the original relation the operands differ in two respects: y versus h and the number of f-applications, in the strengthened version each of the differences has been localized in one of the conjuncts, so that they can be dealt with separately. We could have tried the separation the other way round

y  ⊑ h  ∧  h  ⊑ f. h

but as that choice reintroduces the original poof obligation it is not helpful.
(End of Remark)

*                *
*

The role of the hints

With suitable formalization, the hints would fully define the manipulations, and we could omit all the intermediate results, as they would follow. Clearly we have not done so; we consider the intermediate results an essential ingredient of the proof since it is the “intermediate” result that indicates whether we are done or, if not, suggests what to do next.

Our hints were intended to be helpful, and as time went by, we made up our mind how we wanted to help the reader. The most important property of the hint became that it restrict and delineate the search space where the justification should be found. So, if the hint is

{predicate calculus}        ,

then this means that the rules of the predicate calculus suffice. When anything beyond that is needed, it is something, a rule or a property , from the context in which the calculation is embedded; in that case the hint should identify that context element uniquely. For this purpose we commonly number formulae (like “(0)” in the last example).

Remark  For the formula number’s place the left margin is to be preferred over the right margin, because then it is easier to maintain a small distance between the number and the formula it numbers. (A similar remark applies to page numbers in tables of contents.)
(End of Remark.)

In the hints, in our last example, that referred to (0), we gave the instantiations —“z := f. h” and “z := h” respectively— though in a simple example like this it is perhaps a little bit overdone. As soon as the pattern matching might become a problem, however, the instantiation is really helpful and we therefore don’t omit it: our texts should not pose puzzles to the reader.

To save space we sometimes combine two manipulations within a single step. We do not hesitate to do so in the case of independent commuting operations on disjoint subexpressions of the intermediate result. We never combine nested substitutions, for that would be asking for trouble. For such microscopic space savings, the general advice is “In dubio abstine.”; the space savings that can be obtained by proper proof structure —such as effective disentanglement and avoided case analyses— are greater and intellectually more satisfying.

*                *
*

Overloading and an unsolved dilemma

Derivation distributes over addition, i.e.,

d	(x+y)  =	dx	+	dy	.
dt		dt		dt

Usually we don’t consider this an example of overloading, but if x+y  stands for a speed and t is time, than the  +  at the right-hand side adds accelerations.   Yet we don’t feel obliged to introduce two different + signs and to write something like

d	(x +s y)  =	dx	+a	dy	,
dt		dt		dt

primarily because the absence of a notational distinction between the two additions did not introduce any ambiguity.

Let now x and y be two functions which, when applied to t yield two addable values. Then it is customary to define the function that is denoted by x+y by

(x+y). t  =  x. t + y. t            for all t,

Note that, formally, “. t ” now distributes (to the left) over +  .  (In our former example the distribution of d/dt  was “to the right”, so we are still on reasonably familiar ground.)

But now the question arises what meaning to ascribe to x = y  . The traditional interpretation is that x = y is a boolean  expression stating that x and y are the same function, i.e.,

x = y   ≡   〈 ∀t :: x. t = y. t 〉

(Here we have used ≡ for equality between boolean operands.) But in analogy to our previous example x = y could also be interpreted as a boolean function given by

(1)       (x = y). t   ≡   x. t  =  y. t    for all t  ,

i.e.,  the boolean function that yields true wherever x and y coincide, and false everywhere else.

   In many of my writings I have chosen interpretation (1). In addition I have chosen to use a pair of square brackets to denote for a boolean function universal quantification over its domain:

(2)        [b]    ≡    〈 ∀t  :: b. t 〉

The great advantage of the square brackets is that one does not need to introduce a dummy argument. And now one proceeds

	( x and y are the same function )
≡	{ definition of the functional equality }
	〈 ∀t  :: x. t = y. t 〉
≡	{ (1) }
	〈 ∀t  :: (x = y). t 〉
≡	{ (2)  with  b :=  x = y }
	[x = y ]                                      ;

the annoying moral of the story is that to express what we know and appreciate as plain and honest-to-God equality may require an extra pair of square brackets. All this is not very satisfactory, but I don’t know enough of type theory to try to improve the scene.

Nuenen,  25 July 2000

prof. dr. Edsger W. Dijkstra
Department of Computer Sciences
The University of Texas at Austin
Austin, TX 78712–1188
USA