Semántica denotacional para un cálculo-λ relacional
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 tip...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Tesis de Grado |
| Lenguaje: | Español |
| Publicado: |
2022
|
| Materias: | |
| Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000492_Milicich |
| Aporte de: |
| Sumario: | 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 que la operacional sea correcta y completa. |
|---|