Demostración interactiva de teoremas: teoría y práctica

Beta Ziliani,Universidad de Saarland & Max Planck Institute for Software Systems, Germany.

"Errare humanum est" reza un viejo y sabio proverbio. Y sin embargo, las ciencias exactas, como la computación y la matemática, basan su mecanismo para validar demostraciones en falibles revisores humanos quienes, en algunos casos, deben verificar cientos de páginas de pruebas. Es por ello que en los últimos tiempos ha crecido la atención hacia el uso de la computadora para validar dichos teoremas, siendo el mejor ejemplo la compleja demostración del teorema "de los cuatro colores" conducida en el demostrador interactivo de teoremas Coq. En este curso voy a introducir el demostrador Coq desde la teoría y la práctica, con especial énfasis en la relación entre pruebas y programas. La práctica incluirá ejemplos de laboratorio que los participantes deberán demostrar, es decir, ¡programar! Finalmente se discutirá el estado del arte sobre cómo automatizar las demostraciones para que sean comparables en tamaño y complejidad a la demostración en papel.

Temario:

El curso será dictado en castellano. Se asume familiaridad con programación funcional (ej. Haskell) y se recomienda tener nociones básicas de lambda cálculo. El curso está diseñado para alternar sesiones teóricas con sesiones prácticas en laboratorio, en donde los participantes podrán realizar sus primeros pasos en el demostrador interactivo Coq.

• Breve presentación de la teoría de la demostración y del demostrador interactivo de teoremas Coq. Su lugar en la verificación formal de sistemas y teoremas matemáticos.
• Teoría: Cálculo proposicional de deducción natural. Reglas, ejemplos, y teoremas básicos (substitución, debilitamiento, contracción local).
• Laboratorio: Demostración de teoremas proposicionales en Coq.
• Teoría: Lambda cálculo. Correspondencia de Curry-Howard.
• Laboratorio: Inspección de "proof terms".
• Teoría: Cálculo de primer orden de deducción natural. Reglas, ejemplos, y teoremas básicos.
• Laboratorio: Demostración de teoremas de primer orden en Coq.
• Laboratorio: Tipos inductivos e inducción estructural.
• Laboratorio: Puntos fijos y su relación con la inducción estructural.
• Teoría: Lambda cálculo con puntos fijos. No terminación e inconsistencia.
• Automatización de demostraciones: proof search, Ltac, automatización tipada.

Bibliografía básica:

• Y. Bertot and P. Castéran: Interactive Theorem Proving and Program Development, Springer, 1998.
• The Coq Development Team: Coq Reference Manual, INRIA, 2012, http://coq.inria.fr/refman/
• P. Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Lecture notes, 1996, http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf
• F. Pfenning: Automated Theorem Proving, Chapter 2, 2004, http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf

Bibliografía avanzada:

• G. Gonthier: Formal Proof---The Four-Color Theorem. En Notices of the AMS, 2008.
• D. Delahaye. A Tactic Language for the System Coq. En proceedings of LPAR '00.
• B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, y V. Vafeiadis. 2013. Mtac: A Monad for Typed Tac- tic Programming in Coq. En Proceedings of ICFP '13.