EWD1213

Introducing a course on calculi

The functions I grew up with, such as the sine, the cosine, the square root, and the logarithm were almost exclusively real functions of a real argument. Sometimes, but not very explicitly, the argument could be allowed to be a little bit more complicated, such as the maximum of two values, a real function defined on a pair of real values, or on two values: whether the maximum was a function of one argument (which had to be a pair) or was a function of two arguments (each of which was a real number) was a question that was avoided. Didn't we talk about the types of the function arguments, we did not talk about the types of the function values either: we did not need to, for to all intents and purposes, all our functions were of type real. (Later this was extended to the type complex, but that was about it.) The nett effect was that I was extremely ill-equipped to appreciate functional programming when I encountered it: I was, for instance, totally baffled by the shocking suggestion that the value of a function could be another function.

Outstanding features of functional programming are (i) the rich type structure needed to make the paradigm of function abstraction and function application sufficiently flexible, and (ii) the predominance of functional composition as structuring device. The clarity and economy of expression that the language of functional programming permits is often very impressive, and, but for human inertia, functional programming can be expected to have a brilliant future, the more so because today's computers admit quite efficient implementations of functional programming languages.

But this is not the complete story. You see, there are people —and I am one of them— that think they have a good reason for not wanting to delegate all calculation to our machines, because they see a role for unprogrammed calculations done by themselves —for instance in the deriviation of proofs and programs—. Whether certain operations are convenient to carry out or not, of course greatly depends on the tools one has to do it with, and in this context we have to accept that a random-access store and the combination of pen and paper are two storage media with totally different characteristics. In particular, evaluating a functional program with pen and paper is a pain in the neck! In contrast, this course focusses our attention on calculi, geared to the use of pen and paper (a medium that has more virtues besides being traditional).

I expect most of our time to be spent, first on the predicate calculus, and then on the relation calculus. For the sake of greater utility, we shall immediately introduce a generalized predicate calculus which later will be used as the framework [sic!] in which to define the relation calculus.

The traditional boolean type is two-valued: {true, false}. If so desired we can model these two values by the 2 subsets of a 1-element universe, the traditional association being that of true with that universe and of false with the empty subset. Our generalization consists of a (still boolean) type whose values can —but don't need to— be modelled by the subsets of a larger universe. As a result, this calculus is widely applicable; for those familiar with it, it often becomes the tool of almost daily reasoning.

The reason to deal with the relation calculus is two-fold. Firstly, relations are a mathematically succinct way of capturing the semantics of not necessarily deterministic programs, secondly, because the relation calculus is more structured than just the predicate calculus, it provides an ideal terrain for the development of heuristics for proof design.