I1M2019: El patrón de divide y vencerás en Haskell

En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante divide y vencerás.

La resolución de problemas mediante la técnica de divide y vencerás la
hemos estado utilizando a lo largo del curso en distintos problemas como el de ordenar una lista mediante la ordenación por mezcla o la ordenación rápida.

Analizando estos casos, se extrae el patrón de resolución de problemas mediante divide y vencerás (DyV) que consta de los siguientes pasos:

  • Dividir el problema en subproblemas menores.
  • Resolver por separado cada uno de los subproblemas; si los subproblemas son complejos, usar la misma técnica recursivamente; si son simples, resolverlos directamente.
  • Combinar todas las soluciones de los subproblemas en una solución simple.

Para implementarla, necesitamos funciones que determinen

  • cómo reconocer si el problema es elemental,
  • cómo se resuelven los problemas elementales,
  • cómo se descompone un problema y
  • cómo se combinan las soluciones de los subproblemas.

A continuación se implementa el patrón DyV en Haskell, usando su posibilidad de programar en orden superior para usar las anteriores funciones como argumento

Finalmente, se aplica el patrón DyV para implementar los algoritmos de ordenación por mezcla y ordenación rápida.

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

Los apuntes correspondientes a la clase son la primera sección de

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

LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

  • el razonamiento por casos booleanos,
  • el razonamiento por casos booleanos sobre una variable,
  • el razonamiento por casos sobre listas,
  • el razonamiento por inducción sobre números naturales con patrones,
  • el razonamiento sobre definiciones con existenciales,
  • el uso de librerías auxiliares (como Parity) y
  • el uso de otros métodos de demostración (como presburg).

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

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL”

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”