HFM2019

History of Formal Methods Workshop

Jeremy Gibbons

The School of Squiggol: A History of the Bird-Meertens Formalism

In 1962, IFIP formed Working Group 2.1 to design a successor to the seminal algorithmic language Algol60 [1]. WG2.1 eventually produced the specification for Algol68 [2]—a sophisticated language, presented using an elaborate two-level description notation, which received a mixed reception. WG2.1 continues to this day; technically, it retains responsibility for the Algol languages, but practically it takes on a broader remit under the current name Algorithmic Languages and Calculi. Over the years, the Group has been through periods of focus and periods of diversity. But the period of sharpest focus covered the decade from the mid 1980s to mid 1990s, when what became known as the Bird-Meertens Formalism (BMF) drew the whole group together again. It is the story of that decade that I wish to tell.

BMF arose from the marriage of Bird’s work in recursive programming [3, 4] and Meertens’ efforts in designing the simple accessible programming languages B [5] and ABC [6]. (Meertens taught Guido van Rossum, who went on to design Python based on some of the ideas in ABC.) The motivation for the BMF is transformational programming: developing an efficient program by starting with an obviously correct but possibly hopelessly inefficient initial specification, then applying a series of meaning-preserving transformations to yield an extensionally equivalent but acceptably efficient final program. The essence of the formalism is a concise functional notation. The functional approach ensures referential transparency, and the straightforward manipulation technique of substitution of equals by equals, as in high school algebra. Concision is necessary in order to make such manipulations feasible with just pen and paper; in particular, like APL, BMF embraced funny symbols such as a slash for reduction (+/ sums a sequence of numbers) and banana brackets ([...]) for homomorphisms, which led to the notation being nicknamed Squiggol. Little emphasis was placed on executability: the notation was ‘wide-spectrum’ [7], accommodating convenient specification notations such as inverses and intersection as well as a sublanguage that obviously corresponds to executable code.

The BMF research paradigm consisted of establishing a body of theorems about recurring problem structures and corresponding solution techniques. Typical examples are fusion properties (combining two traversals over a data structure into one), scan lemmas (replacing the independent reduction of each initial segment of a sequence with a single accumulation along the sequence), and Horner’s Rule (exploiting distributivity, as for products over sums in polynomial evaluation). These three formed the core of a beautiful derivation of a linear-time solution to the Maximum Segment Sum problem [8], a central example in the BMF canon. The effort culminated in Bird and de Moor’s book The Algebra of Programming [9], with a collection of theorems expressed in a relational notation providing greedy and dynamic-programming solutions to optimization problems.

WG2.1’s passion for the approach started to fade after Bird and de Moor’s book appeared, and the group’s focus diversified again. Partly this was due to falling out of love with the Squiggolly notation, which may be convenient for aficionados but excludes the unfamiliar reader; later work favours more conventional syntax. It was also partly due to dissatisfaction with the relational approach, which seems necessary for many optimization problems but is too complicated for most readers (and even for writers!); in fact, Bird is returning in a forthcoming book to tackling many of the same optimization problems using a nearly completely functional approach. I hope to pick out some of the lessons from this ebb and flow of enthusiasm.

References

  1. John W. Backus, Friedrich L. Bauer, Julien Green, C. Katz, John McCarthy, Alan J. Perlis, Heinz Rutishauser, Klaus Samelson, Bernard Vauquois, Joseph Henry Wegstein, Adriaan van Wijngaarden, and Michael Woodger. Report on the algorithmic language ALGOL 60. Communications of the ACM, 3(5):299–314, 1960.
  2. A. van Wijngaarden, B. J. Mailloux, J. E. L. Peck, C. H. A. Koster, M. Sintzoff, C. H. Lindsey, L. G. L. T. Meertens, and R. G. Fisker. Revised report on the algorithmic language Algol 68. Acta Informatica, 5(1–3):1–236, 1975. Also appeared as Mathematical Centre Tract 50, CWI, Amsterdam, and published by Springer Verlag in 1976.
  3. Richard S. Bird. Notes on recursion elimination. Communications of the ACM, 20(6):434–439, 1977.
  4. Richard S. Bird. Improving programs by the introduction of recursion. Communications of the ACM, 20(11):856–863, November 1977.
  5. Lambert G. L. T. Meertens and Steven Pemberton. Description of B. SIGPLAN Notices, 20(2):58–76, 1985.
  6. Leo Geurts, Lambert Meertens, and Steven Pemberton. The ABC Programmer’s Handbook. Prentice-Hall, 1990. ISBN 0-13-000027-2.
  7. F. L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, B. Krieg-Brückner, A. Laut, T. Matzner, B. Möller, F. Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, and H. Wössner. The Munich Project CIP, Volume 1: The Wide-Spectrum Language CIP-L, volume 183 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1985.
  8. Richard S. Bird. Algebraic identities for program calculation. Computer Journal, 32(2):122–126, April 1989.
  9. Richard Bird and Oege de Moor. Algebra of Programming. Prentice-Hall, 1996.
hfm-20191011-gibbons.pdf