Formalismo de Bird-Meertens

Cálculo para derivar programas informáticos a partir de especificaciones mediante el proceso de razonamiento ecuacional

El formalismo 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 del IFIP .

En algunas publicaciones se hace referencia a él como BMF, como un guiño a la forma Backus–Naur . Jocosamente también se lo conoce como Squiggol , como un guiño a ALGOL , que también estaba en el ámbito de competencias del WG 2.1, y debido a los símbolos "ondulados" que utiliza. Un nombre de variante menos utilizado, pero en realidad el primero sugerido, es SQUIGOL . Martin y Nipkow proporcionaron soporte automatizado para las pruebas de desarrollo de Squiggol, utilizando el Larch Prover . ^[1]

Ejemplos básicos y notaciones

Map es una función de segundo orden bien 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}].}$

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

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

Usando esos dos operadores y los primitivos (como la suma usual) y (para la concatenación de listas), podemos expresar fácilmente la suma de todos los elementos de una lista y la función flatten, como y , en estilo sin puntos . Tenemos: ${\displaystyle +}$ ${\displaystyle +\!\!\!+}$ ${\displaystyle {\rm {sum}}=+/}$ ${\displaystyle {\rm {flatten}}=+\!\!\!+/}$

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

${\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}.}$

Derivación del algoritmo de Kadane ^[2]

De manera similar, al escribir para la composición funcional y para la conjunción , es fácil escribir una función que pruebe que todos los elementos de una lista satisfacen un predicado p , simplemente como : ${\displaystyle \cdot }$ ${\displaystyle \land }$ ${\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) transforma expresiones ineficientes y fáciles de entender ("especificaciones") en expresiones complejas y eficientes ("programas") mediante manipulación algebraica. Por ejemplo, la especificación " " es una traducción casi literal del problema de suma máxima de segmentos , ^[6] pero ejecutar ese programa funcional en una lista de tamaño llevará tiempo en general. A partir de esto, Bird calcula un programa funcional equivalente que se ejecuta en tiempo , y es de hecho una versión funcional del algoritmo de Kadane . ${\displaystyle \mathrm {max} \cdot \mathrm {map} \;\mathrm {sum} \cdot \mathrm {segs} }$ ${\displaystyle n}$ ${\displaystyle {\mathcal {O}}(n^{3})}$ ${\displaystyle {\mathcal {O}}(n)}$

La derivación se muestra en la imagen, con las complejidades computacionales ^[7] indicadas en azul y las aplicaciones de las leyes indicadas en rojo. Se pueden abrir instancias de ejemplo de las leyes haciendo clic en [mostrar] ; 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: , , y corresponden a , , y una versión generalizada de lo anterior, respectivamente, mientras que y calculan una lista de todos los prefijos y sufijos de sus argumentos, respectivamente. Como se indicó anteriormente, la composición de funciones se denota por " ", que tiene la precedencia de enlace más baja . En las instancias de ejemplo, las listas están coloreadas por profundidad de anidamiento; en algunos casos, se definen nuevas operaciones ad hoc (cuadros grises). ${\displaystyle \mathrm {map} }$ ${\displaystyle \mathrm {concat} }$ ${\displaystyle \mathrm {foldl} }$ ${\displaystyle *}$ ${\displaystyle \mathrm {flatten} }$ ${\displaystyle /}$ ${\displaystyle \mathrm {inits} }$ ${\displaystyle \mathrm {tails} }$ ${\displaystyle \cdot }$

El lema del homomorfismo y sus aplicaciones a implementaciones paralelas

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

${\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 sólo si existe un operador y una función f tales que . ${\displaystyle \oplus }$ ${\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 tiene una implementación altamente paralela, y lo hace también , más obviamente como un árbol binario. Por lo tanto, para cualquier homomorfismo de lista h , existe una implementación paralela. Esa implementación corta la lista en fragmentos, que se asignan a diferentes computadoras; cada una calcula el resultado en su propio fragmento. Son esos resultados los que transitan en la red y finalmente se combinan en uno. En cualquier aplicación donde la lista es enorme y el resultado es un tipo muy simple, digamos un entero, los beneficios de la paralelización son considerables. Esta es la base del enfoque map-reduce . ${\displaystyle f*}$ ${\displaystyle \oplus /}$

Véase también

• Catamorfismo
• Anamorfismo
• Paramorfismo
• Hilomorfismo

Referencias

1. Ursula Martin ; Tobias Nipkow (abril de 1990). "Automatización de Squiggol". En Manfred Broy ; Cliff B. Jones (eds.). Actas de la Conferencia de trabajo IFIP WG 2.2/2.3 sobre conceptos y métodos de programación . Holanda Septentrional. págs. 233–247.
2. Bird 1989, Secc.8, p.126r.
3. Bird 1989, Secc.2, p.123l.
4. Bird 1989, Sec.7, Lem.1, p.125l.
5. Bird 1989, Secc.5, p.124r.
6. Donde , , y devuelven el valor más grande, la suma y la lista de todos los segmentos (es decir, sublistas) de una lista dada, respectivamente. ${\displaystyle \mathrm {max} }$ ${\displaystyle \mathrm {sum} }$ ${\displaystyle \mathrm {segs} }$
7. Cada expresión en una línea denota un programa funcional ejecutable para calcular la suma máxima del segmento.

• Meertens, Lambert (1986). "Algoritmos: hacia la programación como actividad matemática". En de Bakker, JW; Hazewinkel, M.; Lenstra, JK (eds.). Matemáticas y Ciencias de la Computación . Monografías del CWI. Vol. 1. Holanda Septentrional. págs. 289–334.
• Meertens, Lambert ; Bird, Richard (1987). "Dos ejercicios encontrados en un libro sobre algoritmos" (PDF) . Holanda Septentrional.
• 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 . pp. 489–492.
• Backhouse, Roland ; Hoogendijk, Paul (1993). Elementos de una teoría relacional de 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) . Programación funcional, Glasgow 1993: Actas del Taller de Glasgow de 1993 sobre programación funcional, Ayr, Escocia, 5-7 de julio de 1993. Londres: Springer. págs. 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 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 del garabato: una historia del formalismo de Bird-Meertens (PDF) . Métodos formales (Taller sobre historia de los métodos formales) . LNCS. Vol. 12233. Springer. doi :10.1007/978-3-030-54997-8_2.