Reinventing Zero (the hard way)

In a recent paper, Eric Hehner gives the following beautiful example of people reinventing the concept of zero the hard way:

In the 1991 Toronto phone book, there is a page that helpfully gives the time difference to various places in the world; to the U.K. it says "+5", and to Costa Rica it says "-1". But to Cuba it says "NA", and the legenda explains "time difference not applicable". By 1996 they tried to correct it; for Cuba it says "=", with the same explanation. In 1997 they discovered the number 0 , but they felt the need then, and still do today, to explain that 0 means "no time difference".

Logic for Computer Science

Today, in my reading,  I came across the following:

The only kind of logic necessary in computer science is the predicate calculus, used in the rigorous yet "informal" way of the working mathematician, but perhaps reformulated and extended by useful theorems in the direction presently being investigated by Dijkstra. Formalisms requiring a separate "proof system" or bearing the "formal logician's trademark" should be viewed rather critically.

R. T. Boute, On the Shortcomings of the Axiomatic Approach as presently used in Computer Science, Proc. IEEE COMPEURO 88, System Design: concepts, methods and tools, pp. 184-193, April 1988.

[By the "formal logician's trademark" Boute means the turnstile symbol.]

A Quotation on Object Identity and Time

... Not only was it difficult for him to comprehend that the generic symbol dog embraces so many unlike individuals of diverse size and form; it bothered him that the dog at three fourteen (seen from the side) should have the same name as the dog at three fifteen (seen from the front). ...

From Funes el memorioso by Jorge Luis Borges.

Definitions and Designations

The following is from J. R. Abrial and L. Mussat  ["On Using Conditional Definitions in Formal Theories",  in D. Bert et al (Eds.), ZB2002, Lecture Notes in Computer Science. pages 242-269, Springer, 2002]:

Suppes first introduces two criteria characterizing the definition of new symbols in a formal theory: (1) the Criterion of Eliminability, and (2) the Criterion of Non-creativity. The former requires that "any definition introducing a new symbol may be used to eliminate all subsequent meaningful occurrences (of that new symbol)". The latter requires that any definition of a new symbol "(does not) make possible the derivation of some previously unprovable theorem stated wholly in terms of primitive and previously defined symbols". In other words, a proper definition must not add any extra "power" to a theory, it is just a useful, but not indispensable, extension to it.

This means that definitions are just abbreviations and therefore cannot be used to build a theory; they can only be used to express an existing theory in a different way.

Michael Jackson ["Software Requirements and Specifications", Addison Wesley, 1995, pages 51-54] has some interesting things to say on the subject of the symbols used in specifications:

One way to define a term is to give a designation. That means giving a recognition rule for recognizing some class of phenomenon that you could observe in a domain. In the domain of human relationships you might have these designations:

x is a human being (homo sapiens) = Human(x)

x is male = Male(x)

x is female = Female(x)

x is the biological (genetic) mother of y = Mother(x,y)

x is the biological (genetic) father of y = Father(x,y)

[...] You can use the designated terms in refutable descriptions that make assertions about the domain. [...]

Thus designated terms (symbols) here connect the theory with the domain that the theory describes. Jackson goes on:

Now suppose that you want to make some assertions about grandparents, and aunts and uncles, and cousins and brothers and sisters.  You don't have any designations for these terms, but it will be very inconvenient and difficult to do without them.  there are two ways of making them available for use in your descriptions.  One way is to write some more designations.  For example

x is the genetic full brother of y = Brother(x,y)

[...]

Sometimes this is the right thing  to do.  But probably it is not the right thing here.  The right thing here is to do it the other way: to give a formal definition of each of the new terms, using the terms you have already designated.  [...]

Brother(x,y)  ≙ 
  Male(x) ∧
     ∃ f . (Father(f,x) ∧ Father(f,y) ) ∧
     ∃ m . (Mother(m,x) ∧ Mother(m,y) )

This is a definition in the style of Suppes.   However, I think it is unsatisfactory to regard 'Brother' as purely a convenience to make the theory shorter.  If it was, then it wouldn't matter if you replaced 'Brother' by say 'Aunt' throughout the theory.  The choice of names is important even in strictly unnecessary definitions.  They also designate things in the domain.

In my way of specifying there is no need to introduce new symbols, as all possible symbols already exist.  Writing a specification is just a matter of defining the constraints on these already existing symbols.

(By the way, did you spot that the definition of Brother requires the extra constraint x ≠ y?  Without this I would be my own brother.)

Eric Hehner on Model-Checking

A year or so ago I came across the following passage which nicely highlights the limitations of using model-checking to verify that programs meet their specifications:

There is an approach to program proving that exhaustively tests all inputs, called model-checking. Its advantage over the theory in this book is that it is fully automated. With a clever representation of boolean expressions (see Exercise 6), model-checking currently boasts that it can explore up to about 10^60 states. That is more than the estimated number of atoms in the universe! It is an impressive number until we realize that 10^60 is about 2^200, which means we are talking about 200 bits. That is the state space of six 32-bit variables. To use model-checking on any program with more than six variables requires abstraction; each abstraction requires proof that it preserves the properties of interest, and these proofs are not automatic. To be practical, model-checking must be joined with other methods of proving, such as those in this book. (Eric C. R. Hehner, A Practical Theory of Programming, 2nd ed, 2002)

Incidentally, you can find an online copy of Hehner's ground-breaking book at http://www.cs.toronto.edu/~hehner/aPToP/.  Unfortunately, many people have not yet noticed that the ground has been broken and seem to be busy trampling it flat again!