1. Nombre del proyecto

Especificaciones y programas: modelos de cálculo, tipos e implementaciones

El plan consiste en la definición y la investigación de las propiedades de ciertos cálculos tipados (inspirados del cálculo lambda [Bar85]), que permiten la modelización de la especificación de un problema y del programa que lo resuelve. Nos interesa estudiar propiedades como por ejemplo la confluencia y la normalización: la primera asegura el determinismo del sistema, y la segunda la existencia de un resultado para cada computación.

Si bien en los sistemas tipados todas las computaciones permiten obtener el resultado deseado, es importante definir una estrategia que llegue a este resultado lo más rápido posible. Desde un punto de vista práctico, para obtener una implementación eficiente de estos cálculos, nos proponemos estudiar diferentes estrategias de computación y comparar sus performances. La herramienta que nos servirá de base en este estudio es la Lógica Lineal [Gir87] y sus derivados, como las redes de interacción, que inspiraron la definición de estrategias eficientes (y optimales) en el cálculo lambda gracias a la descomposición en acciones atómicas de cada paso en la computación.

En [Sza97] Nora Szasz presenta una teoría formal de la programación basada en la Teoría Constructiva de Tipos. La principal contribución de este trabajo es que se obtiene una noción de programa más realista que la que existe en las distintas formulaciones de la teoría de tipos pero se mantienen las ventajas que tiene la utilización de dichas teorías, esto es: la unificación de conceptos, el hecho que la verificación de programas se reduce a un control de tipos, y la posibilidad de construir en paralelo los programas y sus pruebas de corrección.
En este proyecto proponemos iniciar el proceso de construcción de un asistente que permita utilizar en la practica la teoría de Nora Szasz. Para ello, las principales etapas son: el estudio de las relaciones entre tipos y normalización, el desarrollo de un algoritmo de control de tipos, y el estudio de estrategias eficientes de reducción utilizando técnicas derivadas de la Lógica Lineal.

5.2. Descripción del proyecto Científico y objetivos perseguidos

Fundamentación y Antecedentes

El proyecto de investigación propuesto se fundamenta en el hecho de que el cálculo lambda es la base teórica de la programación funcional [BW88] y puede ser considerado como un lenguaje de programación abstracto dado que contiene el concepto de cómputo en su forma más pura y general (es equivalente a la máquina de Turing) y además tiene una sintaxis extremadamente simple. Los primeros lenguajes de programación tipados fueron Pascal y Algol, luego aparecieron otros lenguajes como ML, Miranda y Haskell. Estos lenguajes están basados en fragmentos del Sistema F [Gir86], que es un cálculo lambda tipado de segundo orden desarrollado por Girard y Reynolds. La teoría de los cálculos lambda tipados también puede ser pensada desde el punto de vista de la lógica como la teoría de la demostración. En esta perspectiva el estudio de la normalización es el estudio de la simplificación de las demostraciones. Una forma normal es la prueba más simple que se puede encontrar de un teorema. El estudio del chequeo de tipos y de la habitabilidad de tipos corresponde al chequeo de demostraciones y a la deducción automática de la demostración a partir del enunciado del teorema. Los llamados asistentes de demostraciones, que son sistemas que ayudan a la demostración de teoremas matemáticos, están basados en su mayor parte en los cálculos lambda tipados. Algunos de ellos son Coq [Ba97], Lego [LP92], Constructor [HA91], Nuprl [Co86] y Alf [Mag94]. Estos sistemas pueden ser usados en particular para probar que un programa funcional es correcto, es decir, que satisface su especificación. Las propiedades de confluencia y de normalización aseguran la coherencia del sistema de prueba.

En la tesis de doctorado [Sza97], Nora Szasz presentó una Teoría de Especificaciones basada en la Teoría de Tipos de Martin Löf, en la cual es posible construir programas correctos a partir de sus Especificaciones. En [SS99] Paula Severi y Nora Szasz reformularon la Teoría de Especificaciones y comenzaron a estudiar propiedades de dicha teoría como normalización y confluencia de la reducción.

En la tesis de doctorado [Fer93] y en sus trabajos posteriores [BF97,BF95,BBF96], Maribel Fernández realizó estudios de confluencia y normalización para varios cálculos que combinan cálculo lambda (para la definición de funciones de orden superior) y reescritura de términos (para la representación de estructuras de datos y operadores algebraicos). Entre los resultados obtenidos está la modularidad de las propiedades de confluencia y terminación (normalización fuerte) en los fragmentos tipados de estos cálculos. En la tesis de doctorado [Sev96a] y en otros trabajos [SP94,Sev96b,RS95,Sev98,RSSX99] Paula Severi realizó estudios de confluencia y normalización sobre la teoría general de Sistemas Puros de Tipos [Ber88,Ter89,Bar92], así como también estudios de la normalización fuerte en cálculo lambda puro. En la tesis de doctorado [Mac94] y en sus trabajos posteriores [Mac98a,Mac98b] Ian Mackie estudió la implementación del cálculo lambda utilizando redes de interacción, basadas en redes de prueba de la Lógica Lineal, y la Geometría de la Interacción (un modelo semántico de la Lógica Lineal). Ian Mackie y Maribel Fernández [FM99] definieron, basados en estos trabajos, una estrategia de reducción en un cálculo lambda con substituciones explícitas, que tiene todas las ventajas de la llamada reducción débil, pero que permite reducciones dentro de las abstracciones (cosa que la reducción débil no permite), y gracias a esto las reducciones son más eficientes.

Objetivos Generales y Específicos, Resultados Previstos

En [Sza97] se presentó la Teoría de Especificaciones como una extensión a la Teoría de Tipos de Martin Löf, que permite la construcción de programas correctos a partir de sus especificaciones. Una especificación para un programa es una propiedad que el programa debe satisfacer. En general ésta es una proposición que tiene la forma "xÎA. $yÎB. P(x, y). A partir de una prueba p de una proposición de esta forma, la idea es extraer la función f Î A® B tal que P(x, f(x)) se cumpla. La función f será el programa buscado que satisface la especificación. Ya que el existencial en la teoría de conjuntos de Martin Löf es constructivo, el axioma de elección es derivable y es posible construir esta función dada por f = l xÎA. fst(p x). Sin embargo, desde el punto de vista computacional esta función extraída a partir del existencial constructivo no es ni buena ni deseable ya que contiene cierta información redundante y al momento de evaluar f(a) se realizarían cómputos innecesarios.

En la Teoría de Especificaciones se agrega una nueva construcción áxÎA | P(x) ñ llamada par que es en principio similar al existencial. Este par posee propiedades especiales que permiten extraer programas sin información redundante. Para esto, en [SS99] se agrega una reducción o relación de cómputo de manera que la forma normal de un elemento de "xÎA áyÎB| P(x, y) ñ sea un par de la forma áf, qñ donde f es la función deseada de A en B y q es la prueba de "xÎA. P(x, f(x)). De esta manera, es posible construir el programa junto con su especificación y luego al normalizar se separa la parte que corresponde al programa de la parte que corresponde a la prueba de su corrección.

En otros asistentes de pruebas como Coq [Ba97], es posible realizar extracción de programas. El programa extraído en Coq será el mismo que se obtiene por medio de esta reducción. La diferencia está en el hecho que en Coq la extracción se realiza por medio de una función que esta por fuera de la teoría. En cambio, en la Teoría de Especificaciones la extracción de programas se realiza calculando la forma normal de una cierta reducción dentro de la teoría y además es posible obtener tanto la parte del programa f como la prueba de su corrección q.

Paula Severi estudió en su tesis de doctorado las propiedades de normalización de una clase de cálculos tipados, los Sistemas Puros de Tipos (PTS). El estudio de la normalización de un cálculo es importante entre otras razones porque el chequeo de tipos es decidible para aquellos sistemas que son normalizables. En [Sev96b,Sev98] se simplificaron las reglas de los PTS's obteniendo los llamados Sistemas Puros de Tipos Débiles(WPTS); se estudió la propiedad de normalización y se definió un algoritmo de inferencia de tipos para los sistemas puros de tipos usando los sistemas debilitados. La ventaja de este algoritmo es que actúa sobre una clase de sistemas (los PTS's). La prueba de corrección de este algoritmo es delicada por ser un algoritmo general de inferencia de tipos. En el trabajo del proyecto PEDECIBA Una Sistema de Tipos para un Lenguaje Funcional con Constantes Polimorficas, Paula Severi definió un algoritmo de inferencia de tipos para un cálculo lambda tipado particular; se probó su corrección y se llevó a cabo su implementación.

Maribel Fernández estudió las propiedades de normalización de extensiones de los sistemas del cubo de Barendregt (que incluye l P y el Cálculo de Construcciones) con reglas de reescritura de términos arbitrarios. Utilizando la técnica de los Predicados de Reductibilidad de Girard, que es equivalente al uso de conjuntos saturados, se demostró en [BFG97] que todos estos sistemas son fuertemente normalizantes si las reglas de reducción agregadas tienen una forma particular, llamada esquema general de recursión. Este resultado también es válido en sistemas de tipos implícitos, como el sistema de tipos intersección (originalmente definido para el cálculo lambda [CDC80]), y extendido a combinaciones de cálculo lambda y reescritura en [BBF96]. En particular, el sistema intersección permite la caracterización por medio de tipos de los conjuntos de términos fuertemente normalizantes, y que tienen una ``head-normal-form'', es decir, que la raíz del término es estable luego de un cierto número de pasos de reducción.

Otro objetivo de este trabajo es el estudio comparado de diferentes estrategias de reducción en la Teoría de Especificaciones, un paso hacia la implementación de la teoría. Para expresar estrategias, es importante que todas las etapas de cómputo sean descriptas de manera explícita en el sistema. Esto es posible por ejemplo utilizando los llamados cálculos de substituciones explícitas. El cálculo definido por Maribel Fernández e Ian Mackie [FM99] permite también la representación explícita del manejo de recursos (duplicación y borrado). Existe una correspondencia entre la reducción en este sistema, y la reducción en un sistema de redes de interacción en el cual los términos se representan por medio de grafos. Actualmente se dispone de varias implementaciones (secuenciales y paralelas) [Pin00] de las redes de interacción.

Las redes de interacción, derivadas de las redes de prueba de la Lógica Lineal, permiten la codificación del algoritmo de reducción optima en el cálculo lambda [GAL92], y la definición de estrategias eficientes de reducción [Mac98b]. Estos resultados fueron obtenidos para un cálculo lambda con un sistema de tipos simples. La extensión de estos resultados a sistemas de tipos como F o lP es el punto de partida para el estudio de estrategias de reducción eficientes en la Teoría de Especificaciones.

Finalmente, en programación funcional, las definiciones de tipos recursivos o inductivos juegan un papel esencial. Una extensión posible de la Teoría de Especificaciones consiste en agregar una noción de tipo inductivo general [CP90,Ore92,Dyb93] a estos sistemas de tipos y ver su comportamiento con los pares. Este es un objetivo a largo plazo.

Actividades de Formación

• Presentar en tres ejemplares.