Bird–Meertens formalism
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.
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 :
![{\displaystyle f*[e_{1},\dots ,e_{n}]=[f\ e_{1},\dots ,f\ e_{n}].}](../I/m/abdac9dfa9f2077d607f460cbc88eb3a1b97d263.svg)
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 as a suitable binary operator with neutral element e, we have
![{\displaystyle \oplus /[e_{1},\dots ,e_{n}]=e\oplus e_{1}\oplus \dots \oplus e_{n}.}](../I/m/9ec2130e09b98ca06ad5dab69f67c4867ffba2a0.svg)
Using those two operators and the primitives (as the usual addition), and (for list concatenation), we can easily express the sum of all elements of a list, and the flatten function, as and , in currified notation. We have:
![{\displaystyle {\rm {sum}}\ [e_{1},\dots ,e_{n}]=+/[e_{1},\dots ,e_{n}]=0+e_{1}+\dots +e_{n}=\sum _{k}e_{k}.}](../I/m/27f6da65c87fcfaf1f5cb850062fe7184ffbdefd.svg)
![{\displaystyle {\rm {flatten}}\ [l_{1},\dots ,l_{n}]=+\!\!\!+/[l_{1},\dots ,l_{n}]=[\,]+\!\!\!+\;l_{1}+\!\!\!+\dots +\!\!\!+\;l_{n}={\text{ the concatenation of all lists }}l_{k}.}](../I/m/de016b2e0e9f97cd72cefa904a07289051251ebd.svg)
Similarly, writing for functional composition and for conjunction, it is easy to write a function testing that all elements of a list satisfy a predicate p, simply as :
![{\displaystyle {\begin{aligned}{\rm {all}}\ p\ [e_{1},\dots ,e_{n}]&=(\land /)\cdot (p*)\ [e_{1},\dots ,e_{n}]\\&=\land /(p*[e_{1},\dots ,e_{n}])\\&=\land /[p\ e_{1},\dots ,p\ e_{n}]\\&=p\ e_{1}\land \dots \land p\ e_{n}\\&=\forall k\ .\ p\ e_{k}.\end{aligned}}}](../I/m/75ce83a39d68f8e9b47c18d961948ef29835e70d.svg)
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 of neutral element such that the following holds:
![{\displaystyle {\begin{aligned}&h\ [\,]&&=\ e\\&h\ (l+\!\!\!+\;m)&&=\ h\ l\oplus h\ m.\end{aligned}}}](../I/m/b808d49f3a8b67c8cf68aa9ac3401dd7dd9182b4.svg)
The homomorphism lemma states that h is a homomorphism if and only if there exists an operator and a function f such that .
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 has a highly parallel implementation, and so does — most obviously as a binary tree. Thus for any list homomorphism h, there exists a parallel implementation. That implementation cuts the list into chunks, which are assigned to different computers; each computes the result on its own chunk. It is those results that transit on the network and are finally combined into one. In any application where the list is enormous and the result is a very simple type – say an integer – the benefits of parallelisation are considerable. This is the basis of the map-reduce approach.
See also
References
- Lambert Meertens (1986). "Algorithmics — Towards programming as a mathematical activity." (PDF). In J.W. de Bakker; M. Hazewinkel; J.K. Lenstra. Mathematics and Computer Science, CWI Monographs Volume 1. North-Holland. pp. 289–334.
- Lambert Meertens; Richard Bird (1987). "Two Exercises Found in a Book on Algorithmics" (PDF). North-Holland.
- Richard Bird; Oege de Moor (1997). Algebra of Programming, International Series in Computing Science, Vol. 100. Prentice Hall. ISBN 0-13-507245-X.
- Cole, Murray (1993). "Parallel Programming, List Homomorphisms and the Maximum Segment Sum Problem". Parallel Computing: Trends and Applications, PARCO 1993, Grenoble, France. pp. 489–492.