I1M2012: El problema de las números bonitos y números feos en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la solución con Haskell el desafío matemáticos Números bonitos, números feos publicado en EL PAÍS con motivo del sorteo de la Lotería de Navidad. Su enunciado es

Desde el año 2011 en la Lotería Navidad se sortean los premios entre los cien mil números que van del 00000 al 99999 (en los décimos los números siempre se escriben con cinco cifras). Aunque todos los números tienen exactamente las mismas posibilidades de resultar premiados, con frecuencia se habla de números bonitos y números feos. Como es una valoración estética, que un número sea bonito o feo depende de los gustos de cada uno.

En este caso un número de lotería nos parecerá bonito si cumple
exactamente una, y solamente una, de estas tres condiciones:

  • a) es divisible entre 5,
  • b) da resto 2 al dividirlo entre 7,
  • c) la suma de sus cifras es divisible entre 9.

Por ejemplo, el 00037 es bonito porque cumple la condición b pero no las otras dos; sin embargo, el 00324 es feo, ya que cumple las condiciones b y c. De igual forma, podríamos decir que el 00041 y el 00450 son horribles. El primero, porque no cumple ninguna de las tres condiciones; y el segundo, porque es un exagerado y cumple las tres.

El desafío que se propone es decidir cuántos de los números que participan en el sorteo de Lotería de Navidad (recordad, del 00000 al 99999) son bonitos según el criterio expresado anteriormente.

A continuación, se presentan 5 soluciones en Haskell y se comparan sus eficiencias.
Read More “I1M2012: El problema de las números bonitos y números feos en Haskell”

I1M2012: Ejercicios de definiciones por recursión y comprensión en Haskell (6)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios 9 a 12 de la 11ª relación en las que se presentan ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2012: Ejercicios de definiciones por recursión y comprensión en Haskell (6)”

DAO2012: Razonamiento sobre programas con Isabelle

En la sesión de hoy del seminario Demostración asistida por ordenador (DAO2012) se ha presentado cómo se puede demostrar con Isabelle propiedades de programas.

En el tema 8 del curso de I1M vimos cómo se puede razonar sobre programas funcionales. Hoy hemos visto cómo Isabelle puede hacer automáticamente las demostraciones de dicho tema. Los métodos que hemos usado son

  • simplificación (con simp),
  • automático (con auto),
  • inducción sobre números naturales y listas (con induct),
  • inducción con variables libres (con arbitrary) y
  • inducción en varias variables (con induct rule).

La teoría correspondiente a la clase es T3_Razonamiento_sobre_programas.thy cuyo contenido se muestra a continuación
Read More “DAO2012: Razonamiento sobre programas con Isabelle”

I1M2012: Ejercicios de definiciones por recursión y comprensión en Haskell (5)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios 6 a 8 de la 11ª relación en las que se presentan ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2012: Ejercicios de definiciones por recursión y comprensión en Haskell (5)”

LI2012: Formas normales de Skolem y cláusulas

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que no tenga cuantificadores, que esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.

Las transparencias de esta clase son las del tema 10
Read More “LI2012: Formas normales de Skolem y cláusulas”