Secciones
Usted está aquí: Inicio Biblioteca Tesis de Grado y Posgrado Tesis de posgrado Tesis de Doctorado Realizabilidad clásica y efectos de borde

Etienne Miquey (2017)

Realizabilidad clásica y efectos de borde

Tesis de Doctorado, PEDECIBA, UdelaR, Université Sorbonne Paris Cite.

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á divido en tres partes, la primera constituyendo una introducción detallada a los conceptos y herramientas involucrados. La secunda 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 ω 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 ω , de la cual depende la coherencia del sistema. Semejante prueba es difícil de conseguir, debido a la presencia simultanea 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 → 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 λμ μ-cria 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 λμ μ-c ́ está demostrada por gracias a una traducción CPS que toma las dependencias en cuenta. Por último, introducimos una variante de dPA ω 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 esta centrada en el estudio de las estructuras algebricas 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 algebrica 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 λ-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 disjunctivas, centradas en el “par” de la lógica linear (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).