Formalismo de Bird-Meertens
El formalismo de Bird-Meertens ( BMF ) es un cálculo para derivar programas a partir de especificaciones (en un entorno de programación funcional ) mediante un proceso de razonamiento ecuacional. Fue ideado por Richard Bird y Lambert Meertens como parte de su trabajo dentro del Grupo de Trabajo 2.1 de IFIP .
A veces se hace referencia en las publicaciones como BMF, como un guiño a la forma Backus-Naur . En broma, también se le conoce como Squiggol , como un guiño a ALGOL , que también estaba en el ámbito de WG 2.1, y debido a los símbolos "garabatos" que utiliza. Una variante de nombre menos utilizada, pero en realidad la primera sugerida, es SQUIGOL .
Map es una función de segundo orden bien conocida que aplica una función dada a cada elemento de una lista; en BMF, está escrito :
Asimismo, reduce es una función que colapsa una lista en un solo valor mediante la aplicación repetida de un operador binario . Está escrito / en BMF. Tomando como operador binario adecuado con elemento neutro e , tenemos
Usando esos dos operadores y las primitivas (como la suma habitual) y (para la concatenación de listas), podemos expresar fácilmente la suma de todos los elementos de una lista y la función aplanar , como y , en estilo sin puntos . Tenemos:
De manera similar, escribiendo para composición funcional y para conjunción , es fácil escribir una función que pruebe que todos los elementos de una lista satisfacen un predicado p , simplemente como :
