The Bird–Meertens formalism (BMF) is a calculus for deriving programs from program 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. Martin and Nipkow provided automated support for Squiggol development proofs, using the Larch Prover.

Basic examples and notations

Map:

Likewise, reduce is a function that collapses a list into a single value by repeated application of a binary operator as a suitable binary operator with neutral element e, we have

(for list concatenation), we can easily express the sum of all elements of a list, and the flatten, in point-free style. We have:

for functional composition for conjunction, it is easy to write a function testing that all elements of a list satisfy a predicate p:

" is an almost literal translation of the maximum segment sum problem,, and is in fact a functional version of Kadane's algorithm.

The derivation is shown in the picture, with computational complexities given in blue, and law applications indicated in red. Example instances of the laws can be opened by clicking on [show] compute a list of all prefixes and suffixes", which has the lowest binding precedence. In the example instances, lists are colored by nesting depth; in some cases, new operations are defined ad hoc (grey boxes).

The homomorphism lemma and its applications to parallel implementations

A function h on lists is called a list homomorphism such that the following holds:

The homomorphism lemma states that h and a function f.

A point of great interest for this lemma is its application to the derivation of highly parallel — 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

• Catamorphism

• Anamorphism

• Paramorphism

• Hylomorphism

References

Bibliography