En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los 3 primeros ejercicios de la relación 9 sobre tipos de dato algebraico.
Los ejercicios y su solución se muestran a continuación
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los primeros ejercicios de la relación 8 sobre árboles binarios definidos como tipo de dato algebraico.
Los ejercicios y su solución se muestran a continuación
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 teoría con los ejemplos presentados en la clase es la siguiente:
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo construir un programa para determinar si una fórmula es una tautología.
Para ello se consideran las siguientes fases:
- definir un tipo de dato algebraico para las fórmulas proposicionales,
- definir un tipo de dato para las interpretaciones,
- definir una función para calcular los valores de las fórmulas en las interpretaciones
- definir una función para generar todas las posibles interpretaciones de una fórmula y
- definir una función que para decidir si una fórmula es tautología (es decir, su valor es verdadero en todas sus interpretaciones).
Los apuntes correspondientes a la clase son
El código correspondiente es
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los primeros ejercicios de la relación 7 sobre funciones de orden superior.
Los ejercicios y su solución se muestran a continuación
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
Como tarea para la próxima clase se ha propuesto resolver de manera colaborativa los ejercicios de la 8ª relación.
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.
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.
La teoría con los ejemplos presentados en la clase es la siguiente:
En la segunda parte de la clase clase de hoy de Informática de 1º del Grado en Matemáticas hemos explicado cómo se instalan librerías de Haskell: en una consola se ejecutan las siguientes órdenes
cabal update cabal install primes |
La primera actualiza la lista de librerías y la segunda instala la librería de números primos. La documentación, con ejemplos, de dicha librería se encuentra aquí
Como ejemplo de uso de la librería hemos resuelto el problema Números libres de cuadrados de Exercitium.
A continuación, hemos comentado las soluciones de los ejercicios de la 6ª relación que trata de funciones sobre cadenas.
Los ejercicios, y sus soluciones, se muestran a continuación:
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado, como aplicación de las funciones de orden superior, la codificación binaria de cadenas y su transmisión.
Los apuntes correspondientes a la clase son los del tema 7
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,
lemma "longitud (repite n x) = n" |
También se puede poner un nombre al lema, por ejemplo,
lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys" |
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: