El tipo abstracto de datos de los polinomios en Haskell

Como comenté en la entrada anterior, estoy elaborando los apuntes de los temas del curso Informática del Grado en Matemáticas (2010-11) no incluidos aún en el libro Temas de programación funcional (2010-11).

Uno de los temas en los que he estado trabajando últimamente es en el de los tipos abstractos de datos (TAD). Además de los habituales (pilas, colas, colas de prioridad, conjuntos, tablas, árboles binarios de búsqueda, montículos y árboles AVL), un TAD especialmente adecuado para los estudiantes de matemáticas es el de polinomios. A continuación muestro la implementación que estoy diseñando en Haskell para incluirla en el tema.

Del código deseo resaltar las siguientes características:

  • Independización de los resultados de las implementaciones mediante las funciones de escritura.
  • Comprobación de las implementaciones con QuickCheck mediante las funciones generadoras de polinomios.

A continuación muestro los ficheros con los códigos desarrollados.
Read More “El tipo abstracto de datos de los polinomios en Haskell”

Curso de Informática (del Grado en Matemáticas)

Como he comentado en otras entradas, uno de los objetivos de este blog es servir de diario de las publicaciones docentes que realizo en mi página personal.

Esta semana he publicado el curso Informática del Grado en Matemáticas (2010-11) que se impartirá desde el 4 de Octubre al 10 de Junio de 2011.

El material del curso publicado hasta ahora está englobado en los siguientes libros:

A lo largo del curso se irán ampliando con los ejercicios, los exámenes y los apuntes de los temas restantes.

Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases

Se ha publicado recientemente el artículo Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases.

En el artículo se presenta una forma de combinar sistemas SAT (basados en el algoritmo DPLL) y bases de Gröbner de forma que cuando se encuentran conflictos, el aprendizaje de las nuevas cláusulas se realice mediante bases de Gröbner en lugar de hacerlo por resolución.

Para experimentar la propuesta, han creado el sistema MiniSat+GB en el que integran el sistema MiniSat con la librería para el cálculo de bases de Gröbner del sistema de cálculo simbólico Reduce.

En los resultados de los experimentos se observa cómo MiniSat+GB supera en eficiencia a MiniSat en los casos en los que se requiere más tiempo de cómputo.

Los autores del artículo son Christoph Zengler y Wolfgang Küchlin que son miembros del Grupo de cálculo simbólico de la Universidad de Tubinga (Tübingen en alemán), Alemania.

El artículo se ha publicado en el LNCS 6244: Computer Algebra in Scientific Computing. (12th International Workshop, CASC 2010)

Libro de introducción al cálculo simbólico con Maxima (versión 2)

En una entrada anterior anuncié la publicación de la primera versión de un libro de introducción al cálculo simbólico con Maxima.

He publicado una nueva versión del libro en la que he eliminado erratas e incluidos los comentarios recibidos.

Esta nueva versión es la que usaré este curso en la asignatura de Informática de 1º de Matemáticas.

En el libro se hace una presentación de Maxima a través de ejercicios resueltos (que se comentan en clases) y propuestos (para resolver por los alumnos en la wiki de la asignatura y, posteriormente, comentar as soluciones en clase).

Esta es la segunda versión del libro y he incluido también las soluciones de los ejercicios propuestos. Espero vuestros comentarios para las siguientes versiones.

Trabajo de lógica computacional en Kassel

El Grupo de Métodos Formales y Verificación de la Universidad de Kassel, Alemania, ha publicado el anuncio de la oferta de una plaza postdoctoral para trabajar en lógica computacional.

El trabajo se desarrollará en el proyecto ERC Model Checking Unleashed.

El objetivo del trabajo es el estudio de aplicaciones no estándard de las técnicas de verificación de modelos (en inglés, model checking) en varias áreas de ciencias de la verificación y temas relacionados.