The Bird–Meertens formalism is a calculus for deriving programs from specifications (in a functional-programming setting) by a process of equational reasoning. It was devised by Richard Bird and Lambert Meertens as part of their work within IFIP Working Group 2.1.
Contents
- Basic examples and notations
- The homomorphism lemma and its applications to parallel implementations
- References
It is sometimes referred to in publications as BMF, as a nod to Backus–Naur form. Facetiously it is also referred to as Squiggol, as a nod to ALGOL, which was also in the remit of WG 2.1, and because of the "squiggly" symbols it uses. A less-used variant name, but actually the first one suggested, is SQUIGOL.
Basic examples and notations
Map is a well-known second-order function that applies itself to every element of a list; in BMF, it is written
Likewise, reduce is a function that collapses a list into a single value by repeated application of a binary operator. It is written / in BMF. Taking
Using those two operators and the primitives
Similarly, writing
The homomorphism lemma and its applications to parallel implementations
A function h on lists is a list homomorphism if there exists an associative binary operator
The homomorphism lemma states that h is a homomorphism if and only if there exists an operator
A point of great interest for this lemma is its application to the derivation of highly parallel implementations of computations. Indeed, it is trivial to see that