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”

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”

Programas compactos para calcular pi con la fórmula de Leibniz

PorJosé A. Alonso

En artículos anteriores hemos comparado la eficiencia de programas en distintos lenguajes. En este vamos a comparar la simplicidad de los programas para resolver un problema.

Como ejemplo he elegido el problema del cálculo compacto del número \pi mediante la fórmula de Leibniz


<br /> \pi = 4 \times \left(1 - \dfrac{1}{3} + \dfrac{1}{5} - \dfrac{1}{7} + \dots\right)<br />

El enunciado de problema es el siguiente

Escribir un programa, con el menor número posible de caracteres, para calcular el número \pi usando la fórmula de Leibniz con un error menor que 0.00001.

El problema se ha planteado en Code Golf: Leibniz formula for Pi y se han escrito distintas respuestas que resumo al final del artículo. Antes voy a presentar programas compactos en nuestros lenguajes habituales (Haskell, Maxima y Common Lisp).

Read More “Programas compactos para calcular pi con la fórmula de Leibniz”

Trabajo de Lógica Computacional en Saarbrücken (Alemania)

PorJosé A. Alonso

El Grupo de automatización de la Lógica (del Instituto Max Planck en Saarbrücken, Alemania) ha publicado un anuncio de ofertas de plazas.

La investigación del grupo se centra en la deducción automática en fragmentos de la lógica de primer orden.

Desde el punto de vista teórico trabajan en el desarrollo, análisis y combinación de cálculos lógicos.

Desde el punto de vista práctico trabajan en la implementación de demostradores automáticos de teoremas y otros sistemas deductivos y su aplicación a la verificación asistida por computador de software y hardware.

Algunos de los sistemas que desarrolla el grupo son SPASS, SPASS+T y Waldmeister

Más novedades de la Competición de IA de Google 2010

PorJosé A. Alonso

Como comenté en la entrada en la que anunciaba la Competición de IA de Google 2010, estaba previsto posibilitar la programación del juego en Haskell, Common Lip.

En la entrada anterior anuncié el soporte del juego en Haskell

En Common Lisp Starter Package se ha publicado el soporte del juego en Common Lisp.

Como la competición se celebrará del 10 de Septiembre al 27 de Noviembre, pienso que puede ser un reto que se le plantee a los alumnos de la asignatura de Inteligencia Artificial el primer día de clase. Incluso se puede fomentar la participación puntuando los resultados obtenidos en la competición.