El formalismo 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 del IFIP .
A veces se lo conoce en las publicaciones como BMF, como un guiño a la forma Backus-Naur . En broma, también se lo 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 "ondulados" que utiliza. Un nombre de variante menos utilizado, pero en realidad el primero sugerido, es SQUIGOL .
Ejemplos básicos y notaciones
Map es una función de segundo orden conocida que aplica una función determinada a cada elemento de una lista; en BMF, está escrito:
Asimismo, reducir es una función que contrae una lista en un solo valor mediante la aplicación repetida de un operador binario . Está escrito / en BMF. Tomandocomo un operador binario adecuado con el elemento neutro e , tenemos
Usando esos dos operadores y las primitivas (como la adición 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:
Del mismo modo, escribir para la composición funcional ypara conjunción , es fácil escribir una función que pruebe que todos los elementos de una lista satisfacen un predicado p , simplemente como:
Bird (1989) transforma expresiones ineficientes y fáciles de entender ("especificaciones") en expresiones implicadas eficientes ("programas") mediante manipulación algebraica. Por ejemplo, la especificación ""es una traducción casi literal de" algoritmo de suma máxima de segmentos ", [5] pero ejecutar ese programa funcional en una lista de tamaños tomará tiempo en general. A partir de esto, Bird calcula un programa funcional equivalente que se ejecuta en el tiempo, y de hecho es una versión funcional del algoritmo de Kadane .
La derivación se muestra en la imagen, con las complejidades computacionales [6] indicadas en azul y las aplicaciones de leyes indicadas en rojo. Se pueden abrir ejemplos de las leyes haciendo clic en [mostrar] ; utilizan listas de números enteros, suma, menos y multiplicación. La notación en el artículo de Bird difiere de la utilizada anteriormente:, , y corresponden a las , , y una versión generalizada de arriba, respectivamente, mientras y calcular una lista de todos los prefijos y sufijos de sus argumentos, respectivamente. Como anteriormente, la composición de funciones se denota por "", que tiene la precedencia de encuadernación más baja . En los casos de ejemplo, las listas se colorean según la profundidad de anidación; en algunos casos, las nuevas operaciones se definen ad hoc (casillas grises).
El lema del homomorfismo y sus aplicaciones a implementaciones paralelas
Una función h en listas se llama homomorfismo de lista si existe un operador binario asociativo y elemento neutro de modo que se mantenga lo siguiente:
El lema del homomorfismo establece que h es un homomorfismo si y solo si existe un operadory una función f tal que.
Un punto de gran interés para este lema es su aplicación a la derivación de implementaciones de cálculos altamente paralelas . De hecho, es trivial ver que tiene una implementación muy paralela, al igual que - más obviamente como un árbol binario. Por tanto, para cualquier homomorfismo de lista h , existe una implementación paralela. Esa implementación corta la lista en trozos, que se asignan a diferentes computadoras; cada uno calcula el resultado en su propio fragmento. Son esos resultados los que transitan por 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 número entero, los beneficios de la paralelización son considerables. Ésta es la base del enfoque de reducción de mapas .
Ver también
Referencias
- ^ Bird 1989 , sección 8, p.126r.
- ↑ a b Bird , 1989 , Sección 2, p.123l.
- ↑ Bird 1989 , Sect.7, Lem.1, p.125l.
- ↑ a b Bird , 1989 , Sect.5, p.124r.
- ^ Donde, , y devuelve el valor más grande, la suma y la lista de todos los segmentos (es decir, sublistas) de una lista determinada.
- ^ Cada expresión en una línea denota un programa funcional ejecutable para calcular la suma máxima de segmentos.
- Lambert Meertens (1986). "Algoritmos: Hacia la programación como actividad matemática". . En JW de Bakker; M. Hazewinkel; JK Lenstra (eds.). Matemáticas e Informática, Monografías del CWI Volumen 1 . Holanda Septentrional. págs. 289–334.
- Lambert Meertens ; Richard Bird (1987). "Dos ejercicios encontrados en un libro sobre algoritmos" (PDF) . Holanda Septentrional.
- Richard S. Bird (1989). "Identidades algebraicas para el cálculo de programas" . The Computer Journal . 32 (2): 122-126. doi : 10.1093 / comjnl / 32.2.122 .
- Richard Bird ; Oege de Moor (1997). Álgebra de programación, Serie internacional de ciencias de la computación, vol. 100 . Prentice Hall. ISBN 0-13-507245-X.
- Cole, Murray (1993). "Programación en paralelo, lista de homomorfismos y el problema de la suma máxima del segmento" . Computación paralela: tendencias y aplicaciones, PARCO 1993, Grenoble, Francia . págs. 489–492.