Quoi de neuf dans les structures de données purement fonctionnelles depuis Okasaki?

Depuis le livre de Chris Okasaki paru en 1998 "Des structures de données purement fonctionnelles", je n'ai pas vu apparaître trop de nouvelles structures de données passionnantes et purement fonctionnelles; Je peux n'en nommer que quelques-uns:

• IntMap (également inventé par Okasaki en 1998, mais non présent dans ce livre)
• Arbres à doigt (et leur généralisation sur les monoïdes)

Il existe également des méthodes intéressantes pour mettre en œuvre des infrastructures de données déjà connues, telles que l’utilisation de "types imbriqués" ou de "types de données algébriques généralisés" pour garantir des invariants d’arbres.

Quelles autres idées nouvelles sont apparues depuis 1998 dans ce domaine?

Nouvelles structures de données purement fonctionnelles publiées depuis 1998:

• 2001: Ideal Hash Trees , et son prédécesseur de 2000, Fast and Space Efficient Trie Recherches , par Phil Bagwell : Apparemment utilisé comme un bloc de construction fondamental dans la bibliothèque standard de Clojure.

• 2001: Une technique d'implémentation simple pour les files de recherche prioritaires , par Ralf Hinze : une technique très simple et esthétique pour l'implémentation de cette importante infrastructure de données (utile, par exemple, dans l'algorithme de Dijkstra). La mise en œuvre est particulièrement belle et lisible en raison de l'utilisation intensive de "modèles de vue".

• 2002: Amorçage des tableaux flexibles unilatéraux , par Ralf Hinze : similaires aux listes à accès aléatoire d'Okasaki, mais elles peuvent être ajustées pour modifier le compromis temps cons-index / index.

• 2003: Deques nouvelles caténables et non caténables , de Radu Mihaescu et Robert Tarjan : une nouvelle version de certains travaux plus anciens (de Kaplan et Tarjan) cités par Okasaki (La version la plus récente du travail de Kaplan & Tarjan a été publiée en 2000 ). Cette version est plus simple à certains égards.

• 2005: Les tas maxiphobiques ( papier et code ), de Chris Okasaki : présentés non pas comme une nouvelle structure plus efficace, mais comme un moyen d'enseigner les files d'attente prioritaires.

• 2006: Listes classées par ordre chronologique de pires cas, purement fonctionnelles , de Gerth Stølting Brodal, Christos Makris et Kostas Tsichlas : répond à une question en suspens de Kaplan et de Tarjan en présentant une structure avec O (lg n), insérer, rechercher et effacer (1) concat.

• 2008: essais persistants pour un contrôle de version efficace , par Erik D. Demaine, Stefan Langerman et Eric Price : présente plusieurs structures de données pour les essais avec une navigation et une modification efficaces près des feuilles. Certains sont purement fonctionnels. D'autres améliorent en fait une structure de données de longue date de Dietz et al. pour des tableaux totalement persistants (mais pas persistants de manière confluente ou purement fonctionnels). Cet article présente également des arbres coupés de liens purement fonctionnels , parfois appelés "arbres dynamiques".

• 2010: Un nouvel algorithme de suppression purement fonctionnel pour les arbres rouge-noir , par Matt Might : comme l'algorithme d'insertion d'arbre rouge-noir d'Okasaki, il ne s'agit pas d'une nouvelle structure de données ni d'une nouvelle opération sur une structure de données, mais d'une nouvelle méthode plus simple écrire une opération connue.

• 2012: RRB-Trees: Vecteurs immuables efficaces , par Phil Bagwell et Tiark Rompf : Une extension des tentatives mappées avec tableau de hachage, prenant en charge la concaténation de vecteurs immuables, l'insertion et la scission en temps O (lg n), tout en conservant l'indice, mise à jour et les vitesses d'insertion du vecteur immuable d'origine.

Connu en 1997, mais non abordé dans le livre d'Okasaki:

• Beaucoup d'autres styles d'arborescence de recherche équilibrée . L'AVL, le frère, l'équilibre hiérarchique, l'équilibre équilibré et de nombreux autres arbres de recherche équilibrés peuvent être (et ont été) mis en œuvre de manière purement fonctionnelle par copie de chemins. Peut-être méritent une mention spéciale:

  • Arbres de recherche biaisés , par Samuel W. Bent, Daniel D. Sleator et Robert E. Tarjan : un élément clé de l'article de Brodal et al. De 2006 et de l'article de Demaine et al., 2008.

• Ensembles infinis qui permettent une recherche exhaustive rapide , par Martín Escardó : Peut-être pas une structure de données en soi .

• Trois algorithmes sur les arbres Braun , par Chris Okasaki : Les arbres Braun offrent de nombreuses opérations de pile dans le cas le plus défavorable O (lg n). Cette limite est dépassée par de nombreuses autres structures de données, mais les arbres Braun ont uneconsopération paresseuse dans leur deuxième argument et peuvent donc être utilisés comme des piles infinies à certains égards, contrairement aux autres structures.

• Le tas relaxé min-max: une file d'attente prioritaire fusionnable à deux extrémités et le tas KD: une file d'attente efficace multidimensionnelle efficace , par Yuzheng Ding et Mark Allen Weiss : Celles-ci sont purement fonctionnelles, bien que cela ne soit pas discuté dans les journaux . Je ne pense pas que les délais atteints soient meilleurs que ceux qui peuvent être atteints en utilisant des arbres à doigts (de Hinze & Paterson ou Kaplan & Tarjan) comme files d'attente prioritaires à dimension k, mais je pense que les structures de Ding & Weiss utilisent moins d'espace. .

• La fermeture à glissière , de Gérard Huet : Utilisé dans de nombreuses autres structures de données (telles que les empreintes digitales de Hinze & Paterson), il permet de retourner une structure de données à l'envers.

• Les listes de différences sont des listes caténables par O (1) avec une transformation par O (n) en conslistes habituelles . Ils sont apparemment connus depuis l'antiquité dans la communauté Prolog, où ils subissent une transformation en O (1) en conslistes habituelles . La transformation O (1) semble être impossible dans la programmation fonctionnelle traditionnelle, mais l'abstraction de trous de Minamide, à partir de POPL '98, discute d'une manière de permettre la transformation O (1) append et O (1) au sein de la programmation fonctionnelle pure. Contrairement aux implémentations de programmation fonctionnelle habituelles des listes de différences, qui sont basées sur les fermetures de fonctions, les abstractions de trous sont essentiellement les mêmes (dans leur utilisation et leur implémentation) que les listes de différences de Prolog. Cependant, il semble que pendant des années, la seule personne qui l’ait remarqué étaitun des critiques de Minamide .

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

Principalement des structures de données fonctionnelles, avant, pendant et après le livre d'Okasaki:

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

• 1989: Recherche Arbres répartition aléatoire par Cecilia R. Aragon et Raimund Seidel : Ils ont été discutés dans un cadre purement fonctionnel par Guy E. Blelloch et Margaret Reid-Miller dans des opérations de prise rapide Utilisation Treaps et par Dan Blandford et Guy Blelloch dans les opérations Set fonctionnels avec Treaps ( code). Ils fournissent toutes les opérations des onglets purement fonctionnels et des arbres de recherche biaisés, mais nécessitent une source aléatoire, ce qui les rend non purement fonctionnels. Cela peut également invalider la complexité temporelle des opérations sur les pistes, en supposant un adversaire capable de chronométrer les opérations et de répéter les plus longues. (C’est la même raison pour laquelle les arguments d’amortissement impératifs ne sont pas valables dans un contexte persistant, mais il faut un adversaire avec un chronomètre)

• 1997: Skip-trees, une structure de données alternative aux listes de sauts dans une approche concurrente , de Xavier Messeguer et Exploration de la dualité entre les listes de sauts et les arbres de recherche binaires , de Brian C. Dean et Zachary H. Jones : Les listes de sauts ne sont pas purement et simplement fonctionnel, mais ils peuvent être implémentés fonctionnellement sous forme d’arbres. Comme les treaps, ils nécessitent une source de bits aléatoires. (Il est possible de faire des listes de sauts déterministes, mais, après les avoir traduites en un arbre, je pense qu’elles ne sont qu’une autre façon de regarder 2-3 arbres.)

• 1998: Toutes les structures amorties du livre d'Okasaki! Okasaki a inventé cette nouvelle méthode de mélange d’amortissement et de structures de données fonctionnelles, auparavant considérées comme incompatibles. Cela dépend de la mémorisation, qui, comme Kaplan et Tarjan l'ont parfois mentionné, est en réalité un effet secondaire. Dans certains cas ( tels que PFDS sur SSD pour des raisons de performances ), cela peut être inapproprié.

• 1998: Listes simples de catalogues persistants confluents , de Haim Kaplan, Chris Okasaki et Robert E. Tarjan : Modifications sous le capot pour donner des deques caténables amorties O (1), présentant la même interface qu'un précédent (purement fonctionnel, mais avec mémo ) dans le livre d’Okasaki. Kaplan et Tarjan avaient précédemment créé une structure purement fonctionnelle O (1) dans le cas du pire des cas, mais elle est nettement plus compliquée.

• 2007: comme mentionné dans une autre réponse sur cette page, structures de données semi-persistantes et recherche d' union persistante par Sylvain Conchon et Jean-Christophe Filliâtre

Techniques de vérification des structures de données fonctionnelles avant, pendant et après le livre d'Okasaki:

• Les types fantômes sont une ancienne méthode pour créer une API qui n'autorisait pas certaines opérations mal formées. On en trouve une utilisation sophistiquée dans les capacités statiques légères d' Oleg Kiselyov et de Chung-chieh Shan .

• Les types imbriqués ne sont en réalité pas plus récents que 1998 - Okasaki les utilise même dans son livre. Il y a beaucoup d'autres exemples qui ne figurent pas dans le livre d'Okasaki; certains sont nouveaux et certains sont vieux. Ils incluent:

  • Les arbres rouge-noirs de Stefan Kahrs avec des types ( code )
  • Arbres AVL de Ross Paterson ( miroir )
  • De l'exponentiation rapide aux matrices carrées de Chris Okasaki : une aventure en types
  • La notation de De Bruijn de Richard S. Bird et Ross Peterson en tant que type de données imbriqué
  • Représentations numériques de Ralf Hinze en tant que types de données imbriqués d'ordre supérieur .

• Les GADT ne sont pas non plus nouveaux. Il s’agit d’un ajout récent à Haskell et à certains ML, mais ils sont présents, je pense, dans divers calculs lambda typés depuis les années 1970 .

• 2004-2010: Coq et Isabelle pour l'exactitude . Plusieurs personnes ont utilisé des démonstrateurs de théorèmes pour vérifier l'exactitude de structures de données purement fonctionnelles. Coq peut extraire ces vérifications du code de travail dans Haskell, OCaml et Scheme; Isabelle peut extraire à Haskell, ML et OCaml.

  • Coq:
    • Pierre Letouzey et Jean-Christophe Filliâtre ont formalisé les arbres rouge-noir et AVL (ish), trouvant un bogue dans la bibliothèque standard OCaml .
    • J'ai officialisé les files d'attente prioritaires asymptotiquement optimales de Brodal et Okasaki .
    • Arthur Charguéraud a formalisé 825 des 1 700 lignes de ML dans le livre d'Okasaki .
  • Isabelle:
    • Tobias Nipkow et Cornelia Pusch ont officialisé les arbres AVL .
    • Viktor Kuncak a officialisé des arbres de recherche binaires non équilibrés .
    • Peter Lammich a publié Le cadre Isabelle Collections , qui inclut des formalisations de structures de données efficaces purement fonctionnelles, telles que les arbres et les essais rouge-noirs, ainsi que des structures de données moins efficaces lorsqu'elles sont utilisées de manière persistante, telles que les files d'attente à deux piles (sans le paresseux d'Okasaki) ) et tables de hachage.
    • Peter Lammich a également publié les formalisations d' automates d'arbres , des arbres à doigts de Hinze & Patterson (avec Benedikt Nordhoff et Stefan Körner) et des files d'attente prioritaires purement fonctionnelles de Brodal et Okasaki (avec Rene Meis et Finn Nielsen).
    • René Neumann a officialisé les files d'attente binomiales prioritaires .

• 2007: Vérification typographique raffinée avec Stardust , par Joshua Dunfield : Ce document utilise des types de raffinement pour ML afin de rechercher les erreurs dans la fonction de suppression d'arbre rouge-noir de SMLNJ.

• 2008: Analyse légère de complexité temporelle semi-formelle pour des structures de données purement fonctionnelles par Nils Anders Danielsson : Utilise Agda avec une annotation manuelle pour prouver les limites de temps pour certains PFDS.

Structures de données impératives ou analyses non abordées dans le livre d'Okasaki, mais liées à des structures de données purement fonctionnelles:

• Soft Heap: Une approximative file d' attente prioritaire avec un taux d'erreur optimal , par Bernard Chazelle : Cette structure de données n'utilise pastableaux, et a donc tenté d' abord le canal IRC #haskell et plus tard Stack utilisateurs trop - plein , mais il comprenddeleteen o (lg n) , ce qui n’est généralement pas possible dans un environnement fonctionnel, et l’analyse impérative avec amortissement, qui n’est pas valable dans un environnement purement fonctionnel.

• Arbres de recherche binaires équilibrés avec O (1) mises à jour de doigts . Dans Rendre les structures de données persistantes , James R. Driscoll, Neil Sarnak, Daniel D. Sleator et Robert E. Tarjan présentent une méthode de regroupement des nœuds dans un arbre rouge-noir afin que les mises à jour persistantes ne requièrent que de l'espace O (1). Les arbres à doigts et à doigts purement fonctionnels conçus par Tarjan, Kaplan et Mihaescu utilisent tous une technique de regroupement très similaire pour permettre des mises à jour de O (1) aux deux extrémités. Les arbres AVL pour la recherche localisée par Athanasios K. Tsakalidis fonctionnent de la même manière.

• Plus rapide des tas d'appariement ou de meilleures limites pour des tas d'appariement : Depuis le livre de Okasaki a été publié, plusieurs nouvelles analyses des tas d'appariement impératif sont apparus, y compris des tas de jumelage avec O (log log n) diminuent le coût par Amr Elmasry et vers une analyse finale de l' appariement Heaps par Seth Pettie. Il est peut-être possible d’appliquer une partie de ce travail sur les tas d’appariements paresseux d’Okasaki.

• Arbres doigt biaisés déterministes : Dans Biased listes de saut , par Amitabha Bagchi, Adam L. Buchsbaum et Michael T. Goodrich, un dessin est présenté pour les listes de saut déterministes biaisées. Grâce à la transformation de la liste de sauts / des arbres mentionnée ci-dessus, il peut être possible de créer des arbres de recherche biaisés et déterministes. Les listes de sauts biaisés par les doigts décrits par John Iacono et Özgür Özkan dans Dictionnaires fusionnés pourraient alors être possibles sur des sauts biaisés. Un arbre à doigts biaisé est suggéré par Demaine et al. dans leur document sur les essais purement fonctionnels (voir ci-dessus) comme moyen de réduire les limites de temps et d'espace lors de la mise à jour du doigt dans les essais.

• String B-tree: une nouvelle structure de données pour la recherche de chaînes dans la mémoire externe et ses applications de Paolo Ferragina et Roberto Grossi est une structure de données bien étudiée combinant les avantages des essais et des B-trees.

Aux excellentes notes déjà faites, je vais ajouter les fermetures éclair .

Huet, Gérard. «Perle fonctionnelle: la fermeture à glissière» Journal de programmation fonctionnelle 7 (5): 549-554, septembre 1997.

Wikipedia: Zipper (structure de données)

Conchon, Filliatre, une structure de données UNION-FIND persistante et des structures de données semi-persistantes .

J'ajouterais la version de McBride des fermetures à glissière en tant que dérivés des types de données.

Cartes de rangée

C'est une structure de données spécialisée, mais elle peut remplacer le DIET de Martin Erwig, avec des propriétés légèrement différentes, de sorte qu'il existe au moins une structure de données existante à laquelle le comparer. Le régime lui-même a été décrit dans un article paru dans JFP en 1998; il n’est donc peut-être pas inclus dans les structures de données purement fonctionnelles.

Pour faire suite au document de 2012 lié ci-dessus, les travaux sur les vecteurs RRB ont depuis été étendus et publiés dans ICFP'15.

Vecteur RRB: séquence immuable pratique polyvalente http://dl.acm.org/citation.cfm?id=2784739