I1M2018: Razonamiento sobre programas

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de programas Haskell.

Los tipos de razonamiento estudiado son

  • Razonamiento ecuacional sin variables.
  • Razonamiento ecuacional con variables.
  • Razonamiento ecuacional con análisis de casos
  • Razonamiento por inducción sobre los naturales
  • Razonamiento por inducción sobre listas.

En las demostraciones por inducción se ha destacado la elección de variables, las demostraciones anidadas y la generalización de propiedades para su prueba por inducción.

Los apuntes correspondientes a la clase son los del tema 8

Además, se ha mostrado cómo automatizar las demostraciones usando Isabelle/HOL.

I1M2018: Programación dinámica: Apilamiento de barriles

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han resuelto ejercicios de la relación 46, en el que se comparan distintas soluciones del problema del apilamiento de barriles. Se ha mostrado como transformar las definiciones recursivas en definiciones con programación dinámica. Además, se han comparado experimentalmente la eficiencia de las distintas definiciones.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2018: Programación dinámica: Apilamiento de barriles”

Resumen de lecturas compartidas durante mayo de 2019

Esta entrada es una recopilación de lecturas compartidas, durante mayo de 2019, 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 mayo de 2019”