RA2014: Razonamiento sobre tipos recursivos en Isabelle/HOL

En la tercera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado

  • cómo definir árboles binarios en Isabelle/HOL y cómo demostrar sus propiedades,
  • cómo definir y razonar con funciones recursivas que no son primitivas recursivas y
  • cómo definir y razonar con tipos de datos mutuamente recursivos.

La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2014: Razonamiento sobre tipos recursivos en Isabelle/HOL”

I1M2014: Evaluación perezosa en Haskell

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la evaluación perezosa en Haskell. Se han visto la estrategias de evaluación perezosa e impaciente, se han comparado respecto de la terminación y el número de pasos necesarios en las computaciones, se ha aplicado a la computación con estructuras infinitas y se han visto casos en los que se aumenta la eficiencia con evaluación estricta.

Como ejemplo, se ha estudiado el cálculo de los números primos mediante la criba de Erastótenes.

Las transparencias usadas en la clase son las del tema 10
Read More “I1M2014: Evaluación perezosa en Haskell”

I1M2014: Problemas de Exercitium

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han comentado las soluciones de los primeros problemas propuestos en Exercitium:

  1. Divisibles por el primero.
  2. Listas equidigitales.
  3. Elementos no repetidos.
  4. Parte impar de un número.
  5. Mayúscula inicial.
  6. Máximo de una función.
  7. Suma de todos los anteriores.
  8. Rompecabeza matemático.
  9. Distancia de Hamming.
  10. Extensión de un fichero.
  11. Precio total.