Formalismo de Bird-Meertens

El formalismo de Bird-Meertens ( BMF ) es un cálculo para derivar programas a partir de especificaciones de programas (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 en el Grupo de Trabajo 2.1 de la IFIP .

En ocasiones se la denomina en publicaciones como BMF, en alusión a la forma Backus-Naur . De forma jocosa, también se la conoce como Squiggol , en alusión a ALGOL , que también formaba parte del ámbito del WG 2.1, y debido a los símbolos "ondulados" que utiliza. Una variante menos común, pero que en realidad fue la primera que se sugirió, es SQUIGOL . Martin y Nipkow proporcionaron soporte automatizado para las pruebas de desarrollo de Squiggol, utilizando el Larch Prover . ^{[ 1 ]}

Map es una función de segundo orden muy conocida que aplica una función dada a cada elemento de una lista; en BMF, se escribe${\displaystyle *}$:

${\displaystyle f*[e_{1},\dots ,e_{n}]=[f\ e_{1},\dots ,f\ e_{n}].}$

Asimismo, reduce es una función que colapsa una lista en un solo valor mediante la aplicación repetida de un operador binario . Se escribe como${\displaystyle /}$en BMF. Tomando${\displaystyle \oplus }$como un operador binario adecuado con elemento neutro e , tenemos

${\displaystyle \oplus /[e_{1},\dots ,e_{n}]=e\oplus e_{1}\oplus \dots \oplus e_{n}.}$

Utilizando esos dos operadores y las primitivas${\displaystyle +}$(como adición habitual), y${\displaystyle +\!\!\!+}$(para la concatenación de listas), podemos expresar fácilmente la suma de todos los elementos de una lista, y la función de aplanamiento , como${\displaystyle {\rm {suma}}=+/}$y${\displaystyle {\rm {aplanar}}=+\!\!\!+/}$, en estilo sin puntos . Tenemos:

${\displaystyle {\rm {suma}}\ [e_{1},\dots ,e_{n}]=+/[e_{1},\dots ,e_{n}]=0+e_{1}+\dots +e_{n}=\sum _{k}e_{k}.}$

${\displaystyle {\rm {aplanar}}\ [l_{1},\dots ,l_{n}]=+\!\!\!+/[l_{1},\dots ,l_{n}]=[\,]+\!\!\!+\;l_{1}+\!\!\!+\dots +\!\!\!+\;l_{n}={\text{ la concatenación de todas las listas }}l_{k}.}$

De manera similar, escribir${\displaystyle \cdot }$para composición funcional y${\displaystyle \land }$Para la conjunción , es fácil escribir una función que compruebe que todos los elementos de una lista satisfacen un predicado p , simplemente como${\displaystyle {\rm {todos}}\ p=(\land /)\cdot (p*)}$:

${\displaystyle {\begin{aligned}{\rm {todos}}\ 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) transforma expresiones ineficientes y fáciles de entender ("especificaciones") en expresiones eficientes y complejas ("programas") mediante manipulación algebraica. Por ejemplo, la especificación "${\displaystyle \mathrm {max} \cdot \mathrm {mapa} \;\mathrm {suma} \cdot \mathrm {segs} }$" es una traducción casi literal del problema de la suma máxima de segmentos , ^{[ 6 ]} pero ejecutando ese programa funcional en una lista de tamaño${\displaystyle n}$llevará tiempo${\displaystyle {\mathcal {O}}(n^{3})}$en general. A partir de esto, Bird calcula un programa funcional equivalente que se ejecuta en tiempo${\displaystyle {\mathcal {O}}(n)}$y, de hecho, es una versión funcional del algoritmo de Kadane .

La derivación se muestra en la imagen, con las complejidades computacionales ^{[ 7 ]} indicadas en azul y las aplicaciones de las leyes en rojo. Se pueden abrir ejemplos de las leyes haciendo clic en [mostrar] ; estos ejemplos utilizan listas de números enteros, suma, resta y multiplicación. La notación en el artículo de Bird difiere de la utilizada anteriormente:${\displaystyle \mathrm {mapa} }$,${\displaystyle \mathrm {concat} }$, y${\displaystyle \mathrm {foldl} }$corresponder a${\displaystyle *}$,${\displaystyle \mathrm {aplanar} }$y una versión generalizada de${\displaystyle /}$arriba, respectivamente, mientras que${\displaystyle \mathrm {inits} }$y${\displaystyle \mathrm {colas} }$Calcula una lista de todos los prefijos y sufijos de sus argumentos, respectivamente. Como se indicó anteriormente, la composición de funciones se denota por "${\displaystyle \cdot }$", que tiene la precedencia de enlace más baja . En los ejemplos, las listas están coloreadas según la profundidad de anidamiento; en algunos casos, se definen nuevas operaciones ad hoc (cuadros grises).

Una función h sobre listas se denomina homomorfismo de listas si existe un operador binario asociativo.${\displaystyle \oplus }$y elemento neutro ${\displaystyle e}$de tal manera que se cumple lo siguiente:

${\displaystyle {\begin{aligned}&h\ [\,]&&=\ e\\&h\ (l+\!\!\!+\;m)&&=\ h\ l\oplus h\ m.\end{aligned}}}$

El lema del homomorfismo establece que h es un homomorfismo si y solo si existe un operador${\displaystyle \oplus }$y una función f tal que${\displaystyle h=(\oplus /)\cdot (f*)}$.

Un punto de gran interés para este lema es su aplicación a la derivación de implementaciones altamente paralelas de cálculos. De hecho, es trivial ver que${\displaystyle f*}$tiene una implementación altamente paralela, y también${\displaystyle \oplus /}$— lo más evidente es que se trata de un árbol binario. Por lo tanto, para cualquier homomorfismo de listas h , existe una implementación paralela. Dicha implementación divide la lista en fragmentos, que se asignan a diferentes ordenadores; cada uno calcula el resultado en su propio fragmento. Son esos resultados los que se transmiten por la red y finalmente se combinan en uno solo. En cualquier aplicación donde la lista sea enorme y el resultado sea de un tipo muy simple —por ejemplo, un número entero—, las ventajas de la paralelización son considerables. Esta es la base del enfoque MapReduce .

• Catamorfismo
• Anamorfismo
• Paramorfismo
• Hilomorfismo

• Meertens, Lambert (1986). «Algoritmos: Hacia la programación como actividad matemática» . En de Bakker, JW; Hazewinkel, M .; Lenstra, JK (eds.). Matemáticas e Informática . Monografías del CWI. Vol.  1. North-Holland. pp. 289–334 . 
• Meertens, Lambert ; Bird, Richard (1987). "Dos ejercicios encontrados en un libro sobre algoritmia" (PDF) . North-Holland.
• Backhouse, Roland (1988). Una exploración del formalismo de Bird-Meertens (PDF) (Informe técnico).
• Bird, Richard S. (1989). "Identidades algebraicas para el cálculo de programas" (PDF) . The Computer Journal . 32 (2): 122– 126. doi : 10.1093/comjnl/32.2.122 .
• Cole, Murray (1993). "Programación paralela, homomorfismos de listas y el problema de la suma máxima de segmentos" . Computación paralela: tendencias y aplicaciones, PARCO 1993, Grenoble, Francia . págs. 489–492 . 
• Backhouse, Roland ; Hoogendijk, Paul (1993). Elementos de una teoría relacional de los tipos de datos (PDF) . págs. 7–42 . doi : 10.1007/3-540-57499-9_15 . ISBN  978-3-540-57499-6.
• Bunkenburg, Alexander (1994). O'Donnell, John T.; Hammond, Kevin (eds.). The Boom Hierarchy (PDF) . Functional Programming, Glasgow 1993: Proceedings of the 1993 Glasgow Workshop on Functional Programming, Ayr, Scotland, 5–7 July 1993. Londres: Springer. pp. 1–8 . doi : 10.1007/978-1-4471-3236-3_1 . ISBN  978-1-4471-3236-3.
• Bird, Richard ; de Moor, Oege (1997). Álgebra de la programación . Serie internacional en ciencias de la computación. Vol.  100. Prentice Hall. ISBN 0-13-507245-X.
• Gibbons, Jeremy (2020). Troy Astarte (ed.). La escuela de Squiggol: una historia del formalismo de Bird-Meertens (PDF) . Métodos formales (Taller sobre la historia de los métodos formales) . LNCS. Vol.  12233. Springer. doi : 10.1007/978-3-030-54997-8_2 .