El desafío matemático “Un número curioso” en Haskell

En El País del día 16 se presentó el desafío matemático Un número curios cuyo enunciado es el siguiente:

El equipo que preparamos los desafíos matemáticos hemos decidido abonarnos durante todo el año a un número de la Lotería. Para elegir ese número, que debe estar comprendido entre el 0 y el 99.999, pusimos como condición que tuviese las cinco cifras distintas y que, además, cumpliese alguna otra propiedad interesante. Finalmente hemos conseguido un número que tiene la siguiente propiedad: si numeramos los meses del año del 1 al 12, en cualquier mes del año ocurre que al restar a nuestro número de lotería el número del mes anterior, el resultado es divisible por el número del mes en el que estemos. Y esto sucede para cada uno de los meses del año.

Es decir, si llamamos L a nuestro número, tenemos por ejemplo que en marzo L-2 es divisible entre 3 y en diciembre L-11 es divisible entre 12.

El reto que os planteamos es que nos digáis a qué número de Lotería estamos abonados.

He elaborado una relación de ejercicios (para la asignatura de Informática de 1º del Grado en Matemáticas y para la siguiente versión del libro Piensa en Haskell) en la que se generaliza el problema y se resuelve con Haskell de cuatro maneras distintas. La relación de ejercicios es la siguiente
Read More “El desafío matemático “Un número curioso” en Haskell”

El juego de “tres en raya” en Haskell

El tres en raya es un juego entre dos jugadores que marcan los espacios de un tablero de 3×3 alternadamente. Un jugador gana si consigue tener una línea de tres de sus símbolos: la línea puede ser horizontal, vertical o diagonal.

El objetivo de esta relación de ejercicos es realizar un programa para que la máquina juegue contra el humano el tres en raya usando la estrategia minimax.
Read More “El juego de “tres en raya” en Haskell”

Evaluación en Haskell con tiempo acotado

A veces es interesante evaluar expresiones en Haskell durante un tiempo limitado. Se puede conseguir usando la función timeout de la librería System.Timeout y la evaluate de la Control.Exception.

Vamos a mostrar su uso el siguiente ejemplo. En primer lugar, importamos las funciones

A continuación, definimos la función de Fibonacci

y la función acotada tal que (acotada t f x) calcula (f x) durante t microsegundos (1/10^6 segundos) y devuelve (Just (f x)) si encuentra su valor o Nothing en caso contrario.

Con acotada podemos realizar evaluaciones con tiempo limitado. Por ejemplo,

También se puede acotar con evaluate. Por ejemplo,

Esta entrada se basa en la consulta Haskell time limit on evaluation de StackOverflow.

El problema de Josefo en Haskell

El problema de Josefo hace referencia a Flavio Josefo, un historiador judío que vivió en el siglo I. Según lo que cuenta Josefo, él y cuarenta soldados camaradas fueron capturados por los romanos. Antes que rendirse, decidieron acabar ellos mismos con sus vidas. Para hacerlo, se dispusieron en un círculo y acordaron que irían contando de tres en tres, de forma que cada tercer soldado sería ejecutado por la persona de su izquierda. El último hombre que quedara con vida tendría que suicidarse. Según cuenta la leyenda, Josefo calculó rápidamente cuál sería la posición del último hombre en morir para colocarse allí, y una vez hubieron muerto sus compatriotas, se entregó a los romanos.

El enunciado del problema de Josefo de orden (n,m) es el siguiente: Se tienen n personas entorno a un círculo, ordenadas y numeradas desde la primera a la n-ésima. Empezando por la persona número 1, se saltan m-1 personas y se mata a la m-ésima. A continuación se saltan otras m-1 personas y se ejecuta a la siguiente. El proceso continúa hasta que sólo quede una. El objetivo es, dados n y m, encontrar el lugar inicial en el círculo para sobrevivir.

A continuación muestro una relación de ejercicios (elaborada para la asignatura de Informática de 1º del Grado en Matemáticas y para la siguiente versión del libro Piensa en Haskell) en la que se presentan distintas soluciones y se compara su eficiencia.

Read More “El problema de Josefo en Haskell”

Formal kinematic analysis of the two-link planar manipulator

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre cinemática titulado Formal kinematic analysis of the two-link planar manipulator.

Sus autores son Binyameen Farooq, Osman Hasan, Sohail Iqbal (de la Universidad de Islamabad, Pakistán).

Su resumen es

Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral step of their design. The main idea behind kinematic analysis is to study the motion of the robot based on the geometrical relationship of the robotic links and their joints. Given the continuous nature of kinematic analysis, traditional computer-based verification methods, such as simulation, numerical methods or model checking, fail to provide reliable results. This fact makes robotic designs error prone, which may lead to disastrous consequences given the safety-critical nature of robotic applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving for conducting formal kinematic analysis. As a first step towards this direction, we utilize the geometry theory of HOL-Light to develop formal reasoning support for the kinematic analysis of a two-link planar manipulator, which forms the basis for many mechanical structures in robotics. To illustrate the usefulness of our foundational formalization, we present the formal kinematic analysis of a biped walking robot.

El trabajo se ha presentado en el ICFEM 2013 (15th International Conference on Formal Engineering Methods). Las trasparencias de la presentación se encuentran aquí.

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