Formalizm Birda-Meertensa

Formalizm Birda-Meertensa ( BMF ) to rachunek do wyprowadzania programów ze specyfikacji (w ustawieniu programowania funkcyjnego ) w procesie wnioskowania równaniowego. Został opracowany przez Richarda Birda i Lamberta Meertensa w ramach ich pracy w ramach Grupy Roboczej IFIP 2.1 .

W publikacjach jest czasami określany jako BMF, jako ukłon w stronę formy Backusa – Naura . Żartobliwie jest również określany jako Squiggol , jako ukłon w stronę ALGOL , który również był w gestii WG 2.1, i ze względu na używane przez niego „faliste” symbole. Rzadziej używaną nazwą wariantu, ale tak naprawdę pierwszą sugerowaną, jest SQUIGOL .

Podstawowe przykłady i oznaczenia

Mapa jest dobrze znaną funkcją drugiego rzędu, która stosuje daną funkcję do każdego elementu listy; w BMF jest napisane ${\ displaystyle *}$ :

${\ Displaystyle f * [e_ {1}, \ kropki, e_ {n}] = [f \ e_ {1}, \ kropki, f \ e_ {n}].}$

Podobnie redukcja jest funkcją, która zwija listę do pojedynczej wartości przez wielokrotne zastosowanie operatora binarnego . Jest napisane / w BMF. Biorąc jako odpowiedni operator binarny z elementem neutralnym e , mamy ${\ displaystyle \ oplus}$

${\ Displaystyle \ oplus / [e_ {1}, \ kropki, e_ {n}] = e \ oplus e_ {1} \ oplus \ kropki \ oplus e_ {n}.}$

$)$ i prymitywów (jako zwykłego dodawania) i $( do łączenia$ możemy łatwo wyrazić sumę wszystkich elementów listy i funkcji spłaszczania, ponieważ ${\ Displaystyle {\ rm {sum}} = + /}$ i ${\ Displaystyle {\ rm {spłaszczyć }}=+\!\!\!+/}$ , w stylu bez punktów . Mamy:

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

${\ Displaystyle {\ rm {spłaszczyć}} \ [l_ {1}, \ kropki, l_ {n}] = + \! \! \! +/[l_ {1}, \ kropki, l_ {n}] = [\,]+\!\!\!+\;l_{1}+\!\!\!+\dots +\!\!\!+\;l_{n}={\text{ konkatenacja wszystkie listy }}l_{k}.}$

Wyprowadzenie algorytmu Kadane'a

Podobnie, pisząc $kompozycji$ funkcjonalnej i dla $koniunkcji , łatwo$${\ Displaystyle {\ rm {wszystko}} \ p = (\ ziemia /) \ cdot (p *)}$ wszystkie elementy listy spełniają predykat p , po prostu jako a :

${\ Displaystyle {\ rozpocząć {wyrównane} {\ rm {wszystkie}} \ p \ [e_ {1}, \ kropki, e_ {n}] & = (\ ziemia /) \ cdot (p *) \ [e_ { 1},\kropki ,e_{n}]\\&=\kraj /(p*[e_{1},\kropki ,e_{n}])\\&=\kraj /[p\ e_{1} ,\dots ,p\ e_{n}]\\&=p\ e_{1}\land \dots \land p\ e_{n}\\&=\forall k\ .\ p\ e_{k}. \end{wyrównane}}}$

Bird (1989) przekształca nieefektywne, łatwe do zrozumienia wyrażenia („specyfikacje”) w wydajne wyrażenia zaangażowane („programy”) za pomocą manipulacji algebraicznych. Na przykład specyfikacja " ${\ Displaystyle \ operatorname {max} \ cdot \ operatorname {mapa} \; \ operatorname {suma} \ cdot \ operatorname {seg$ "jest prawie dosłownym tłumaczeniem problemu maksymalnej sumy segmentów , ale uruchomienie tego programu funkcjonalnego na liście o rozmiarze $Displaystyle$ trochę czasu ${\ mathcal {O}} (n ^{3})}$ ogólnie. Na tej podstawie Bird $i$ równoważny program funkcjonalny, który działa w czasie jest rzeczywistości funkcjonalną wersją Kadane'a

Wyprowadzenie jest pokazane na rysunku, ze złożonością obliczeniową zaznaczoną na niebiesko i aplikacjami prawa zaznaczonymi na czerwono. Przykładowe przykłady praw można otworzyć, klikając [pokaż] ; używają list liczb całkowitych, dodawania, minus i mnożenia. Notacja $re$$artykule$ Birda $\ mathrm {foldl}}$ : odpowiadają odpowiednio ${\ Displaystyle *}$ , ${\ Displaystyle \ operatorname {spłaszczyć}}$ i uogólnionej wersji ${\ Displaystyle /}$ powyżej, podczas gdy ${\ displaystyle \ operatorname {inits}}$ i ${\ displaystyle \ operatorname {ogony}}$ obliczyć odpowiednio listę wszystkich przedrostków i sufiksów jego argumentów. Jak wyżej, skład funkcji jest oznaczony przez „ $,$ który ma najniższy priorytet wiązania . W przykładowych instancjach listy są kolorowane według głębokości zagnieżdżenia; w niektórych przypadkach nowe operacje są definiowane ad hoc (szare pola).

Lemat o homomorfizmie i jego zastosowania w implementacjach równoległych

Funkcja h na listach nazywana jest homomorfizmem listy , jeśli istnieje asocjacyjny operator binarny i element neutralny, $oplus}$ że zachodzi: $\$

${\ Displaystyle {\ rozpocząć {wyrównane} & h \ [\,] & & = \ e \\ & h \ (l + \! \! \! + \; m) & & = \ h \ l \ oplus h \ m. \ koniec {wyrównany}}}$

Lemat o homomorfizmie stwierdza, że ${\ Displaystyle h = (\ oplus / )\cdot (f*)}$ jest $homomorfizmem$ wtedy i tylko wtedy, gdy istnieje operator i funkcja f taka, że .

Bardzo interesującym punktem tego lematu jest jego zastosowanie do wyprowadzania wysoce równoległych implementacji obliczeń. $najwyraźniej$ łatwo jest zobaczyć, że $ma$ wysoce równoległą implementację, podobnie jak jako drzewo binarne Zatem dla każdego homomorfizmu listy 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 swoim własnym fragmencie. To właśnie te wyniki przechodzą przez sieć i ostatecznie są łączone w jeden. W każdej aplikacji, w której lista jest ogromna, a wynikiem jest bardzo prosty typ — powiedzmy liczba całkowita — korzyści z równoległości są znaczne. Jest to podstawa map-reduce .

Zobacz też

• katamorfizm
• Anamorfizm
• Paramorfizm
• Hylomorfizm

• Meertens, Lambert (1986). „Algorytmika: w kierunku programowania jako działalność matematyczna” . W JW de Bakker; M. Hazewinkel; JK Lenstra (red.). Matematyka i Informatyka . Monografie CWI. Tom. 1. Holandia Północna. s. 289–334.
• Meertens, Lambert ; Ptak, Richard (1987). „Dwa ćwiczenia znalezione w książce o algorytmach” (PDF) . Holandia Północna.
• Zaplecze, Roland (1988). Badanie formalizmu Birda-Meertensa (PDF) (raport techniczny).
• Ptak, Richard S. (1989). „Tożsamości algebraiczne do obliczania programu” (PDF) . Dziennik komputerowy . 32 (2): 122–126. doi : 10.1093/comjnl/32.2.122 .
• Cole, Murray (1993). „Programowanie równoległe, homomorfizmy list i problem maksymalnej sumy segmentów” . Obliczenia równoległe: trendy i zastosowania, PARCO 1993, Grenoble, Francja . s. 489–492.
•   Zaplecze, Roland ; Hoogendijk, Paweł (1993). Elementy relacyjnej teorii typów danych (PDF) . s. 7–42. doi : 10.1007/3-540-57499-9_15 . ISBN 978-3-540-57499-6 .
•   Bunkenburg, Aleksander (1994). Johna T. O'Donnella; Kevin Hammond (red.). Hierarchia boomu (PDF) . Programowanie funkcjonalne, Glasgow 1993: Proceedings of the 1993 Glasgow Workshop on Functional Programming, Ayr, Szkocja, 5–7 lipca 1993 . Londyn: Springer. s. 1–8. doi : 10.1007/978-1-4471-3236-3_1 . ISBN 978-1-4471-3236-3 .
•   Ptak, Ryszard ; de Moor, Oege (1997). Algebra Programowania . Międzynarodowa seria w informatyce. Tom. 100. Sala praktykantów. ISBN 0-13-507245-X .
• Gibbons, Jeremy (2020). Troy Astarte (red.). Szkoła Squiggola: historia formalizmu Bird-Meertens (PDF) . Metody formalne (Warsztaty z historii metod formalnych) . LNCS. Tom. 12233. Zygmunt. doi : 10.1007/978-3-030-54997-8_2 .