Bird–Meertens Formalism

Richard Bird and Lambert Meertens developed the Bird–Meertens formalism (BMF), a calculus for deriving programs from specifications through equational reasoning in functional programming. The formalism, sometimes called "Squiggol," enables algebraic manipulation of expressions to transform inefficient specifications into efficient programs, as demonstrated by Bird's derivation of Kadane's algorithm for the maximum segment sum problem.

Bird–Meertens formalism The Bird–Meertens formalism BMF is a calculus /wiki/Proof calculus for deriving programs /wiki/Program derivation from program specifications /wiki/Program specification in a functional programming /wiki/Functional programming setting by a process of equational reasoning. It was devised by Richard Bird /wiki/Richard Bird computer scientist and Lambert Meertens /wiki/Lambert Meertens as part of their work within IFIP Working Group 2.1 /wiki/IFIP Working Group 2.1 . It is sometimes referred to in publications as BMF, as a nod to Backus–Naur form /wiki/Backus%E2%80%93Naur form . Facetiously, it is also referred to as Squiggol , as a nod to ALGOL /wiki/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 /wiki/Larch Prover . 1 cite note-1 Basic examples and notations edit /w/index.php?title=Bird%E2%80%93Meertens formalism&action=edit§ion=1 Map /wiki/Map higher-order function is a well-known second-order function that applies a given function to every element of a list; in BMF, it is written : Likewise, reduce /wiki/Fold higher-order function is a function that collapses a list into a single value by repeated application of a binary operator /wiki/Iterated binary operation . It is written as in BMF. Taking as a suitable binary operator with neutral element e , we have 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 /wiki/Flatten higher-order function function, as and , in point-free style /wiki/Tacit programming . We have: Kadane's algorithm /wiki/Kadane%27s algorithm 2 cite note-FOOTNOTEBird1989Sect.8, p.126r-2 | Example instances of used laws | |---| Similarly, writing for functional composition /wiki/Functional composition and for conjunction /wiki/Logical conjunction , it is easy to write a function testing that all elements of a list satisfy a predicate p , simply as : Bird 1989 transforms inefficient easy-to-understand expressions "specifications" into efficient involved expressions "programs" by algebraic manipulation. For example, the specification "" is an almost literal translation of the maximum segment sum problem /wiki/Maximum segment sum problem , 6 but running that functional program on a list of size will take time in general. From this, Bird computes an equivalent functional program that runs in time , and is in fact a functional version of Kadane's algorithm /wiki/Kadane%27s algorithm . The derivation is shown in the picture, with computational complexities 7 given in blue, and law applications indicated in red. 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: , , and correspond to , , and a generalized version of above, respectively, while and compute a list of all prefixes /wiki/Prefix computer science and suffixes /wiki/Suffix computer science of its arguments, respectively. As above, function composition is denoted by "", which has the lowest binding precedence /wiki/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 edit /w/index.php?title=Bird%E2%80%93Meertens formalism&action=edit§ion=2 A function h on lists is called a list homomorphism /wiki/Homomorphism if there exists an associative binary operator and neutral element such that the following holds: 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 /wiki/Parallel computing 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 /wiki/Map-reduce approach. See also edit /w/index.php?title=Bird%E2%80%93Meertens formalism&action=edit§ion=3 References edit /w/index.php?title=Bird%E2%80%93Meertens formalism&action=edit§ion=4 ^ cite ref-1 Ursula Martin /wiki/Ursula Martin ; Tobias Nipkow /wiki/Tobias Nipkow Apr 1990 . "Automating Squiggol" https://www21.in.tum.de/~nipkow/pubs/squiggol.html . In Manfred Broy /wiki/Manfred Broy ; Cliff B. Jones /wiki/Cliff Jones computer scientist eds. . Proc. . North-Holland. pp. 233–247. IFIP WG 2.2/2.3 /wiki/IFIP Working Group 2.3 Working Conference on Programming Concepts and Methods ^ cite ref-FOOTNOTEBird1989Sect.8, p.126r 2-0 Bird 1989 CITEREFBird1989 , Sect.8, p.126r.- ^ a b Bird 1989 CITEREFBird1989 , Sect.2, p.123l. ^ cite ref-FOOTNOTEBird1989Sect.7, Lem.1, p.125l 4-0 Bird 1989 CITEREFBird1989 , Sect.7, Lem.1, p.125l.- ^ a b Bird 1989 CITEREFBird1989 , Sect.5, p.124r. Where , , and returns the largest value, the sum, and the list of all segments i.e. sublists of a given list, respectively. ^ cite ref-6 Each expression in a line denotes an executable functional program to compute the maximum segment sum. ^ cite ref-7 Bibliography edit /w/index.php?title=Bird%E2%80%93Meertens formalism&action=edit§ion=5 Meertens, Lambert /wiki/Lambert Meertens 1986 . "Algorithmics: Towards programming as a mathematical activity" https://ir.cwi.nl/pub/2686 . In de Bakker, J.W.; Hazewinkel, M. /wiki/Michiel Hazewinkel ; Lenstra, J.K. eds. . Mathematics and Computer Science . CWI Monographs. Vol. 1. North-Holland. pp. 289–334. Meertens, Lambert /wiki/Lambert Meertens ; Bird, Richard /wiki/Richard Bird computer scientist 1987 . "Two Exercises Found in a Book on Algorithmics" https://www.kestrel.edu/people/meertens/publications/papers/Two exercises found in a book on Algorithmics.pdf PDF . North-Holland. Backhouse, Roland /wiki/Roland Carl Backhouse 1988 . PDF Technical report . An Exploration of the Bird-Meertens Formalism Bird, Richard S. /wiki/Richard Bird computer scientist 1989 . "Algebraic Identities for Program Calculation" https://academic.oup.com/comjnl/article-pdf/32/2/122/1445670/320122.pdf PDF . The Computer Journal . 32 2 : 122–126. doi /wiki/Doi identifier : 10.1093/comjnl/32.2.122 https://doi.org/10.1093%2Fcomjnl%2F32.2.122 .- Cole, Murray 1993 . "Parallel Programming, List Homomorphisms and the Maximum Segment Sum Problem" http://homepages.inf.ed.ac.uk/mic/Pubs/segmentsum.ps.gz . Parallel Computing: Trends and Applications, PARCO 1993, Grenoble, France . pp. 489–492. Backhouse, Roland /wiki/Roland Carl Backhouse ; Hoogendijk, Paul 1993 . PDF . pp. 7–42. Elements of a Relational Theory of Datatypes doi /wiki/Doi identifier : 10.1007/3-540-57499-9 15 https://doi.org/10.1007%2F3-540-57499-9 15 . ISBN /wiki/ISBN identifier 978-3-540-57499-6 /wiki/Special:BookSources/978-3-540-57499-6 .- Bunkenburg, Alexander 1994 . O'Donnell, John T.; Hammond, Kevin eds. . PDF . The Boom Hierarchy Functional Programming, Glasgow 1993: Proceedings of the 1993 Glasgow Workshop on Functional Programming, Ayr, Scotland, 5–7 July 1993 . London: Springer. pp. 1–8. doi /wiki/Doi identifier : 10.1007/978-1-4471-3236-3 1 https://doi.org/10.1007%2F978-1-4471-3236-3 1 . ISBN /wiki/ISBN identifier 978-1-4471-3236-3 /wiki/Special:BookSources/978-1-4471-3236-3 . Bird, Richard /wiki/Richard Bird computer scientist ; de Moor, Oege 1997 . Algebra of Programming . International Series in Computing Science. Vol. 100. Prentice Hall. ISBN /wiki/ISBN identifier 0-13-507245-X /wiki/Special:BookSources/0-13-507245-X . Gibbons, Jeremy /wiki/Jeremy Gibbons 2020 . Troy Astarte ed. . PDF . The School of Squiggol: A History of the Bird-Meertens Formalism Formal Methods Workshop on History of Formal Methods . LNCS. Vol. 12233. Springer. doi /wiki/Doi identifier : 10.1007/978-3-030-54997-8 2 https://doi.org/10.1007%2F978-3-030-54997-8 2 .