My motication (in 1987 this was) This should have been 1984 (and motivation).

I'd also like to add: I had some difficulty in getting my ideas about stable coequalisers across (partly, of course, my fault, because I didn't get the rigt answer, involving stable transitive closures, until 1993). People said, "while programs can't possibly be described by finitary first order theories, because the theory of the natural numbers is an example". I knew that, and it wasn't what I meant. This illustrates a subtlely in first order categorical logic: that the relevant structure consists of *less* than all finite (limits and) stable disjoint colimits. The categorical structure corresponding to first order logic is a (Heyting) pretopos, which need not have coequalisers of arbitrary parallel pairs. For example, the category of compact Hausdorff spaces is a pretopos but does not have all stable coequalisers. (I have a feeling I haven't got this quite right, and Peter Freyd is going to jump on me. I shouldn't be so foolish as to answer mathematical questions on the modem from home!) More recently, Jiri Rosicky and Peter Johnstone have considered the question of what theories can be expressed with finite sketches. As Peter Freyd showed in 1972, this includes the natural numbers. My results and those of Jiri and Peter are more complicated forms of Peter Freyd's original observation. Finally, since my more recent work on categorical recursion, I no longer think that a coequaliser diagram is the best way of presenting a WHILE program categorically (though the diagram I would use now expresses the same logical content). Paul