I1M2019: Programación dinámica en Haskell

En la clase hoy de Informática de 1º del Grado en Matemáticas se ha explicado cómo transformar definiciones recursivas en otras con programación dinámica y la mejora en eficiencia obtenida con la transformación.

Para la explicación se han elegido 6 ejemplos:

  • Los números de Fibonacci
  • Coeficientes binomiales
  • Longitud de la subsecuencia común máxima
  • Subsecuencia común máxima
  • Distancia de Levenshtein

El estudio de cada uno de los ejemplos ha consistido en

  • Enunciar el problema
  • Definir una solución por recursión.
  • Transformar la definición recursiva en otra con programación dinámica.
  • Comparar experimentalmente la eficencia de las dos definiciones.

La clase se ha dado mediante videoconferencia y el correspondiente vídeo es

Los apuntes correspondientes a la clase son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

Resumen de lecturas compartidas durante abril de 2020

Esta entrada es una recopilación de lecturas compartidas, durante abril de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.

Read More “Resumen de lecturas compartidas durante abril de 2020”

LMF2019: Razonamiento sobre programas con Isabelle/HOL (2º parte)

En la clase de hoy del curso de Lógica matemática y fundamentos se ha concluido el estudio, iniciado en la clase anterior, de cómo se pueden demostrar manualmente propiedades de programas Haskell y cómo traducir dichas demostraciones a Isabelle/HOL.

Para ello, se han usado las transparencias del tema 8 del curso de Informática (de 1º del Grado en Matemática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.

De cada propiedad se han presentados distintas demostracciones:

  • automática,
  • aplicativa estructurada (usando simp)
  • aplicativa detallada (usando simp only)
  • declarativa estructurada (usando simp)
  • declarativa detallada (usando simp only)

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte:

  • Segunda parte:

  • Tercera parte:

Las transparencia utilizadas son las del tema a partir de la página 29.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Razonamiento sobre programas con Isabelle/HOL (2º parte)”

I1M2019: El TAD de los polinomios en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los polinomios y su implementación en Haskell.

Comenzamos la clase analizando las posibles representaciones de los polinomios y, como consecuencia, establecer la signatura y las propiedades del TAD de los polinomios.

A continuación, estudiamos tres posibles representaciones del TAD de los polinomios mediante tipos algebraicos, mediantes listas dispersas y mediante listas densas y sus implementaciones en Haskell

La clase se ha dado mediante videoconferencia y los correspondientes vídeos son

Los apuntes correspondientes a la clase son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.