Bird–Meertens formalism - Wikipedia
Jump to content
Search
Search
Donate
Create account
Log in
Personal tools
Donate
Create account
Log in
Bird–Meertens formalism
Add languages
Add links
From Wikipedia, the free encyclopedia
Calculus for deriving computer programs
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.<br>Martin and Nipkow provided automated support for Squiggol development proofs, using the Larch Prover.[1]
Basic examples and notations<br>[edit]
Map is a well-known second-order function that applies a given function to every element of a list; in BMF, it is written
{\displaystyle *}
{\displaystyle f*[e_{1},\dots ,e_{n}]=[f\ e_{1},\dots ,f\ e_{n}].}
Likewise, reduce is a function that collapses a list into a single value by repeated application of a binary operator. It is written as
{\displaystyle /}
in BMF.<br>Taking
{\displaystyle \oplus }
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}.}
Using those two operators and the primitives
{\displaystyle +}
(as the usual addition), and
{\displaystyle +\!\!\!+}
(for list concatenation), we can easily express the sum of all elements of a list, and the flatten function, as
{\displaystyle {\rm {sum}}=+/}
and
{\displaystyle {\rm {flatten}}=+\!\!\!+/}
, in<br>point-free style. 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}.}
the concatenation of all lists
{\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}.}
Derivation of Kadane's algorithm[2] Example instances of used laws Map promotion law[3] Fold promotion law[3] Generalized Horner's rule[4] Scan lemma[5] Fold-scan fusion law[5]<br>Similarly, writing
{\displaystyle \cdot }
for functional composition and
{\displaystyle \land }
for conjunction, it is easy to write a function testing that all elements of a list satisfy a predicate p, simply as
{\displaystyle {\rm {all}}\ p=(\land /)\cdot (p*)}
{\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}}}
Bird (1989) transforms inefficient easy-to-understand expressions ("specifications") into efficient involved expressions ("programs") by algebraic manipulation. For example, the specification "
{\displaystyle \mathrm {max} \cdot \mathrm {map} \;\mathrm {sum} \cdot \mathrm {segs} }
" is an almost literal translation of the maximum segment sum problem,[6] but running that functional program on a list of size
{\displaystyle n}
will take time
{\displaystyle {\mathcal {O}}(n^{3})}
in general. From this, Bird computes an equivalent functional program that runs in time
{\displaystyle {\mathcal {O}}(n)}
, and is in fact a functional version of Kadane's algorithm.
The derivation is shown in the picture, with computational complexities[7] given in blue, and law applications indicated in red.<br>Example instances of the laws can be opened by clicking on [show]; they use lists of integer numbers, addition, minus, and multiplication. The notation in Bird's paper differs from that used above:
{\displaystyle \mathrm {map} }
{\displaystyle \mathrm {concat} }
, and
{\displaystyle \mathrm {foldl} }
correspond to
{\displaystyle *}
{\displaystyle \mathrm {flatten} }
, and a generalized version of
{\displaystyle /}
above, respectively, while
{\displaystyle \mathrm {inits} }
and
{\displaystyle \mathrm {tails} }
compute a list of all prefixes and suffixes of its arguments, respectively. As above, function composition is denoted by "
{\displaystyle \cdot }
", 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<br>[edit]
A function h on lists is called a list homomorphism if there exists an associative binary operator
{\displaystyle \oplus }
and neutral element
{\displaystyle e}
such that the following holds:
{\displaystyle {\begin{aligned}&h\ [\,]&&=\ e\\&h\ (l+\!\!\!+\;m)&&=\ h\ l\oplus h\ m.\end{aligned}}}
The...