Co nowego w czysto funkcjonalnych strukturach danych od czasu Okasaki?

Od czasu książki Chrisa Okasakiego z 1998 r. „Czysto funkcjonalne struktury danych”, nie widziałem zbyt wielu nowych ekscytujących czysto funkcjonalnych struktur danych; Mogę wymienić tylko kilka:

• IntMap (również wynaleziony przez Okasaki w 1998 r., Ale nieobecny w tej książce)
• Drzewa palcowe (i ich uogólnienie na monoidy)

Istnieje również kilka interesujących sposobów wdrażania już znanych struktur danych, takich jak użycie „typów zagnieżdżonych” lub „uogólnionych typów danych algebraicznych” w celu zapewnienia niezmienników drzewa.

Jakie inne nowe pomysły pojawiły się w tej dziedzinie od 1998 roku?

Nowe czysto funkcjonalne struktury danych publikowane od 1998 r .:

• 2001: Ideal Hash Trees i jego poprzednik z 2000 roku, szybkie i oszczędne wyszukiwanie Trie , autor: Phil Bagwell : Najwyraźniej używany jako podstawowy element składowy standardowej biblioteki Clojure.

• 2001: Prosta technika implementacji dla priorytetowych kolejek wyszukiwania autorstwa Ralfa Hinze : naprawdę prosta i piękna technika implementacji tej ważnej struktury danych (przydatna, powiedzmy, w algorytmie Dijkstry). Implementacja jest szczególnie piękna i czytelna ze względu na intensywne stosowanie „wzorców widoków”.

• 2002: Bootstrapping jednostronne elastyczne tablice , autor: Ralf Hinze : Podobne do list o swobodnym dostępie Okasaki, ale można je dostroić, aby zmienić kompromis czasowy consi indeksowanie.

• 2003: Nowe dające się dogadać i nie dające się dogadać , autorstwa Radu Mihaescu i Roberta Tarjana : Nowe spojrzenie na niektóre starsze prace (autorstwa Kaplana i Tarjana), które przytacza Okasaki ( Najnowsza wersja pracy Kaplana i Tarjana została opublikowana w 2000 r .). Ta wersja jest pod pewnymi względami prostsza.

• 2005: Kupy Maxiphobic ( papier i kod ), Chris Okasaki : Przedstawiony nie jako nowa, bardziej wydajna struktura, ale jako sposób na nauczenie kolejek priorytetowych.

• 2006: Gerth Stølting Brodal, Christos Makris i Kostas Tsichlas : Czyste, funkcjonalne, najgorsze przypadki w stałych przypadkach z sortowanymi listami : Odpowiedzi na wybitne pytanie Kaplana i Tarjana poprzez wykazanie struktury z wstawianiem, wyszukiwaniem, usuwaniem i usuwaniem O (lg n) (1) concat.

• 2008: Erik D. Demaine, Stefan Langerman i Eric Price : Konsekwentnie trwałe próby skutecznej kontroli wersji Przedstawia kilka struktur danych dla prób, które mają wydajną nawigację i modyfikację w pobliżu liści. Niektóre są wyłącznie funkcjonalne. Inne faktycznie poprawiają długoletnią strukturę danych przez Dietz i in. dla w pełni trwałych (ale nie konfluentnie trwałych lub czysto funkcjonalnych) tablic. W tym artykule zaprezentowano również czysto funkcjonalne drzewa cięte linkami , czasami nazywane „drzewami dynamicznymi”.

• 2010: Nowy czysto funkcjonalny algorytm usuwania drzew czerwono-czarnych , autor: Matt Might : Podobnie jak algorytm wstawiania drzew czerwono-czarnych Okasaki, nie jest to nowa struktura danych ani nowa operacja na strukturze danych, ale nowy, prostszy sposób napisz znaną operację.

• 2012: RRB-Trees: Efficient Immutable Vector, Phil Bagwell i Tiark Rompf : Rozszerzenie do Hash Array Mapped Tries, obsługujące niezmienne konkatenacje wektora, wstawianie i podział w czasie O (lg n), przy zachowaniu indeksu, aktualizacji oraz prędkości wstawiania oryginalnego niezmiennego wektora.

Znany w 1997 roku, ale nie omawiany w książce Okasaki:

• Wiele innych stylów zrównoważonego drzewa wyszukiwania . AVL, brat, zrównoważony według rang, zrównoważony i wiele innych zrównoważonych drzew wyszukiwania można (i zaimplementowano) wyłącznie funkcjonalnie poprzez kopiowanie ścieżek. Być może na szczególną uwagę zasługują:

  • Biased Search Trees , autor: Samuel W. Bent, Daniel D. Sleator i Robert E. Tarjan : Kluczowy element w pracy Brodal i wsp. Z 2006 r. Oraz w pracy Demaine i wsp. Z 2008 r.

• Zestawy nieskończone, które pozwalają na szybkie wyczerpujące wyszukiwanie , Martín Escardó : Być może nie jest to struktura danych per se .

• Trzy algorytmy na drzewach Braun , Chris Okasaki : Drzewa Braun oferują wiele operacji na stosie w najgorszym przypadku O (lg n). Ta granica jest przekraczana przez wiele innych struktur danych, ale drzewa Braun mająconsoperację leniwą w drugim argumencie, a więc mogą być używane jako nieskończone stosy w pewien sposób, którego inne struktury nie mogą.

• Rozluźniona sterta min-max: łącząca podwójna kolejka priorytetowa i sterta KD: wydajna wielowymiarowa kolejka priorytetowa , autor: Yuzheng Ding i Mark Allen Weiss : Są to wyłącznie czynności funkcjonalne, choć nie zostało to omówione w dokumentach . Nie sądzę, aby osiągnięte limity czasowe były lepsze niż te, które można osiągnąć za pomocą drzewek palców (Hinze & Paterson lub Kaplan i Tarjan) jako priorytetowych k-wymiarowych kolejek, ale myślę, że struktury Ding & Weiss zajmują mniej miejsca .

• Zipper , Gérard Huet : Używany w wielu innych strukturach danych (takich jak drzewa palców Hinze & Paterson), jest to sposób na odwrócenie struktury danych na lewą stronę.

• Listy różnic są listami bazowymi O (1) z transformacją O (n) do zwykłych conslist. Najwyraźniej byli znani od starożytności w społeczności Prologów, gdzie dokonali transformacji O (1) do zwykłych conslist. Transformacja O (1) wydaje się niemożliwa w tradycyjnym programowaniu funkcjonalnym, ale abstrakcja dziury Minidama z POPL '98 omawia sposób pozwalający na dołączenie O (1) i transformację O (1) w ramach czystego programowania funkcjonalnego. W przeciwieństwie do zwykłych implementacji programowania funkcjonalnego list różnic, które są oparte na zamknięciach funkcji, abstrakcje dziur są zasadniczo takie same (zarówno w ich użyciu, jak i implementacji) jak listy różnic Prolog. Wydaje się jednak, że przez lata jedyną osobą, która to zauważyłajeden z recenzentów Minamid .

• $O(\sqrt{n})$$\Theta(n \lg n)$$\Theta(\sqrt{n \lg n})$$\Theta(\lg^2 n)$

Przeważnie funkcjonalne struktury danych przed, w trakcie i po książce Okasaki:

• $O(m)$$m$$O(\lg \lg n)$

• 1989: Randomizowane drzewa wyszukiwania Cecilia R. Aragon i Raimund Seidel : Zostały one omówione w czysto funkcjonalnym otoczeniu przez Guya E. Blellocha i Margaret Reid-Miller w Szybkich operacjach z użyciem pułapek oraz Dan Blandford i Guy Blelloch w Operacjach zestawu funkcjonalnego z Treaps ( kod). Zapewniają wszystkie operacje czysto funkcjonalnych palców dotykowych i stronnicze drzewa wyszukiwania, ale wymagają źródła losowości, co czyni je nie tylko funkcjonalnymi. Może to również unieważnić złożoność czasową operacji na pułapkach, zakładając, że przeciwnik może mierzyć operacje i powtarzać długie. (To jest ten sam powód, dla którego argumenty o bezwzględnej amortyzacji nie są ważne w ustawieniach trwałych, ale wymaga to przeciwnika ze stoperem)

• 1997: Skip-trees, alternatywna struktura danych do Skip-listów w podejściu równoległym , autorstwa Xaviera Messeguera i Exploring the Duality Between Skip Lists and Binary Search Trees , Brian C. Dean i Zachary H. Jones : Listy pominięć nie są czysto funkcjonalne, ale można je funkcjonalnie implementować jako drzewa. Podobnie jak pułapki, wymagają źródła losowych bitów. (Możliwe jest, aby listy pominięć były deterministyczne, ale po przetłumaczeniu ich na drzewo, myślę, że są one po prostu innym sposobem patrzenia na 2-3 drzewa.)

• 1998: Wszystkie zamortyzowane struktury w książce Okasaki! Okasaki wynalazł tę nową metodę mieszania amortyzacji i funkcjonalnych struktur danych, które wcześniej uważano za niezgodne. Zależy to od zapamiętywania, które, jak czasem wspominają Kaplan i Tarjan, jest w rzeczywistości efektem ubocznym. W niektórych przypadkach ( takich jak PFDS na dyskach SSD ze względu na wydajność ) może to być nieodpowiednie.

• 1998: Simple Confluently Persistent Catenable Lists , autorstwa Haima Kaplana, Chrisa Okasakiego i Roberta E. Tarjana : Używa modyfikacji pod maską, aby uzyskać zamortyzowany dezaktywowany O (1), prezentując ten sam interfejs co wcześniej (czysto funkcjonalny, ale z zapamiętywaniem ) wersja pojawiająca się w książce Okasaki. Kaplan i Tarjan wcześniej stworzyli czysto funkcjonalną strukturę O (1) najgorszego przypadku, ale jest ona znacznie bardziej skomplikowana.

• 2007: Jak wspomniano w innej odpowiedzi na tej stronie, półtrwałe struktury danych i trwałe połączenie przez Sylvaina Conchon i Jean-Christophe Filliâtre

Techniki weryfikacji funkcjonalnych struktur danych przed, w trakcie i po książce Okasaki:

• Typy fantomów to stara metoda tworzenia interfejsu API, który nie pozwala na pewne źle sformułowane operacje. Ich zaawansowane zastosowanie można znaleźć w Lekkich zdolnościach statycznych Olega Kiselyova i Chung-chieha Shana .

• Zagnieżdżone typy nie są tak naprawdę nowsze niż 1998 - Okasaki używa ich nawet w swojej książce. Istnieje wiele innych przykładów, których nie ma w książce Okasaki; niektóre są nowe, a niektóre stare. Zawierają:

  • Czerwono-czarne drzewa Stefana Kahrsa z typami ( kod )
  • Drzewa AVL Rossa Patersona ( lustro )
  • Chris Okasaki's Od szybkiego potęgowania do macierzy kwadratowych: przygoda typowa
  • Notacja de Bruijna Richarda S. Birda i Rossa Petersona jako zagnieżdżony typ danych
  • Reprezentacje liczbowe Ralfa Hinze jako zagnieżdżone typy danych wyższego rzędu .

• GADT też nie są takie nowe. Są najnowszym dodatkiem do Haskell i niektórych ML, ale myślę, że są obecne, jak sądzę, w różnych typach lambda od 1970 roku .

• 2004-2010: Coq i Isabelle za poprawność . Kilka osób wykorzystało dowody twierdzeń do zweryfikowania poprawności czysto funkcjonalnych struktur danych. Coq może wyodrębnić te weryfikacje do działającego kodu w Haskell, OCaml i Scheme; Isabelle może ekstrahować do Haskell, ML i OCaml.

  • Coq:
    • Pierre Letouzey i Jean-Christophe Filliâtre sformalizowali drzewa czerwono-czarne i AVL (ish), znajdując w tym czasie błąd w standardowej bibliotece OCaml .
    • I sformalizowane Brodal and Okasaki jest asymptotycznie optymalne kolejki priorytetowe .
    • Arthur Charguéraud sformalizował 825 z 1700 linii ML w książce Okasaki .
  • Isabelle:
    • Tobias Nipkow i Cornelia Pusch sformalizowali drzewa AVL .
    • Viktor Kuncak sformalizował niezrównoważone drzewa wyszukiwania binarnego .
    • Peter Lammich opublikował platformę Isabelle Kolekcje , która obejmuje formalizowanie wydajnych czysto funkcjonalnych struktur danych, takich jak czerwono-czarne drzewa i próby, a także struktur danych, które są mniej wydajne, gdy są używane w sposób ciągły, takich jak kolejki z dwoma stosami (bez sztuczki lenistwa Okasaki ) i tabele skrótów.
    • Peter Lammich opublikował także formalizacje automatów drzew , palców Hinze & Patterson (z Benediktem Nordhoffem i Stefanem Körnerem) oraz czysto funkcjonalne kolejki priorytetowe Brodala i Okasaki (z Rene Meis i Finnem Nielsenem).
    • René Neumann sformalizował dwumianowe kolejki priorytetowe .

• 2007: Ulepszone sprawdzanie typów za pomocą Stardust , autor: Joshua Dunfield : W tym artykule wykorzystano typy udoskonalenia ML, aby znaleźć błędy w funkcji usuwania drzewa czerwono-czarnego SMLNJ.

• 2008: Nils Anders Danielsson : lekka analiza złożoności czasu półformalnego dla czysto funkcjonalnych struktur danych : Wykorzystuje Agdę z ręcznymi adnotacjami do udowodnienia ograniczeń czasowych dla niektórych PFDS.

Imperatywne struktury danych lub analizy nie omówione w książce Okasaki, ale związane z czysto funkcjonalnymi strukturami danych:

• Miękkie sterty: przybliżona kolejka priorytetowa z optymalnym współczynnikiem błędów , autor: Bernard Chazelle : Ta struktura danych nie korzysta z tablic, dlatego też kusiło najpierw kanał IRC #haskell, a później użytkowników przepełnienia stosu , ale zawiera ondeleteo (lg n) , co zwykle nie jest możliwe w otoczeniu funkcjonalnym, oraz analiza bezwzględnie zamortyzowana, która nie jest ważna w otoczeniu czysto funkcjonalnym.

• Zrównoważone drzewa wyszukiwania binarnego z aktualizacjami palca O (1) . W tworzeniu trwałych struktur danych James R Driscoll, Neil Sarnak, Daniel D. Sleator i Robert E. Tarjan przedstawiają metodę grupowania węzłów w czerwono-czarnym drzewie, aby trwałe aktualizacje wymagały tylko miejsca O (1). Czysto funkcjonalne deques i drzewa palców zaprojektowane przez Tarjana, Kaplana i Mihaescu używają bardzo podobnej techniki grupowania, aby umożliwić aktualizacje O (1) na obu końcach. Drzewa AVL do wyszukiwania lokalnego przez Athanasios K. Tsakalidis działają podobnie.

• Szybsze stosy parowania lub lepsze granice dla parowania : Od czasu opublikowania książki Okasaki pojawiło się kilka nowych analiz imperatywnych stosów parowania, w tym Kupy parowania z O (log log n) zmniejszają Koszt według Amr Elmasry i W kierunku ostatecznej analizy stosów parowania o Seth Pettie. Niektóre z tych prac można zastosować do leniwych stosów parowania Okasaki.

• Deterministyczne tendencyjne drzewa palców : W Biased Skip Lists autorstwa Amitabha Bagchi, Adama L. Buchsbauma i Michaela T. Goodricha przedstawiono projekt deterministycznych tendencyjnych list pomijanych. Za pomocą wspomnianej wyżej listy pomijania / transformacji drzewa może być możliwe utworzenie deterministycznych stronniczych drzew wyszukiwania. Listy pomijanych stronniczo palców opisane przez Johna Iacono i Özgüra Özkan w Mergeable Dictionaries mogą być wówczas możliwe na drzewach pomijanych stronniczo. Uprzedzone drzewo palca jest sugerowane przez Demaine i in. w swoim artykule na temat czysto funkcjonalnych prób (patrz wyżej) jako sposób na ograniczenie ograniczeń czasowych i przestrzennych aktualizacji palca podczas prób.

• Ciąg B-drzewo: Nowa struktura danych do wyszukiwania ciągów w pamięci zewnętrznej i jego zastosowania Paolo Ferragina i Roberto Grossi to dobrze zbadana struktura danych łącząca zalety prób i B-drzew.

Do doskonałych notatek, które już zrobiłem, dodam Zamki błyskawiczne .

Huet, Gerard. „Functional Pearl: The Zipper” Journal of Functional Programming 7 (5): 549-554, wrzesień 1997 r.

Wikipedia: Zipper (struktura danych)

Conchon, Filliatre, A Trwała struktura danych UNION-FIND i półtrwałe struktury danych .

Dodam wersję zamków firmy McBride jako pochodne typów danych.

Rangemaps

Jest to wyspecjalizowana struktura danych, ale może być stosowana jako substytut DIET Martina Erwiga, z nieco innymi właściwościami, więc przynajmniej istnieje jedna istniejąca struktura danych do porównania. Sama DIETA została opisana w artykule w JFP w 1998 roku, więc być może nie została uwzględniona w strukturach danych o czysto funkcjonalnym charakterze.

W związku z powyższym dokumentem z 2012 r. Prace nad wektorami RRB zostały odtąd rozszerzone i opublikowane w ICFP'15.

Wektor RRB: praktyczna niezmienna sekwencja ogólnego przeznaczenia http://dl.acm.org/citation.cfm?id=2784739