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

PorJosé A. Alonso

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

PorJosé A. Alonso

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.

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

PorJosé A. Alonso

Se ha publicado un nuevo artículo de formalización: Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Los autores del artículo son Freek Verbeek y Julien Schmaltz de la Universiad de Radboud en Nimega (en neerlandés: Nijmegen), Paises Bajos.

El artículo se publicó ayer (18 de Septiembre de 2010) en el Journal of Automated Reasoning.

Una versión preliminar del artículo puede leerse aquí y el código ACL2 correspondiente puede obtenerse aquí

El artículo es una demostración en ACL2 de una condición necesaria y suficiente para enrutamiento sin estancamiento introducida por William J. Dally y Charles L. Seitz en su artículo Deadlock Free Message Routing in Multiprocessor Interconnection Networks de 1987.
Read More “Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks”

La profesión de matemático

PorJosé A. Alonso

Ordenando la mesa de trabajo me he encontrado una ficha en la que anoté, hace más de 30 años, los aspectos de la profesión de matemático que describe Georges Glaeser en su libro Mathématiques pour l’élève professeur (Hermann, 1971). Dichos aspectos los describe en la página 17 donde dice

Hacer matemáticas es una actividad compleja, que involucra aptitudes variadas. Un matemático se mantiene en el ejercicio de su profesión cuando se entrega a trabajos tan dispares como:

  • Plantearse problemas y resolverlos. Idear teoremas y demostrarlos.
  • Resolver problemas de los que no ha concebido el enunciado personalmente.
  • Participar en la circulación de la información matemática tomando parte activa en seminarios consagrados a trabajos recientes. Redactar en forma sintética resultados obtenidos por otros investigadores que trabajan en temas cercanos.
  • Estudiar teorías clásicas o acabadas. Preparar exposiciones magistrales y redactar libros. Enseñar.
  • Aplicar técnicas matemáticas (cálculo, programación, métodos gráficos, estadísticos, etc.).
  • Adaptar métodos abstractos a la solución de problemas prácticos (ciencias aplicadas).

En realidad, la mayoría de los matemáticos sólo conocen algunas de las actividades citadas y tienen tendencia a ignorar, desatender o subestimar las otras.

Comparación de 3 implementaciones de Common Lisp (Clisp, GCL y SBCL) mediante la función de Takeuchi

PorJosé A. Alonso

En artículos anteriores comentamos la función de Takeuchi como prueba de rendimiento y la usamos para la comparación del rendimiento de Haskell, Maxima y Common Lisp.

En este artículo voy a usar una variación de la prueba anterior para comparar tres implementaciones de Common Lisp: Clisp, GCL (GNU Common Lisp) y SBCL (Steel Bank Common Lisp).

La función de Takeuchi es
tak(x,y,z) = \newline \left\{ \begin{array}{ll} y, & \mathrm{si} \ x \leq y \\ \mathrm{tak}(\mathrm{tak}(x-1,y,z), \mathrm{tak}(y-1,z,x), \mathrm{tak}(z-1,x,y)) & \mathrm{en\ caso\ contrario} \end{array} \right.

La prueba consistirá en comparar los tiempos empleados en calcular tak(n,0,n+1) para n entre 10 y 15.
Read More “Comparación de 3 implementaciones de Common Lisp (Clisp, GCL y SBCL) mediante la función de Takeuchi”