Reseña: Proof pearl – A mechanized proof of GHC’s mergesort

PorJosé A. Alonso

Se publicado un artículo de verificación en Iabelle/HOL titulado Proof pearl – A mechanized proof of GHC’s mergesort.

Su autor es Christian Sternagel (de la Univ. de la Univ. de Insbruck).

Su resumen es

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art poof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.

La librería estándard de GHC (The Glasgow Haskell Compiler) tiene un algoritmo de ordenación, que es una variante de la ordenación por mezcla. El objetivo del trabajo es la verificación de dicho algortimo en Isabelle/HOL, demostrando su corrección y estabilidad.

La principal característica de este trabajo es la verificación de programas eficientes. El método empleado tiene tres pasos:

  1. formalizar variantes del algoritmo que faciliten la demostración y probar todas las propiedades deseadas;
  2. formalizar variantes eficientes del algoritmo y probar su equivalencia y
  3. usar la generación de código y obtener un programa eficiente del que se tiene garantía que satisface todas las propiedades que se probaron en la formalización inicial.

La formalización es pequeña (menos de 400 líneas de código) y la mayoría de las demostraciones son automáticas. Este éxito se basa en dos principios: la generalización de los conceptos y la definición de esquemas de inducción.

El código en Isabelle/HOL de la teoría correspondiente al trabajo se encuentra en The Archive of Formal Proofs.

Confluence by decreasing diagrams – Formalized

PorJosé A. Alonso

Se ha publicado un trabajo de formalización de sistemas de reescritura en Isabelle/HOL titulado Confluence by decreasing diagrams – formalized.

Su autor es Harald Zankl (de la Universidad de Insbruck, Austria).

Su resumen es

Decreasing diagrams are a complete characterization of confluence for abstract rewrite systems whose convertibility classes are countable. In this paper we present a formalization of decreasing diagrams in the theorem prover Isabelle. The main contribution is a formal proof that any locally decreasing abstract rewrite system is confluent.

Las teorías Isabelle/HOL correspondiente al trabajo se encuentran aquí.

LI2012: Semántica de la lógica proposicional

PorJosé A. Alonso

El objetivo fundamental de la clase de hoy del curso Lógica Informáticaha consistido en responder estas dos preguntas:

  • ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?
  • ¿cómo se puede construir un programa para que dada un conjunto de fórmulas S una fórmula F decida si es consecuencia de S?

Para responder a la primera pregunta, desarrollamos la semántica de la lógica proposicional. En primer lugar, el valor de verdad de una fórmula en una interpretación se define por recursión. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).

Hemos continuado planteando los problemas SAT y TAUT y presentando dos algoritmos para su solución: tablas de verdad y método de Quine.

Además, se han definidos los conceptos de equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y la relación de consecuencia lógica.

Se ha visto la equivalencia de los siguientes problemas

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. 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.

Finalmente, se ha presentado cómo se puede utilizar dos sistemas en la resolución de los anteriores problemas: Gateway to Logic y Prover9/Mace4.

Una implementación en Haskell de la semántica de la lógica proposicional siguiendo el contenido de esta clase se encuentra en el primer capítulo del libro Lógica en Haskell.

Los ejercicios pendientes para la próxima clase son desde el 26 al 37 del capítulo 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 14-34 del tema 1
Read More “LI2012: Semántica de la lógica proposicional”