Las dos caras de la moneda de la correspondencia Curry-Howard: demostración y verificación.

Ponente(s): Eduardo Ugalde Reyes, Dr. Favio E. Miranda-Perea

Las dos caras de la moneda de la correspondencia Curry-Howard: demostración y verificación. Eduardo Ugalde-Reyes§§ & Favio E. Miranda-Perea§ La deducción natural y el cálculo lambda son sistemas formales utilizados para representar y manipular pruebas formales como objetos matemáticos. Ambos enfoques persiguen objetivos distintos pero complementarios. Por un lado, la deducción natural ofrece una notación conveniente que facilita la construcción de pruebas y nos permite comprender los mecanismos involucrados en la demostración de teoremas. Por otro lado, el cálculo lambda, a través de la teoría de tipos, captura información relevante sobre las entidades con las que razonamos en un sistema formal, permitiendo abstraer modelos computacionales partiendo de las demostraciones involucradas en una prueba. La correspondencia Curry-Howard establece una conexión fundamental entre la deducción natural intuicionista y la teoría de tipos constructiva. Esta correspondencia nos brinda valiosas intuiciones sobre la íntima relación entre las pruebas y la computación en tres aspectos principalmente: a) la interpretación de las proposiciones como tipos de datos, considerando los tipos como conjuntos constructivos; b) la interpretación de las pruebas formales de proposiciones como programas, donde los términos que habitan los tipos representan las pruebas; y c) el proceso de normalizar las pruebas, considerando intuitivamente esta noción en el sentido de simplificar una prueba o mostrar cómo obtener pruebas directas en contraposición a tener pruebas indirectas, corresponde al procedimiento de reducir o evaluar un programa, llegando así a la interpretación de la normalización de pruebas como evaluación de programas. Al examinar la correspondencia de Curry-Howard y sus resultados formales, surge una doble interpretación de las pruebas. Desde una perspectiva epistémica, las pruebas nos brindan comprensión y explican por qué una proposición demostrada es verdadera. Desde una perspectiva ontológica, las pruebas tienen un contenido computacional que respalda o garantiza dicha afirmación. Esta dualidad puede aprovecharse en ambos sentidos. El conocimiento sobre cómo construir una prueba se puede traducir en un proceso de verificación, a saber evaluando en cada etapa de la prueba si un objeto cumple con las reglas de construcción. A su vez, la información codificada en el proceso de verificación puede ser aplicada para mejorar la construcción de demostraciones, haciéndolas más formales, detalladas y libres de errores. La ventaja de utilizar técnicas basadas en la correspondencia de Curry-Howard radica en que el proceso de verificación de pruebas se simplifica al proceso de razonar dentro de nuestro dominio de conocimiento. De esta manera, descubrir una prueba a través de inferencias válidas es similar a verificar una prueba mediante cómputos correctos.