Traducción de pruebas lineales en pruebas diagramáticas: normalización fuerte del cálculo lambda con tipos simples y la lógica minimal

Ponente(s): Eduardo Ugalde Reyes, FAVIO EZEQUIEL MIRANDA PEREA

En la teoría de la prueba podemos observar dos enfoques que en su desarrollo se encuentran presentes: La teoría estructural de la prueba y la teoría interpretativa de la prueba. En esta charla se echará mano de ambos enfoques al hablar sobre la estrecha relación entre derivabilidad en deducción natural y computabilidad en el cálculo lambda a través de la correspondencia Curry-Howard. Nos centraremos en los avances de nuestra investigación que atañen a la reconstrucción formal de la prueba de normalización fuerte de Joachimski & Matthes 2003. La prueba original fue presentada para el cálculo lambda con tipos simples y otros sistemas, pero la reconstrucción que ofrecemos corresponde al fragmento implicacional positivo de la lógica minimal en deducción natural y está guiada por la siguiente pregunta: ¿Cuál es la relación entre el pensamiento diagramático en deducción natural y el razonamiento algebraico en el cálculo lambda? Nuestro interés está en ofrecer una prueba que concilie. Esta conciliación busca cerrar la brecha entre el alto nivel de abstracción y complejidad argumentativa del cálculo lambda y el nivel más intuitivo que nos proporciona la deducción natural al analizar la estructura de pruebas manipulándolas como diagramas.