Realizabilidad clásica y efectos de borde -Etienne Miquey (2017)

Esta tesis se enfoca en el contenido calculatorio de las pruebas clásicas, particularmente en las pruebas con efectos de borde y en la realizabilidad clásica de Krivine. El manuscrito está dividido en tres partes, la primera constituyendo una introducción detallada a los conceptos y herramientas involucrados. La segunda parte se concentra en el contenido calculatorio del axioma de elección dependiente en lógica clásica. Este trabajo se inscribe en la continuidad del sistema \(dPA ^{\omega} \) de Hugo Herbelin, que permite adaptar la prueba constructiva del axioma de elección en la teoría de tipos de Martin-L ̈of en una prueba constructiva del axioma de elección dependiente en un marco compatible con la lógica clásica. El objetivo principal de esta parte es la demostración de la propiedad de normalización para \(dPA^{\omega}\) , de la cual depende la coherencia del sistema. Semejante prueba es difícil de conseguir, debido a la presencia simultánea de tipos dependientes (para la parte constructiva de la elección), de operadores de control (para la lógica clásica), de objetos coinductivos (para “codificar” una función del tipo \( \mathbb{N} \rightarrow A \) mediante el flujo de sus valores \((a_0, a_1, . . . ) \) ) y de evaluación perezosa (para esos objetos coinductivos). En una primera etapa, las dificultades están estudiada separadamente. En particular, demostramos la cálculo con memo- normalización del call-by-need clásico (presentado como una extensión del \( \lambda \mu \hat{\mu} \)- cálculo con memoria compartida) usando técnicas de realizabilidad. Desarrollamos después un cálculo de los secuentes cálculo, cuya corrección clásico con tipos dependientes, definido otra vez como una extensión del \( \lambda \mu \hat{\mu} \) cálculo está demostrada por gracias a una traducción CPS que toma las dependencias en cuenta. Por último, introducimos una variante de \(dPA^{\omega} \) en cálculo de los secuentes que combina los dos sistemas anteriores. Su normalización está finalmente demostrada usando técnicas de realizabilidad. La última parte está centrada en el estudio de las estructuras algebraicas de los modelos inducidos por la realizabilidad clásica. Este trabajo está basado en la noción de álgebras implicativas de Alexandre Miquel, una estructura algebraica muy sencilla generalizando al mismo tiempo las álgebras completas de Boole y las álgebras de realizabilidad de Krivine, de tal forma que se puede expresar en un mismo marco la teoría del forcing (de Cohen) y la teoría de la realizabilidad clásica (de Krivine). El defecto principal de esas estructuras es que son profundamente orientadas hacia el \( \lambda \)-cálculo, y que solamente permiten una interpretación fiel de lenguajes en call-by-name. Para remediar a ese problema, introducimos dos variantes de las álgebras implicativas: las álgebras disyuntivas, centradas en el “par” de la lógica lineal (pero en un marco non-linear) y naturalmente adaptadas para lenguajes en call-by-name; y las álgebras conjunctivas, centradas en el tensor ⊗ de la lógica linear y adaptadas para lenguajes en call-by-value. Entre otras cosas, demostramos que las álgebras disjunctivas son casos particulares de las álgebras implicativas y que las álgebras conjunctivas pueden ser obtenidas por dualidad desde álgebras disjunctivas (invirtiendo el orden subyacente). Además, mostramos cómo interpretar en esos marcos los fragmentos del sistema L de Guillaume Munch-Maccagnoni’s correspondiendo al call-by-value (en las álgebras conjunctivas) y al call-by-name (en las álgebras disjunctivas).