La Biblioteca de tipos y algoritmos de datos eficientes (LEDA) es una biblioteca de software con licencia patentada que proporciona implementaciones C ++ de una amplia variedad de algoritmos para la teoría de grafos y la geometría computacional . [1] Fue desarrollado originalmente por el Instituto Max Planck de Informática Saarbrücken . [2] Desde 2001, LEDA es desarrollado y distribuido por Algorithmic Solutions Software GmbH.
LEDA está disponible como edición gratuita, de investigación y profesional. La edición gratuita es gratuita , con acceso al código fuente disponible para su compra. Las ediciones Research y Professional requieren el pago de tarifas de licencia para cualquier uso. Desde octubre de 2017, los algoritmos de gráficos LEDA también están disponibles para el entorno de desarrollo de Java .
Detalles técnicos
Tipos de datos
Representaciones numéricas
LEDA proporciona cuatro representaciones numéricas adicionales junto con las integradas en C ++: integer , racional , bigfloat y real . El tipo de entero de LEDA ofrece una mejora sobre el tipo de datos int incorporado al eliminar el problema del desbordamiento a costa del uso ilimitado de memoria para números cada vez más grandes. De ello se deduce que el tipo racional de LEDA tiene la misma resistencia al desbordamiento porque se basa directamente en la definición matemática de racional como el cociente de dos enteros . El tipo bigfloat mejora los tipos de punto flotante de C ++ al permitir que la mantisa se establezca en un nivel arbitrario de precisión en lugar de seguir el estándar IEEE . El tipo real de LEDA permite representaciones precisas de números reales y se puede utilizar para calcular el signo de una expresión radical. [1]
Comprobación de errores
LEDA utiliza algoritmos de certificación para demostrar que los resultados de una función son matemáticamente correctos. Además de la entrada y salida de una función, LEDA calcula un tercer valor "testigo" que se puede utilizar como entrada para los programas de verificación para validar la salida de la función. Los programas de verificación de LEDA se desarrollaron en Simpl, un lenguaje de programación imperativo , y se validaron utilizando Isabelle / HOL , una herramienta de software para verificar la exactitud de las pruebas matemáticas. [3]
La naturaleza de un valor testigo a menudo depende del tipo de cálculo matemático que se realice. Para la función de prueba de planaridad de LEDA, si el gráfico es plano , se produce una incrustación combinatoria como testigo. De lo contrario, se devuelve un subgrafo de Kuratowski . Estos valores se pueden pasar directamente a las funciones de verificación para confirmar su validez. Un desarrollador solo necesita comprender el funcionamiento interno de estas funciones de verificación para estar seguro de que el resultado es correcto, lo que reduce en gran medida la curva de aprendizaje en comparación con obtener una comprensión completa del algoritmo de prueba de planaridad de LEDA. [4]
Casos de uso
LEDA es útil en el campo de la geometría computacional debido a su soporte para representaciones exactas de números reales a través del tipo de datos leda_real . Esto proporciona una ventaja en la precisión sobre la aritmética de punto flotante . Por ejemplo, los cálculos que involucran radicales son considerablemente más precisos cuando se calculan usando leda_real . Algoritmos como la búsqueda paramétrica , una técnica para resolver un subconjunto de problemas de optimización, y otros bajo el modelo de cálculo de RAM real se basan en parámetros de números reales para producir resultados precisos. [5]
Alternativas
Boost y LEMON son bibliotecas alternativas potenciales con algunos beneficios en eficiencia debido a diferentes implementaciones de algoritmos fundamentales y estructuras de datos. Sin embargo, ninguno emplea un conjunto similar de verificación de corrección, particularmente cuando se trata de aritmética de punto flotante. [3]
Referencias
- ^ a b Mehlhorn, Kurt; Näher, Stefan (1999), LEDA: A Platform for Combinatorial and Geometric Computing , Cambridge University Press, ISBN 978-0-521-56329-1.
- ^ "LEDA - una biblioteca de tipos de datos y algoritmos eficientes" . Universidad de Stony Brook . Consultado el 21 de febrero de 2019 .
- ^ a b Abdulaziz, Mohammad; Mehlhorn, Kurt; Nipkow, Tobias (2019). "Algoritmos gráficos fiables". En Rossmanith, Peter; Heggernes, Pinar; Katoen, Joost-Pieter (eds.). 44o Simposio Internacional sobre Fundamentos Matemáticos de la Informática, MFCS 2019, 26-30 de agosto de 2019, Aquisgrán, Alemania . LÍPICOS. 138 . Schloss Dagstuhl - Leibniz-Zentrum für Informatik. págs. 1: 1–1: 22. arXiv : 1907.04065 . doi : 10.4230 / LIPIcs.MFCS.2019.1 .
- ^ Mehlhorn, Kurt; Näher, Stefan (1998), Brim, Luboš; Gruska, Jozef; Zlatuška, Jiří (eds.), "A partir de algoritmos a los programas de trabajo: En el uso del programa de comprobación en ADEL" , Fundamentos Matemáticos de la Informática 1998 , Springer Berlin Heidelberg, 1450 , pp. 84-93 , doi : 10.1007 / bfb0055759 , ISBN 978-3-540-64827-7, consultado el 22 de noviembre de 2019
- ^ Mehlhorn, Kurt; Schirra, Stefan (2001). "Computación exacta con leda_real - Teoría y aplicaciones geométricas" (PDF) . Métodos algebraicos simbólicos y métodos de verificación . Viena: Springer Verlag: 163-172. doi : 10.1007 / 978-3-7091-6280-4_16 . ISBN 978-3-211-83593-7.
enlaces externos
- Página web oficial