I1M2019: Funciones de orden superior en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se han estudiado las funciones de orden superior.

En primer lugar, se han estudiado las funciones de procesamiento de listas (map y filter).

En segundo lugar, se ha estudiado cómo puede abstraerse los esquemas definición de funciones de recursión sobre listas mediante la función de plegado (foldr) y cómo con dicha función puede simplificarse la definición de funciones.

A continuación se ha visto cómo definir funciones con acumuladores y cómo simplificarlas con el patrón de plegado por la izquierda (foldl).

Finalmente, se ha visto cómo puede simplificarse la definición de funciones usando el operador de composición.

Los apuntes correspondientes a la clase son las 5 primeras secciones del tema 7

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

Por último, se ha comentado el blog de ejercicios (Exercitium)

  • Cada día, de lunes a viernes, se propone a las 7:00 un ejercicio.
  • Los ejercicios están clasificados por niveles: inicial, medio y avanzado (como resultado de las puntuaciones que reciban).
  • Se pueden escribir las soluciones en los comentarios.
  • Usar como nombre de usuario el UVUS.
  • El código se debe escribir entre una línea con <pre lang=”haskell”> y otra con </pre>
  • Sólo publicar soluciones distintas de las publicadas.

RA2019: Razonamiento sobre programas con Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la 1ª relación.

En la segunda parte, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. 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.

A continuación se ha explicado cómo demostrar automáticamente las propiedades anteriores con Isabelle/HOL.

El enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,

También se puede poner un nombre al lema, por ejemplo,

La demostración es la palabra by seguida por el método de demostración. Los métodos que hemos usado son

  • by simp: que es el método de simplificación por reescritura,
  • by (induct x) auto: que es por inducción en x (donde x es un número natural o una lista) y simplificación automática de ambos casos,
  • by (induct rule: fn.induct) auto: que es por inducción según la definición de la función fn y simplificación automática de todos los casos,
  • by (simp add: lema_auxiliar): que es el método de simplificación por reescritura añadiéndole a las reglas de reescritura la correspondiente al lema_auxiliar,

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2019: Razonamiento sobre programas con Isabelle/HOL”

I1M2019: Ejercicios auto-corregidos con Kattis

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha explicado cómo trabajar con un juez en línea. El juez elegido es [Kattis]](https://open.kattis.com) y la explicación se ha basado en la Guía de uso de Kattis.

En la segunda clase se ha resuelto en el laboratorio los ejercicios de la primera sesión con Kattis y se ha dejado pendiente la resolución de los ejercicios de la 6ª relación.

Resumen de lecturas compartidas durante octubre de 2019

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