I1M2019: Definiciones de tipos en Haskell

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha visto

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando data y
  • cómo definir tipos de datos recursivos usando como ejemplo los naturales, las listas y los árboles.

Se ha insistido en la metodología de definición de funciones recursivas sobre tipos de datos escribiendo una ecuación por cada uno de los constructores del tipo de dato.

Los apuntes correspondientes a la clase son las tres primeras secciones del tema 9

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

Como tarea para la próxima clase se ha propuesto

RA2019: Razonamiento estructurado sobre programas con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL de forma estructurada con Isar.

Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.

Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

Se ha usado Isabelle para analizar detalladamente las demostraciones
poniendo de relieve los lemas usados en cada paso. Para encontralos se
ha empleado la búsqueda de teoremas (con find_theorems) y la traza
(con using [[simp_trace]]).

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

RA2019: Ejercicios de razonamiento sobre programas en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 2ª relación de ejercicios de razonamiento sobre programas. Para cada propiedad se dan dos demostraciones en Isabelle/HOL: la primera automática y la segunda aplicativa detallando los pasos.

La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2019: Ejercicios de razonamiento sobre programas en Isabelle/HOL”