Sobre la equivalencia entre semánticas operacionales y denotacionales para lenguajes funcionales paralelos

Abstract

Eden es un lenguaje funcional paralelo que extiende Haskell con construcciones sintácticas para especificar la creación de procesos. En Eden se distinguen dos partes: un lambda cálculo perezoso y expresiones de coordinación. El lenguaje Jauja es una simplificación de Eden que mantiene sus principales características. El objetivo de esta tesis es dar los primeros pasos para demostrar la equivalencia entre las semánticas definidas para Jauja por Hidalgo-Herrero. Se quiere probar la equivalencia en términos de corrección y adecuación computacional entre una semántica operacional y una semántica denotacional. Para hacerlo nos basamos en las ideas expuestas por Launchbury, en el que se demuestra la equivalencia entre una semántica natural y una semántica denotacional estándar para un lambda cálculo extendido con declaraciones locales. Puesto que demostrar la equivalencia entre las semánticas definidas para Jauja supone un estudio demasiado complejo para afrontarlo en un primer paso, hemos comenzado por considerar una extensión del lenguaje utilizado por Launchbury al que se ha añadido una aplicación paralela que da lugar a creaciones de procesos y comunicaciones entre ellos, es decir, a un sistema distribuido formado por distintos procesos que interactúan entre sí. A partir de este sencillo lenguaje el estudio se desarrolla en varias etapas en las que se establece la equivalencia entre distintas semánticas operacionales y denotacionales para modelos distribuidos y no distribuidos. La semántica operacional del modelo distribuido heredada de Jauja es una semántica de paso corto para varios procesadores. Para realizar la equivalencia de esta semántica con una semántica denotacional estándar extendida, con objeto de dotar de significado a la aplicación paralela, se introducen dos semánticas intermedias: una de paso corto pero limitada a un único procesador y una semántica de paso largo que es una extensión de la semántica natural de Launchbury. En el caso de prescindir de las aplicaciones paralelas, la semántica natural de Launchbury y nuestra extensión se comportan igual. Con respecto al modelo no distribuido, y con el fin de completar las demostraciones ausentes en el trabajo de Launchbury, se construye un espacio de funciones para los valores de la semántica denotacional con recursos introducida por el autor. Posteriormente, se comprueba que es equivalente a la semántica denotacional estándar bajo la condición de disponer de infinitos recursos. También se estudian algunas relaciones existentes entre heaps y pares (heap, término) que se aplican para estudiar la equivalencia de las dos semánticas operacionales introducidas por Launchbury. Hemos realizado gran parte del estudio utilizando la notación localmente sin nombres, situada a medio camino entre la de nombres y la de de Bruijn. Así se evitan los problemas derivados de la notación con nombres, es decir, tener que trabajar con términos alfa equivalentes. Por otra parte, también se eluden las desventajas de utilizar solo los índices de de Bruijn, que resultan complicados de manejar y dificultan la lectura de los términos.