¿Qué hay de nuevo en estructuras de datos puramente funcionales desde Okasaki?

Desde el libro de 1998 de Chris Okasaki "Estructuras de datos puramente funcionales", no he visto aparecer muchas nuevas estructuras de datos puramente funcionales; Puedo nombrar solo algunos:

• IntMap (también inventado por Okasaki en 1998, pero no presente en ese libro)
• Árboles de dedos (y su generalización sobre monoides)

También hay algunas formas interesantes de implementar estructuras de datos ya conocidas, como el uso de "tipos anidados" o "tipos de datos algebraicos generalizados" para garantizar la invariabilidad de los árboles.

¿Qué otras ideas nuevas han aparecido desde 1998 en esta área?

Nuevas estructuras de datos puramente funcionales publicadas desde 1998:

• 2001: Ideal Hash Trees , y su predecesor de 2000, Búsquedas rápidas y eficientes en espacio , por Phil Bagwell : Aparentemente utilizado como un elemento fundamental en la biblioteca estándar de Clojure.

• 2001: Una técnica de implementación simple para colas de búsqueda prioritarias , por Ralf Hinze : una técnica realmente simple y hermosa para implementar esta importante estructura de datos (útil, por ejemplo, en el algoritmo Dijkstra). La implementación es particularmente hermosa y legible debido al uso intensivo de "patrones de vista".

• 2002: Bootstrapping matrices flexibles de un solo lado , por Ralf Hinze : Similar a las listas de acceso aleatorio de Okasaki, pero se pueden ajustar para alterar el equilibrio entre el tiempo consy la indexación.

• 2003: Nuevas calcomanías catenables y no catenables , por Radu Mihaescu y Robert Tarjan : una nueva versión de algunos trabajos más antiguos (de Kaplan y Tarjan) que Okasaki cita ( la versión más reciente del trabajo de Kaplan & Tarjan se publicó en 2000 ). Esta versión es más simple en algunos aspectos.

• 2005: Montones maxifóbicos ( papel y código ), por Chris Okasaki : Presentado no como una estructura nueva y más eficiente, sino como una forma de enseñar colas prioritarias.

• 2006: Listas ordenadas de tiempo constante en el peor caso puramente funcional , por Gerth Stølting Brodal, Christos Makris y Kostas Tsichlas : Responde una pregunta pendiente de Kaplan y Tarjan demostrando una estructura con O (lg n) insertar, buscar y eliminar y O (1) concat.

• 2008: Intentos con persistencia confluente para un control de versiones eficiente , por Erik D. Demaine, Stefan Langerman y Eric Price : presenta varias estructuras de datos para intentos que tienen navegación y modificación eficientes cerca de las hojas. Algunos son puramente funcionales. Otros realmente mejoran una estructura de datos de larga data de Dietz et al. para matrices totalmente persistentes (pero no confluentemente persistentes o puramente funcionales). Este documento también presenta árboles de corte de enlace puramente funcionales , a veces llamados "árboles dinámicos".

• 2010: Un nuevo algoritmo de eliminación puramente funcional para árboles rojo-negro , por Matt Might : Al igual que el algoritmo de inserción de árbol rojo-negro de Okasaki, esta no es una nueva estructura de datos o una nueva operación en una estructura de datos, sino una forma nueva y más simple de Escribe una operación conocida.

• 2012: RRB-Trees: vectores eficientes e inmutables , por Phil Bagwell y Tiark Rompf : una extensión de Hash Array Mapped Tries, que admite la concatenación de vectores inmutable, inserción y división en tiempo O (lg n), manteniendo el índice, actualización y velocidades de inserción del vector inmutable original.

Conocido en 1997, pero no discutido en el libro de Okasaki:

• Muchos otros estilos de árbol de búsqueda equilibrado . AVL, hermano, rango equilibrado, equilibrio acotado y muchos otros árboles de búsqueda equilibrados pueden (y han sido) implementados de manera puramente funcional mediante copia de ruta. Quizás merece una mención especial son:

  • Biased Search Trees , de Samuel W. Bent, Daniel D. Sleator y Robert E. Tarjan : un elemento clave en el artículo de Brodal et al. 2006 y el documento de Demaine et al. 2008.

• Conjuntos infinitos que admiten una búsqueda rápida y exhaustiva , por Martín Escardó : Quizás no sea una estructura de datos per se .

• Tres algoritmos en los árboles Braun , de Chris Okasaki : los árboles Braun ofrecen muchas operaciones de apilamiento en el peor de los casos O (lg n). Este límite es superado por muchas otras estructuras de datos, pero los árboles Braun tienen unaconsoperación perezosa en su segundo argumento, por lo que pueden usarse como pilas infinitas de alguna manera que otras estructuras no pueden.

• El montón relajado min-max: una cola prioritaria fusionable de doble extremo y El montón KD: una cola prioritaria multidimensional eficiente , por Yuzheng Ding y Mark Allen Weiss : Estos son puramente funcionales, aunque esto no se discute en los documentos . No creo que los límites de tiempo alcanzados sean mejores que los que se pueden lograr usando árboles de dedos (de Hinze & Paterson o Kaplan & Tarjan) como colas de prioridad k-dimensionales, pero creo que las estructuras de Ding & Weiss usan menos espacio .

• The Zipper , de Gérard Huet : Utilizado en muchas otras estructuras de datos (como los árboles de dedos de Hinze & Paterson), esta es una forma de convertir una estructura de datos al revés.

• Las listas de diferencias son listas catenables O (1) con una transformación O (n) a conslistas habituales . Aparentemente se conocen desde la antigüedad en la comunidad Prolog, donde tienen una transformación O (1) a las conslistas habituales . La transformación O (1) parece ser imposible en la programación funcional tradicional, pero la abstracción de agujeros de Minamide , de POPL '98, discute una forma de permitir que O (1) agregue y la transformación O (1) dentro de la programación funcional pura. A diferencia de las implementaciones de programación funcional habituales de las listas de diferencias, que se basan en el cierre de funciones, las abstracciones de agujeros son esencialmente las mismas (tanto en su uso como en su implementación) que las listas de diferencias de Prolog. Sin embargo, parece que durante años la única persona que notó esto fueuno de los revisores de Minamide .

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

Principalmente estructuras de datos funcionales, antes, durante y después del libro de Okasaki:

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

• 1989: Árboles de búsqueda aleatoria por Cecilia R. Aragon y Raimund Seidel : Guy E. Blelloch y Margaret Reid-Miller analizaron estas cuestiones en un entorno puramente funcional en Operaciones de fraguado rápido con Treaps y Dan Blandford y Guy Blelloch en Operaciones de conjuntos funcionales con Treaps ( código) Proporcionan todas las operaciones de los dedos puramente funcionales y los árboles de búsqueda sesgados, pero requieren una fuente de aleatoriedad, lo que los hace no puramente funcionales. Esto también puede invalidar la complejidad temporal de las operaciones en treaps, suponiendo un adversario que puede cronometrar las operaciones y repetir las largas. (Esta es la misma razón por la cual los argumentos de amortización imperativa no son válidos en un entorno persistente, pero requiere un adversario con un cronómetro)

• 1997: Skip-trees, una estructura de datos alternativa a Skip-lists en un enfoque concurrente , por Xavier Messeguer y Exploring the Duality Between Skip Lists and Binary Search Trees , por Brian C. Dean y Zachary H. Jones : las listas de omisión no son puramente funcional, pero pueden implementarse funcionalmente como árboles. Al igual que los treaps, requieren una fuente de bits aleatorios. (Es posible hacer que las listas de salto sean deterministas, pero, después de traducirlas a un árbol, creo que son solo otra forma de ver 2-3 árboles).

• 1998: ¡ Todas las estructuras amortizadas en el libro de Okasaki! Okasaki inventó este nuevo método para mezclar la amortización y las estructuras de datos funcionales, que anteriormente se consideraban incompatibles. Depende de la memorización, que, como Kaplan y Tarjan han mencionado a veces, es en realidad un efecto secundario. En algunos casos ( como PFDS en SSD por razones de rendimiento ), esto puede ser inapropiado.

• 1998: Listas de Catenable simples y persistentes con confianza , por Haim Kaplan, Chris Okasaki y Robert E. Tarjan : utiliza la modificación debajo del capó para proporcionar calcos catenables O (1) amortizados, presentando la misma interfaz que una anterior (puramente funcional, pero con memoria) ) versión que aparece en el libro de Okasaki. Kaplan y Tarjan habían creado anteriormente una estructura puramente funcional O (1) en el peor de los casos, pero es sustancialmente más complicada.

• 2007: como se menciona en otra respuesta en esta página, estructuras de datos semipersistentes y persistente unión de hallazgos por Sylvain Conchon y Jean-Christophe Filliâtre

Técnicas para verificar estructuras de datos funcionales, antes, durante y después del libro de Okasaki:

• Los tipos fantasma son un método antiguo para crear una API que no permite ciertas operaciones mal formadas. Se puede encontrar un uso sofisticado de ellos en las capacidades estáticas ligeras de Oleg Kiselyov y Chung-chieh Shan .

• Los tipos anidados no son en realidad más recientes que 1998; Okasaki incluso los usa en su libro. Hay muchos otros ejemplos que no están en el libro de Okasaki; algunos son nuevos y otros son viejos. Incluyen:

  • Árboles rojos y negros de Stefan Kahrs con tipos ( código )
  • Árboles AVL de Ross Paterson ( espejo )
  • De Chris Okasaki De la exponenciación rápida a las matrices cuadradas: una aventura en tipos
  • La notación de Bruijn de Richard S. Bird y Ross Peterson como un tipo de datos anidado
  • Las representaciones numéricas de Ralf Hinze como tipos de datos anidados de orden superior .

• Los GADT tampoco son tan nuevos. Son una adición reciente a Haskell y algunos ML, pero creo que han estado presentes en varios cálculos lambda mecanografiados desde la década de 1970 .

• 2004-2010: Coq e Isabelle para la corrección . Varias personas han utilizado demostradores de teoremas para verificar la exactitud de las estructuras de datos puramente funcionales. Coq puede extraer estas verificaciones al código de trabajo en Haskell, OCaml y Scheme; Isabelle puede extraer a Haskell, ML y OCaml.

  • Coq:
    • Pierre Letouzey y Jean-Christophe Filliâtre formalizaron árboles rojo-negro y AVL (ish), encontrando un error en la biblioteca estándar OCaml en el proceso .
    • Me Formalicé Brodal y de Okasaki colas de prioridad asintóticamente óptimos .
    • Arthur Charguéraud formalizó 825 de las 1.700 líneas de ML en el libro de Okasaki .
  • Isabelle:
    • Tobias Nipkow y Cornelia Pusch formalizaron árboles AVL .
    • Viktor Kuncak formalizó árboles de búsqueda binaria desequilibrados .
    • Peter Lammich publicó el marco de Isabelle Collections , que incluye formalizaciones de estructuras de datos eficientes y puramente funcionales como árboles e intentos rojo-negros, así como estructuras de datos que son menos eficientes cuando se usan de manera persistente, como las colas de dos pilas (sin el truco de pereza de Okasaki ) y tablas hash.
    • Peter Lammich también publicó formalizaciones de autómatas de árboles , árboles de dedos de Hinze & Patterson (con Benedikt Nordhoff y Stefan Körner), y colas de prioridad puramente funcionales de Brodal y Okasaki (con Rene Meis y Finn Nielsen).
    • René Neumann formalizó las colas de prioridad binomial .

• 2007: Comprobación de tipos refinada con Stardust , por Joshua Dunfield : este documento utiliza tipos de refinamiento para ML para encontrar errores en la función de eliminación de árbol rojo-negro de SMLNJ.

• 2008: Análisis de complejidad de tiempo semiformal ligero para estructuras de datos puramente funcionales por Nils Anders Danielsson : utiliza Agda con anotación manual para probar los límites de tiempo para algunos PFDS.

Estructuras de datos imperativos o análisis no discutidos en el libro de Okasaki, pero relacionados con estructuras de datos puramente funcionales:

• The Soft Heap: una cola de prioridad aproximada con una tasa de error óptima , por Bernard Chazelle : esta estructura de datos no usa matrices, por lo que ha tentado primero al canal #haskell IRC y luego a los usuarios de Stack Overflow , pero incluyedeleteen o (lg n) , que generalmente no es posible en un entorno funcional, y el análisis amortizado imperativo, que no es válido en un entorno puramente funcional.

• Árboles de búsqueda binaria equilibrada con actualizaciones de dedo O (1) . En Making Data Structures Persistent , James R Driscoll, Neil Sarnak, Daniel D. Sleator y Robert E. Tarjan presentan un método para agrupar los nodos en un árbol rojo-negro para que las actualizaciones persistentes requieran solo espacio O (1). Los deques y árboles de dedos puramente funcionales diseñados por Tarjan, Kaplan y Mihaescu utilizan una técnica de agrupación muy similar para permitir actualizaciones de O (1) en ambos extremos. Los árboles AVL para la búsqueda localizada por Athanasios K. Tsakalidis funcionan de manera similar.

• Montones de emparejamiento más rápidos o mejores límites para los montones de emparejamientos : desde que se publicó el libro de Okasaki, han aparecido varios análisis nuevos de montones de emparejamientos imperativos, incluidos los montones de emparejamientos con O (log log n) disminuyen el costo por Amr Elmasry y hacia un análisis final de los montones de emparejamientos por Seth Pettie. Es posible aplicar parte de este trabajo a los montones de emparejamiento perezoso de Okasaki.

• Árboles dedos sesgados deterministas : En Listas Skip sesgada , por Amitabha Bagchi, Adam L. Buchsbaum, y Michael T. Goodrich, un diseño se presenta para las listas de salto sesgadas deterministas. A través de la lista de salto / transformación de árbol mencionada anteriormente, puede ser posible hacer árboles de búsqueda sesgados deterministas. Las listas de salto sesgadas con los dedos descritas por John Iacono y Özgür Özkan en Mergeable Dictionaries podrían ser posibles en los árboles de salto sesgados. Demaine et al. Sugieren un árbol de dedos sesgado. en su artículo sobre intentos puramente funcionales (ver arriba) como una forma de reducir los límites de tiempo y espacio en la actualización de los dedos en los intentos.

• The String B-Tree: una nueva estructura de datos para la búsqueda de cadenas en la memoria externa y sus aplicaciones por Paolo Ferragina y Roberto Grossi es una estructura de datos bien estudiada que combina los beneficios de los intentos y los B-trees.

A las excelentes notas ya hechas, agregaré Zippers .

Huet, Gerard. "Functional Pearl: The Zipper" Journal of Functional Programming 7 (5): 549-554, septiembre de 1997.

Wikipedia: Cremallera (estructura de datos)

Conchon, Filliatre, una estructura de datos persistente UNION-FIND y estructuras de datos semipersistentes .

Agregaría la versión de cremalleras de McBride como derivados de tipos de datos.

Rangemaps

Es una estructura de datos especializada, pero se puede usar como un sustituto de la DIETA de Martin Erwig, con propiedades ligeramente diferentes, por lo que al menos hay una estructura de datos existente para compararla. La DIETA misma se describió en un artículo en JFP en 1998, por lo que quizás no se incluye en las Estructuras de datos puramente funcionales.

En seguimiento al documento de 2012 vinculado anteriormente, el trabajo sobre los vectores RRB se ha extendido y publicado en ICFP'15.

Vector RRB: una secuencia inmutable práctica de propósito general http://dl.acm.org/citation.cfm?id=2784739