Semánticas formales para un lenguaje funcional paralelo

Resumen

El objetivo del trabajo es definir semánticas formales para un lenguaje que contiene las principales características del lenguaje funcional paralelo Eden, extensión del lenguaje funcional perezoso por excelencia, Haskell, pues Eden permite definir esquemás genéricos de proceso y crear dinámicamente ejemplares a partir de los mismos. Así como Eden presenta paralelismo explícito, la comunicación es, en cambio, implícita. En cuanto a la introducción del no-determinismo, es explícita y se limita a la invocación de un proceso predefinido. Estas características las hemos incluido en un lenguaje más simple, Jauja, y hemos precedido a definir semánticas formales para este último. La primera semántica tratada es la operacional, con un nivel de abstracción separado de las particularidades de cualquier máquina virtual. Nos dirigimos hacia enfoques basados en la semántica natural de Launchbury, como la semántica operacional que Baker-Finch y otros defnieron para el lenguaje funcional paralelo GpH (Glasgow Parallel Haskell), también definido sobre Haskell pero empleando paralelismo semi-explícito. Para Jauja extendemos este modelo operacional para poder representar proceso. A partir de la semántica operacional construida, se definen medidas para estudiar la eficiencia de los programas, sobre si la introducción del paralelismo ha sido fructífera o no. Pensando en un usuario del lenguaje, hemos definido una semántica denotacional que refleja los resultados de la evaluación sin bajar tanto el nivel de abstracción. No obstante, el modelo denotacional elegido no es una semántica denotacional directa, sino un modelo denotacional de continuaciones para poder expresar la pereza de Jauja y los posibles efectos laterales producidos como resultado de la evaluación de una expresión: creación de procesos y comunicaciones subyacentes. La consideración de estos efectos laterales estará implícita en una continuación. El trab