Estructuras algebraicas en Realizabilidad.

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.