Pasar al contenido principal

Estructuras algebraicas en Realizabilidad.

Fecha de inicio
Fecha de fin
Resumen:  La realizabilidad proporciona un conjunto general y bien establecido de técnicas para estudiar las relaciones entre programas y pruebas. En la presentación tradicional de la realizabilidad intuicionista, se parte de un conjunto A de realizadores, que son objetos con significado computacional, programas en algún formalismo (códigos de funciones recursivas, términos $\lambda$, etc.). La lógica se interpreta entonces en el conjunto potencia de A (los valores de verdad), de tal manera que el significado de una fórmula es esencialmente un conjunto de programas que comparten un comportamiento computacional dictado por la fórmula. Desde un punto de vista algebraico, el conjunto A induce en su conjunto potencia un álgebra de Heyting. 

La realizabilidad clásica adapta estos principios a la lógica clásica, basándose en instrucciones de control. La parte computacional se basa en la dualidad entre programas (pruebas) y entornos (contrapruebas). La estructura algebraica que subyace a los valores de verdad de la realizabilidad clásica es un tipo particular de álgebra combinatoria ordenada (OCA) inducida por los lenguajes de términos y pilas. 

En una serie de trabajos que involucran a investigadores del IMERL se prueba que tanto la Realizabilidad Intuicionista como la clásica son posibles de definir en OCAs de modo que tanto los valores de verdad como los realizadores pertenecen al conjunto subyacente de estas estructuras y el orden parcial subsume el subtipado, la reducción de términos y la relación de realizabilidad. Todos estos trabajos abogan por fundamentos de realizabilidad que buscan transformar una definición bastante compleja y operativa en una mucho más simple y algebraica.

El estudio de la Realizabilidad para sistemas concurrentes fue iniciado por Beffara en su tesis de doctorado. El lenguaje de realizadores viene dado por una variante de $\pi$-cálculo, que es a la programación concurrente lo que el $\lambda$-cálculo a la programación secuencial. Tal como en la Realizabilidad Intuicionista o Clásica, los valores de verdad en esta presentación son conjuntos de $\pi$-términos. En un reciente trabajo, basándose en las estructuras conjuntivas de Miquey, presentamos una estructura algebraica que permite interpretar tanto a los $\pi$-términos como a las fórmulas matemáticas.  
 

En esta charla intentaremos mostrar una panorámica de las motivaciones y los diferentes contextos en los que estas estructuras aparecen.

 
----------------------------------------------------------------------------------------

Viernes 25/10 a las 11:15
Salón de Seminarios del IMERL y a través de Zoom

Contacto: Dalia Artenstein   darten@fing.edu.uy  Rafael Parra rparra@fing.edu.uy


Información de acceso a Zoom / Zoom access info:

Enlace / link: https://salavirtual-udelar.zoom.us/j/85001311823

ID de reunión / Meeting ID: 850 0131 1823