Formalizm Bird – Meertens - Bird–Meertens formalism
Bird-Meertens formalizm ( BMF ) jest rachunek za wynikające programy z przeznaczeniem (w funkcjonalnych programowania ustawienia) w procesie equational rozumowania. Został on opracowany przez Richarda Birda i Lamberta Meertensa w ramach ich pracy w grupie roboczej IFIP 2.1 .
Czasami w publikacjach nazywany jest BMF, jako ukłon w stronę formy Backusa – Naura . Mówiąc frazesowo, jest również określany jako Squiggol , jako ukłon w stronę ALGOL , który był również w gestii WG 2.1, i ze względu na używane przez niego „zawijane” symbole. Rzadziej używana nazwa wariantu, ale tak naprawdę pierwsza sugerowana, to SQUIGOL .
Podstawowe przykłady i zapisy
Mapa to dobrze znana funkcja drugiego rzędu, która stosuje daną funkcję do każdego elementu listy; w BMF jest napisane :
Podobnie, redukuj jest funkcją, która zwija listę do pojedynczej wartości przez wielokrotne zastosowanie operatora binarnego . Jest napisane / w BMF. Przyjmując jako odpowiedni operator binarny z neutralnym elementem e , mamy
Używając tych dwóch operatorów i prymitywów (jak zwykle dodawanie) i (do konkatenacji list), możemy łatwo wyrazić sumę wszystkich elementów listy i funkcji spłaszczenia , as i , w stylu bez punktów . Mamy:
Podobnie, pisząc dla kompozycji funkcjonalnej i dla koniunkcji , łatwo jest napisać funkcję sprawdzającą, czy wszystkie elementy listy spełniają predykat p , po prostu jako :
Bird (1989) przekształca nieefektywne, łatwe do zrozumienia wyrażenia („specyfikacje”) w efektywne wyrażenia zaangażowane („programy”) za pomocą manipulacji algebraicznych. Na przykład specyfikacja „ ” jest prawie dosłownym tłumaczeniem „algorytmu maksymalnej sumy segmentów”, ale uruchomienie tego programu funkcjonalnego na liście rozmiarów zajmie na ogół trochę czasu . Na tej podstawie Bird oblicza równoważny program funkcjonalny, który działa w czasie i jest w rzeczywistości funkcjonalną wersją algorytmu Kadane'a .
Wyprowadzenie pokazano na rysunku, złożoność obliczeń zaznaczono na niebiesko, a zastosowania prawa zaznaczono na czerwono. Przykładowe przykłady przepisów można otworzyć, klikając [pokaż] ; używają list liczb całkowitych, dodawania, minusów i mnożenia. Zapis w ptaka różni się od stosowanego papieru powyżej: , i odpowiadają , oraz uogólnione wersja powyżej, odpowiednio, podczas gdy i obliczyć listę wszystkich przedrostków i przyrostków swoich argumentów, odpowiednio. Jak powyżej, kompozycja funkcji jest oznaczona przez „ ”, co ma najniższy priorytet wiązania . W przykładowych przypadkach listy są kolorowane według głębokości zagnieżdżenia; w niektórych przypadkach nowe operacje są definiowane ad hoc (szare pola).
Lemat homomorfizmu i jego zastosowania w implementacjach równoległych
Funkcja h na listach nazywa się homomorfizmem listy, jeśli istnieje asocjacyjny operator binarny i element neutralny, tak że zachodzi:
Homomorfizm lemat stwierdzono, że H jest homomorfizmem wtedy i tylko wtedy, gdy istnieje operatora oraz funkcja f , tak że .
Bardzo interesującym punktem tego lematu jest jego zastosowanie do wyprowadzania wysoce równoległych implementacji obliczeń. Rzeczywiście, trywialne jest zobaczenie, że ma wysoce równoległą implementację, podobnie jak - najbardziej oczywiste jako drzewo binarne. Zatem dla dowolnej listy homomorfizmu h istnieje równoległa implementacja. Ta implementacja dzieli listę na części, które są przypisane do różnych komputerów; każdy oblicza wynik na swojej własnej porcji. To właśnie te wyniki przechodzą przez sieć i ostatecznie łączą się w jeden. W każdej aplikacji, w której lista jest ogromna, a wynik jest bardzo prostym typem - powiedzmy liczbą całkowitą - korzyści z równoległości są znaczne. To jest podstawa podejścia polegającego na ograniczaniu mapy .
Zobacz też
Bibliografia
- Lambert Meertens (1986). „Algorytmika: w kierunku programowania jako czynności matematycznej”. . W JW de Bakker; M. Hazewinkel; JK Lenstra (red.). Matematyka i informatyka, monografie CWI, tom 1 . Holandia Północna. pp. 289–334.
- Lambert Meertens ; Richard Bird (1987). „Dwa ćwiczenia znalezione w książce o algorytmice” (PDF) . Holandia Północna.
- Richard S. Bird (1989). „Tożsamości algebraiczne do obliczania programów” . Dziennik komputerowy . 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, tom. 100 . Prentice Hall. ISBN 0-13-507245-X .
- Cole, Murray (1993). „Programowanie równoległe, homomorfizmy listowe i problem maksymalnej sumy segmentów” . Obliczenia równoległe: trendy i zastosowania, PARCO 1993, Grenoble, Francja . pp. 489–492.