Título: Semántica denotacional para un cálculo-λ relacional
Director: Pablo Barenbaum
Jurado: Alejandro Díaz-Caro y Hernán Melgratti

Resumen:

En esta tesis trabajamos con el cálculo-λU, una extensión del
cálculo-λ que incorpora las características fundamentales de la
programación relacional: alternativa no determinística,
secuenciación explícita, unificación de primer orden e introducción
de variables frescas. Proponemos un sistema de tipos y formulamos una
semántica denotacional para su fragmento tipado. Por semántica
denotacional entendemos a una función [[−]] que dado un programa
devuelve su significado o denotación, es decir, un elemento de algún
dominio de interpretación apropiado. El objetivo es demostrar que la
semántica cumple con propiedades esperables: por un lado, probar la
correctitud de la semántica operacional con respecto a la
denotacional, que asegura que dos programas equivalentes de acuerdo
con una teoría sintáctica de igualdad deben tener la misma
denotación; por otra parte, la propiedad de completitud de la
semántica operacional con respecto a la denotacional, que asegura que
dos programas con la misma denotación se pueden probar equivalentes
en una teoría sintáctica de igualdad. En este trabajo logramos
formular una semántica denotacional para la cual la semántica
operacional verifica una forma débil de correctitud. Queda como
trabajo futuro proponer una semántica denotacional para la cual la
operacional sea correcta y completa.