LMF2019: Razonamiento sobre programas con Isabelle/HOL (1º parte)
En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell y cómo traducir dichas demostraciones a Isabelle/HOL.
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.
La traducción de los enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,
1 |
lemma "longitud (repite n x) = n" |
También se puede poner un nombre al lema, por ejemplo,
1 2 |
lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys" |
De cada propiedad se han presentados distintas demostracciones:
- automática,
- aplicativa estructurada (usando
simp
) - aplicativa detallada (usando
simp only
) - declarativa estructurada (usando
simp
) - declarativa detallada (usando
simp only
)
La clase se ha dado mediante videoconferencia y el vídeo correspondiente a la primera parte es
y el de la segunda parte es
Las transparencia utilizadas son las 28 primeras páginas del tema
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Razonamiento sobre programas con Isabelle/HOL (1º parte)”