I1M2014: El tipo abstracto de datos de los árboles binarios de búsqueda en Haskell

PorJosé A. Alonso

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de datos de los árboles binarios de búsqueda.

Un árbol binario de búsqueda (ABB) (binary search tree) en inglés) es un árbol binario tal que el valor de cada nodo es mayor que los valores de su subárbol izquierdo y es menor que los valores de su subárbol derecho y, además, ambos subárboles son árboles binarios de búsqueda. Por ejemplo, al almacenar los valores de [2,3,4,5,6,8,9] en un ABB se puede obtener los siguientes ABB:

El objetivo principal de los ABB es reducir el tiempo de acceso a los valores.

El contenido de la clase ha sido el siguiente:

  • la signatura del TAD de los árboles binarios de búsqueda;
  • las propiedades del TAD de los árboles binarios de búsqueda;
  • la implementación, en Haskell, de los árboles binarios de búsqueda mediante tipos de datos algebraicos.
  • la comprobación con QuickCheck de sus propiedades.

Las transparencias usadas en la clase son las del tema 19.

conversion-gate02]

Reseña: Echelon form in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Echelon form.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOL-Multivariate Analysis library, and on both the Gauss-Jordan and Cayley-Hamilton AFP entries. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, …). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.

El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs

El código de las correspondientes teorías en Isabelle se encuentra aquí.

Reseña: Isabelle and security

PorJosé A. Alonso

Se ha publicado un artículo sobre verifiación formal con Isabelle/HOL titulado Isabelle and security

Sus autores son

Su resumen es

Isabelle/HOL is a general-purpose proof assistant based on higher-order logic. Its main strengths are its simple-yet-expressive logic and its proof automation. Security researchers make up a significant fraction of Isabelle’s users. In the past few years, many exciting developments have taken place, connecting programming languages, operating system kernels, and security.