I1M2015: El TAD (tipo abstracto de datos) de las tablas en Haskell

En la segunda parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.

Una tabla es una colección de elementos (valores) a los que se accede mediante sus índice.

Se ha seguido el mismo patrón que en los anteriores tipos de datos:

  • elección de las operaciones básicas,
  • especificación de sus propiedades,
  • implementación en Haskell mediante funciones,
  • implementación en Haskell mediante listas de asociación,
  • implementación en Haskell mediante matrices,
  • análisis de la complejidad de las definiciones de las operaciones básicas en las tres implementaciones y
  • verificación con QuickCheck de sus propiedades características.

Las transparencias usadas en la clase son las del tema 18.

Read More “I1M2015: El TAD (tipo abstracto de datos) de las tablas en Haskell”

LMF2016: Deducción natural proposicional en Isabelle/HOL (2)

En la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la formalización en Isabelle/HOL de las demostraciones por deducción natural estudiadas en el tema 2 iniciado en la clase anterior.

Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y automática.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2016: Deducción natural proposicional en Isabelle/HOL (2)”