| Support | |
 |
 |
Programación declarativa
Programación basada en restricciones.
En esta línea hemos trabajado en un lenguaje lógico funcional con restricciones, con capacidad de resolver eficientemente problemas que requieren la cooperación de resolutores de restricciones de diferentes dominios, así como en la exploración de nuevas extensiones de la programación declarativa.En concreto, hemos desarrollado un esquema SQCLP(D) para la programación lógica cualificada con restricciones y relaciones de proximidad, que permite manejar información aproximada con un buen nivel de abstracción, en un ambiente declarativo y parametrizado por un dominio de cualificación D. La traslación del mecanismo operacional a una implementación concreta se ha basado en una técnica de transformación de programas que permite, dado un programa SQCLP de alguna de las instancias soportadas por el sistema, transformarlo a un programa objeto CLP semánticamente equivalente que puede ejecutarse sobre sistemas Prolog usuales.Un paso posterior ha consistido en la incorporación de funciones perezosas al esquema, para obtener uno nuevo más general (SQCFLP), si bien hasta el momento solo se han considerado funciones de primer orden. Estos trabajos han sido objeto de la tesis de Carlos Romero (abril 2011).
También hemos conseguido completar el marco teórico para la cooperación de orden superior entre dominios numéricos a través de la integración de una extensión de la lógica de reescritura con restricciones CRWL(D) en el contexto del lambda cálculo con tipos. De forma paralela, el uso de las restricciones se ha abordado mediante la definición de una semántica de punto fijo para el lenguaje "Constraint Handling Rules'" (CHR). Mostramos que la interpretación declarativa de los estados CHR con respecto a un conjunto de reglas de simplificación se puede caracterizar por un punto fijo mínimo sobre el sistema de transición generado por la semántica abstracta operacional de CHR y que la interpretación con respecto a un conjunto de reglas de propagación se puede caracterizar por un punto fijo máximo. Con el fin de modelizar ambos tipos de reglas dentro de una caracterización de punto fijo, presentamos una semántica operacional con restricciones persistentes y mostramos cómo esta semántica se puede caracterizar por dos puntos fijos anidados.
A nivel de implementación, hemos abordado la integración de resolutores industriales (ILOG Solver, Gecode) en un sistema declarativo multiparadigma (TOY), consiguiendo que los procedimientos de backtracking, labeling y propagación explícita del almacén de restricciones del segundo se comuniquen con los primeros. Hemos modelado problemas reales que incluye optimización, "branch & bound" y diferentes estrategias de selección de variables, obteniendo resultados que evidencian incrementos notables de la eficiencia. Y hemos añadido una nueva extensión al entorno Ciao basada en restricciones mediante el sistema de programación lógica con manejo de información borrosa Rfuzzy.
Por otra parte, hemos continuado con el desarrollo de un prototipo para fórmulas de Harrop hereditarias sobre un sistema de restricciones C ---un lenguaje muy expresivo que puede ser utilizado como lenguaje de consulta para bases de datos deductivas. Se han abordado los problemas que surgen con la implementación de diferentes instancias de C, como son dominios finitos o números reales.
Paralelismo, concurrencia y computación distribuida.
Nuestro objetivo ha sido la investigación en profundidad de la semántica de estos conceptos, para su integración bien fundamentada en lenguajes declarativos y en las diferentes herramientas a desarrollar en el programa.Para demostrar la adecuación computacional entre una semántica operacional natural y una semántica denotacional estándar para un lambda cálculo perezoso, Launchbury define una semántica operacional alternativa y una semántica denotacional de recursos. Nosotros hemos inaugurado dos líneas de trabajo para intentar demostrar las equivalencias entre las dos semánticas operacionales y las dos denotacionales. Con respecto a la equivalencia entre las semánticas denotacionales, una se basa en aproximaciones de la primera de forma que ambas semánticas deben ser equivalentes cuando se dispone de infinitos recursos. El estudio de la equivalencia entre la semántica natural, de tipo "call-by-need", y su versión alternativa, de tipo "call-by-name" ha dado lugar, por el momento, a dos trabajos.
También hemos continuado con el estudio de diversos formalismos para la concurrencia y la movilidad, haciendo énfasis en la verificación de los modelos obtenidos. Se han definido variantes de redes de Petri y se han estudiado sus propiedades, y se han comparado entre sí y con otros modelos bien conocidos. Estas ideas teóricas se plasmaron posteriormente en un trabajo más aplicado.
En una línea más aplicada se ha realizado una implementación de un algoritmo novedoso de ejecución paralela en programas lógicos usando paralelismo independiente y "backtracking" en paralelo que permite ejecutar especulativamente ramas de objetivos para avanzar en la generación de soluciones alternativas, lo que permite alcanzar aceleraciones de 5 órdenes de magnitud en 8 procesadores. También hemos desarrollado un nuevo método genérico de paralelización de programas dinámicos con ejecución "top-down" con el que, experimentalmente, se han obtenido aceleraciones muy significativas.
En el campo de la ejecución distribuida, se ha prestado atención a la Computación Orientada a Servicios. Hemos estudiado técnicas para usar información sobre los datos con que se invocan a los servicios para dar una mejor predicción de determinados parámetros de Calidad de Servicio (QoS), usándose para realizar monitorización predictiva y adaptación proactiva así como para organizar tareas y enlaces de datos en workflows en un retículo cuya semántica es definible por el usuario. Por otro lado se ha realizado una caracterizacion de Acuerdos de Nivel de Servicios (SLA) usando restricciones jerárquicas que permiten realizar negociaciones que violen determinadas restricciones. Adicionalmente se ha estudiado la predicción de la eficiencia de una una orquestación fija dependiendo de los recursos usados para su ejecución.
De manera algo independiente a todo lo anterior, también hemos elaborado un trabajo en el que se realiza un modelo del comportamiento de una red P2P que utiliza la tabla hash distribuida Kademlia en el lenguaje de especificación Maude.
Genericidad.
La programación genérica, estudiada inicialmente en el contexto de la programación funcional y recientemente en otros lenguajes como Java, facilita la reutilización y el mantenimiento del software, mediante librerías que pueden aplicarse a diversos tipos de datos. Hemos pretendido incorporar genericidad en los marcos declarativos y herramientas desarrolladas en el programa, al objeto de ofrecer un incremento considerable de concisión y elegancia en los programas. Para ello, hemos estudiado el problema preliminar de la acomodación de estrategias de reducción (mecanismo de computación en lenguajes declarativos) que tengan las propiedades normalizantes y estándar (en el sentido técnico) para términos abiertos o con ligaduras ("binders'"), los cuales son un ingrediente importante y problemático de los lenguajes declarativos lógicos, los basados en reescritura, y los funcionales con tipos dependientes. Hemos descubierto dos estrategias novedosas con dichas propiedades.Actualmente estamos estudiando las diversas propuestas existentes de sistemas de tipos para programación lógica de primer orden que puedan ser utilizables (o extensibles con la mínima complejidad posible) para la implantación de técnicas de programación genérica (fundamentadas en lenguajes tipados).
Asimismo, los miembros de los dos grupos involucrados se han reunido para discutir el estado del arte de la programación genérica funcional y del lenguaje lógico de reescritura Maude, planteando cómo realizar la integración del primero en el segundo e identificado los trabajos científicos a estudiar por ambos grupos.
En el ámbito de los lenguajes lógico-funcionales, hemos propuesto un sistema de tipos que liberaliza el tradicional de Damas-Milner manteniendo sin embargo las propiedades habituales de seguridad del sistema (preservación de tipos durante la reducción, y progreso), y que tiene mucha capacidad para la programación genérica mediante mecanismos muy simples. El sistema ha sido además aplicado a la implementación de clases de tipos en sistemas lógico-funcionales.
