I1M2013: Ejercicios con tipos de datos algebraicos en Haskell
En las clases de ayer y hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de los ejercicios sobre tipos de datos algebraicos en Haskell de la relaciones 18 y 19.
En la relación 18 se consideran abreviaturas y dos tipos de datos algebraicos: los números naturales (para los que se define su producto) y los árboles binarios, para los que se definen funciones para calcular:
- los puntos más cercanos,
- la ocurrencia de un elemento en el árbol,
- el número de hojas,
- el carácter balanceado de un árbol y
- el árbol balanceado correspondiente a una lista.
En la relación 19 se plantean ejercicios sobre árboles binarios. En concreto, se definen funciones para calcular:
- el número de hojas de un árbol,
- el número de nodos de un árbol,
- la profundidad de un árbol,
- el recorrido preorden de un árbol,
- el recorrido postorden de un árbol,
- el recorrido preorden de forma iterativa,
Los ejercicios, y sus soluciones, se muestran a continuación. Los de la relación 18 son
Read More “I1M2013: Ejercicios con tipos de datos algebraicos en Haskell”
Coinitial semantics for redecoration of triangular matrices
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Coinitial semantics for redecoration of triangular matrices.
Sus autores son Benedikt Ahrens y Régis Spadotti (del IRIT, Université Paul Sabatier).
Su resumen es
Infinite triangular matrices and, in particular, the redecoration operation on them, were studied by Matthes and Picard. In their work, redecoration is characterized as the cobind operation of what the authors call a “weak constructive comonad”.
In this work, we identify weak constructive comonads as an instance of the more general notion of relative comonad. Afterwards, building upon the work by Matthes and Picard, we give a category-theoretic characterisation of infinite triangular matrices—equiped with the canonical bisimulation relation and a compatible comonadic cobind operation—as the terminal object in some category.
El código de las correspondientes teorías en Coq se encuentra aquí.
LMF2014: Sintaxis y semántica de la lógica proposicional
En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la sintaxis y la semántica de la lógica proposicional.
Se ha presentado la sintaxis de la lógica proposicional. Concretamente,
- el lenguaje de la lógica proposicional,
- la definición recursiva de las fórmulas proposicionales,
- árboles de análisis de fórmulas,
- definiciones por recursión sobre fórmulas y
- demostraciones por inducción sobre fórmulas.
En la semántica, los conceptos definidos son los valores de verdad, las funciones de verdad, las interpretaciones, el valor de verdad de las fórmulas respectos de las interpretaciones, los modelos de fórmulas, la clasificación semántica de fórmulas (satisfacibles, insatisfacibles, tautologías, contradictorias y contingentes), los problemas SAT y TAUT. Finalmente, se han visto dos algoritmos para la solución de los problemas SAT y TAUT: tablas de verdad y método de Quine.
Otros conceptos definidos son equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y consecuencia lógica.
Se ha demostrado la equivalencia de los siguientes problemas
- decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
- decidir si una fórmula es una tautología,
- decidir si una fórmula es insatisfacible y
- decidir si un conjunto de fórmulas es inconsistente.
Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos. En la solución del rompecabezas se ha explicado el uso del Gateway to Logic.
Las transparencias de estas clases son las del tema 1
Read More “LMF2014: Sintaxis y semántica de la lógica proposicional”
Proof-by-instance for embedded network design
Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Proof-by-instance for embedded network design.
Sus autores son
- Marc Boyer (de ONERA – The French Aerospace Lab, Toulouse, France),
- Loïc Fejoz (de RealTime-at-Work, Nancy, France) y
- Stephan Merz (Inria & LORIA, Nancy, France).
Su resumen es
Proof-by-instance is a technique that ensures the correctness of the results of a computation rather than proving correct the tool carrying out the computation. We report here on the application of this idea to check the computations relevant for analyzing time bounds for AFDX networks. We have demonstrated the feasibility of the approach by applying a proof-of-concept implementation to an AFDX network of realistic size, and we outline the roadmap towards a mature industrial toolset. This approach should lead to a reduction of the time and cost of developing analysis tools used in the design of embedded networks where certification is mandatory.
El trabajo se presentó el 6 de febrero en el ERTS² 2014 Embedded Real Time Software And Systems.