Library of Efficient Data types and Algorithms

LEDA provides four additional numerical representations alongside those built-in to C++: integer, rational, bigfloat, and real:

• LEDA's integer type offers an improvement over the built-in int datatype by eliminating the problem of overflow at the cost of unbounded memory usage for increasingly large numbers.
• It follows that LEDA's rational type has the same resistance to overflow because it is based directly on the mathematical definition of rational as the quotient of two integers.
• The bigfloat type improves on the C++ floating-point types by allowing for the significand (also commonly called mantissa) to be set to an arbitrary level of precision instead of following the IEEE standard.
• LEDA's real type allows for precise representations of real numbers, and can be used to compute the sign of a radical expression.^[1]

LEDA makes use of certifying algorithms to demonstrate that the results of a function are mathematically correct. In addition to the input and output of a function, LEDA computes a third "witness" value which can be used as an input to checker programs to validate the output of the function. LEDA's checker programs were developed in Simpl, an imperative programming language, and validated using Isabelle/HOL, a software tool for checking the correctness of mathematical proofs.^[3]

The nature of a witness value often depends on the type of mathematical calculation being performed. For LEDA's planarity testing function, If the graph is planar, a combinatorial embedding is produced as a witness. If not, a Kuratowski subgraph is returned. These values can then be passed directly to checker functions to confirm their validity. A developer only needs to understand the inner-workings of these checker functions to be confident that the result is correct, which greatly reduces the learning curve compared to gaining a full understanding of LEDA's planarity testing algorithm.^[4]

LEDA is useful in the field of computational geometry due to its support for exact representations of real numbers via the leda_real datatype. This provides an advantage in accuracy over floating-point arithmetic. For example, calculations involving radicals are considerably more accurate when computed using leda_real. Algorithms such as parametric search, a technique for solving a subset of optimization problems, and others under the real RAM model of computation rely upon real number parameters to produce accurate results.^[5]

Boost and LEMON are potential alternative libraries with some benefits in efficiency due to different implementations of fundamental algorithms and data structures. However, neither employs a similar set of correctness checking, particularly when dealing with floating-point arithmetic. CGAL is an alternative for geometric algorithms and also combines floating point, interval , and arbitrary precision arithmetic to achieve robustness. ^[3]