Diseño, semántica y especificación de Babel : un lenguaje que integra la programación funcional y lógica

RESUMEN El interés no puramente académico de los lenguajes de programación declarativos (es decir, funcionales y lógicos) se ha incrementado enormemente desde que la tecnología VLSI ha demostrado las posibilidades reales de construir máquinas paralelas capaces de ejecutar programas declarativos eficientemente. También el creciente progreso actual de las técnicas de implementación en máquinas convencionales también ha ayudado a despertar el interés por esta clase de lenguajes. Además hay una serie de razones intrínsecas al estilo de programación asociado a estos lenguajes para favorecer su utilización. Ni PROLOG ni los lenguajes funcionales disfrutan de todos los beneficios de la programación declarativa. Durante los últimos años se han realizado una serie de intentos para diseñar lenguajes de programación declarativos que integren los paradigmas funcional y lógico. La consecución de esta integración es algo muy deseable, ya que el lenguaje resultante podría explotar ampliamente las facilidades de la lógica (funciones, predicados e igualdad), permitiendo a sus usuarios usarlas separadamente o mezclarlas de la forma más apropiada para una aplicación en particular. En esta tesis se presenta y estudia el lenguaje de programación experimental BABEL, designado para conseguir la integración de la programación funcional (como la usada en HOPE, Standard ML o MIRANDA) y la programación lógica (como la usada en PROLOG) de una forma simple, flexible y matemáticamente bien fundamentada. El lenguaje sigue una disciplina de constructores, muy adecuado para acomodar términos PROLOG y patrones tipo HOPE. Desde el punto de vista sintáctico, BABEL combina PROLOG puro con una notación funcional sin tipos ni funciones de orden superior. Por otro lado, el lenguaje usa "narroving" como base para una semántica de reducción perezosa, que incluye tanto reescritura como resolución SLD, soportando cómputos con estructuras de datos potencialmente infinitas. Hay también una semántica declarativ basada en dominios de Scott, que aporta una noción de mínimo modelo de H brand para los programas BABEL. Se desarrollan ambas semánticas probando resultados de corrección y completitud estableciendo la esperada equivalencia entre ambas. También se ilustran las características del lenguaje a través de numerosos ejemplos de programación. Se ha argumentado que la implementación del "narroving" no es una tarea fácil y que sería mejor reducirlo a resolución SLD para aprovechar las técnicas de implementación conocidas para PROLOG. Nuestra idea es que se pueden usar las muy eficientes técnicas existentes para los lenguajes funcionales. Se ha diseñado una extensión de una máquina funcional por de reducción de grafos, con facilidades para manejar backtracking y unificación siguiendo las ideas de la máquina abstracta de Varren para PROLOG. De esta forma, se obtiene una máquina abstracta para "narroving" para una versión secuencial e "innermost" de BABEL. Pensamos que nuestra aproximación permite realizar implementaciones eficientes del lenguaje. Objeto de un trabajo futuro será el desarrollo de versiones perezosas y paralelas del prototipo actual. El trabajo también incluye un interprete PROLOG para BABEL. ABSTRACT The non purely academic interest for declarative (that is, functional and logical) programming languages has greatly increased since VLSI technology has opened the realistic possibility to built parallel machines capable to execute declarative programs efficiently. Current progress in the improvement of the implementation techniques on conventional machines has also helped to vake up interest. Moreover, there are several intrinsic reasons to favour declarative languages. Neither PROLOG ñor the functional languages enjoy all the benefits of declarative programming. During the last years, several attempts have been ade to design declarative programming languages integrating the functiona and logical paradigms. To achieve such an integration is a highly desirable , ;al, since the resulting languages vould fully exploit the facilities of logic (functions, predicates and equality) and allov their users to keep them sepárate or to mix them in the vay that best suits to a particular application. In this thesis ve investigate the experimental programming language BABEL, designed to achieve integration of functional programming (as embodied in HOPE, Standard ML or MIRANDA) and logic programming (as embodied in PROLOG) in a simple, flexible, and mathematically vell founded vay. The language relies on a constructor discipline, vell suited to accommodate PROLOG terms and HOPE-like patterns. From the syntactical point of viev, BABEL combines puré PROLOG vith a functional notation vith neither types ñor higher order functions. On the other side, the language uses narroving as the basis of a lazy reduction semantics vhich embodies both revriting and SLD resolution and supports computation vith potentially infinite data structures. There is also a declarative semantics, based on Scott domains vhich provides a notion of least Herbrand model for BABEL programs. We develop both semantics and prove soundness and completeness results giving the expected equivalence betveen them. Ve also illustrate the features of the language through some programming examples. It has been argued that narroving is very hard to implement and should be better reduced to SLD-resolution, in order to exploit the efficient implementation techniques already knovn for PROLOG. But vhat about the efficient implementation techniques for functional languages? We have designed an extensión of a functional graph reduction machine with unification and backtracking facilities borroved from Varren's abstract machine for PROLOG. In this vay, ve obtain an abstract narroving machine vhich supports a sequential, innermost versión of BABEL. Ve believe that this approach is vell suited to achieve efficient implementations. Lazy and parallel versión of the present prototypes vill be a subject of a further research. A PROLOG interpreter for BABEL is also included in the vork