To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

Bird–Meertens formalism

From Wikipedia, the free encyclopedia

The Bird–Meertens formalism (BMF) 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 a given function 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 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 function, as and , in point-free style. We have:

Derivation of Kadane's algorithm[1]   Example instances of used laws    Map promotion law[2]    Fold promotion law[2]    Generalized Horner's rule[3]    Scan lemma[4]    Fold-scan fusion law[4]
Derivation of Kadane's algorithm[1]

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 :

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 "maximum segment sum algorithm",[5] 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.

The derivation is shown in the picture, with computational complexities[6] 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 and suffixes of its arguments, respectively. As above, function composition is denoted by "", which has 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 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 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

  1. ^ Bird 1989, Sect.8, p.126r.
  2. ^ a b Bird 1989, Sect.2, p.123l.
  3. ^ Bird 1989, Sect.7, Lem.1, p.125l.
  4. ^ a b Bird 1989, Sect.5, p.124r.
  5. ^ Where , , and returns the largest value, the sum, and the list of all segments (i.e. sublists) of a given list.
  6. ^ Each expression in a line denotes an executable functional program to compute the maximum segment sum.
  • Lambert Meertens (1986). "Algorithmics: Towards programming as a mathematical activity.". In J.W. de Bakker; M. Hazewinkel; J.K. Lenstra (eds.). 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 S. Bird (1989). "Algebraic Identities for Program Calculation". The Computer Journal. 32 (2): 122–126. doi:10.1093/comjnl/32.2.122.
  • Richard Bird; Oege de Moor (1997). Algebra of Programming, International Series in Computing Science, Vol. 100. Prentice Hall. ISBN 0-13-507245-X.
This page was last edited on 7 May 2021, at 18:10
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.