Relational and Allegorical Semantics for Constraint Logic Programming

El cálculo de relaciones binarias fue creado por De Morgan en 1860 para ser posteriormente desarrollado en gran medida por Peirce y Schröder. Tarski, Givant, Freyd y Scedrov demostraron que las álgebras relacionales son capaces de formalizar la lógica de primer orden, la lógica de orden superior así como la teoría de conjuntos. A partir de los resultados matemáticos de Tarski y Freyd, esta tesis desarrolla semánticas denotacionales y operacionales para la programación lógica con restricciones usando el álgebra relacional como base. La idea principal es la utilización del concepto de semántica ejecutable, semánticas cuya característica principal es el que la ejecución es posible utilizando el razonamiento estándar del universo semántico, este caso, razonamiento ecuacional. En el caso de este trabajo, se muestra que las álgebras relacionales distributivas con un operador de punto fijo capturan toda la teoría y metateoría estándar de la programación lógica con restricciones incluyendo los árboles utilizados en la búsqueda de demostraciones. La mayor parte de técnicas de optimización de programas, evaluación parcial e interpretación abstracta pueden ser llevadas a cabo utilizando las semánticas aquí presentadas. La demostración de la corrección de la implementación resulta extremadamente sencilla. En la primera parte de la tesis, un programa lógico con restricciones es traducido a un conjunto de términos relacionales. La interpretación estándar en la teoría de conjuntos de dichas relaciones coincide con la semántica estándar para CLP. Las consultas contra el programa traducido son llevadas a cabo mediante la reescritura de relaciones. Para concluir la primera parte, se demuestra la corrección y equivalencia operacional de esta nueva semántica, así como se define un algoritmo de unificación mediante la reescritura de relaciones. La segunda parte de la tesis desarrolla una semántica para la programación lógica con restricciones usando la teoría de alegorías—versión categórica del álgebra de relaciones—de Freyd. Para ello, se definen dos nuevos conceptos de Categoría Regular de Lawvere y _-Alegoría, en las cuales es posible interpretar un programa lógico. La ventaja fundamental que el enfoque categórico aporta es la definición de una máquina categórica que mejora e sistema de reescritura presentado en la primera parte. Gracias al uso de relaciones tabulares, la máquina modela la ejecución eficiente sin salir de un marco estrictamente formal. Utilizando la reescritura de diagramas, se define un algoritmo para el cálculo de pullbacks en Categorías Regulares de Lawvere. Los dominios de las tabulaciones aportan información sobre la utilización de memoria y variable libres, mientras que el estado compartido queda capturado por los diagramas. La especificación de la máquina induce la derivación formal de un juego de instrucciones eficiente. El marco categórico aporta otras importantes ventajas, como la posibilidad de incorporar tipos de datos algebraicos, funciones y otras extensiones a Prolog, a la vez que se conserva el carácter 100% declarativo de nuestra semántica. ABSTRACT The calculus of binary relations was introduced by De Morgan in 1860, to be greatly developed by Peirce and Schröder, as well as many others in the twentieth century. Using different formulations of relational structures, Tarski, Givant, Freyd, and Scedrov have shown how relation algebras can provide a variable-free way of formalizing first order logic, higher order logic and set theory, among other formal systems. Building on those mathematical results, we develop denotational and operational semantics for Constraint Logic Programming using relation algebra. The idea of executable semantics plays a fundamental role in this work, both as a philosophical and technical foundation. We call a semantics executable when program execution can be carried out using the regular theory and tools that define the semantic universe. Throughout this work, the use of pure algebraic reasoning is the basis of denotational and operational results, eliminating all the classical non-equational meta-theory associated to traditional semantics for Logic Programming. All algebraic reasoning, including execution, is performed in an algebraic way, to the point we could state that the denotational semantics of a CLP program is directly executable. Techniques like optimization, partial evaluation and abstract interpretation find a natural place in our algebraic models. Other properties, like correctness of the implementation or program transformation are easy to check, as they are carried out using instances of the general equational theory. In the first part of the work, we translate Constraint Logic Programs to binary relations in a modified version of the distributive relation algebras used by Tarski. Execution is carried out by a rewriting system. We prove adequacy and operational equivalence of the semantics. In the second part of the work, the relation algebraic approach is improved by using allegory theory, a categorical version of the algebra of relations developed by Freyd and Scedrov. The use of allegories lifts the semantics to typed relations, which capture the number of logical variables used by a predicate or program state in a declarative way. A logic program is interpreted in a _-allegory, which is in turn generated from a new notion of Regular Lawvere Category. As in the untyped case, program translation coincides with program interpretation. Thus, we develop a categorical machine directly from the semantics. The machine is based on relation composition, with a pullback calculation algorithm at its core. The algorithm is defined with the help of a notion of diagram rewriting. In this operational interpretation, types represent information about memory allocation and the execution mechanism is more efficient, thanks to the faithful representation of shared state by categorical projections. We finish the work by illustrating how the categorical semantics allows the incorporation into Prolog of constructs typical of Functional Programming, like abstract data types, and strict and lazy functions.

Programming with global analysis

Global data-flow analysis of (constraint) logic programs, which is generally based on abstract interpretation [7], is reaching a comparatively high level of maturity. A natural question is whether it is time for its routine incorporation in standard compilers, something which, beyond a few experimental systems, has not happened to date. Such incorporation arguably makes good sense only if: • the range of applications of global analysis is large enough to justify the additional complication in the compiler, and • global analysis technology can deal with all the features of "practical" languages (e.g., the ISO-Prolog built-ins) and "scales up" for large programs. We present a tutorial overview of a number of concepts and techniques directly related to the issues above, with special emphasis on the first one. In particular, we concéntrate on novel uses of global analysis during program development and debugging, rather than on the more traditional application área of program optimization. The idea of using abstract interpretation for validation and diagnosis has been studied in the context of imperative programming [2] and also of logic programming. The latter work includes issues such as using approximations to reduce the burden posed on programmers by declarative debuggers [6, 3] and automatically generating and checking assertions [4, 5] (which includes the more traditional type checking of strongly typed languages, such as Gódel or Mercury [1, 8, 9]) We also review some solutions for scalability including modular analysis, incremental analysis, and widening. Finally, we discuss solutions for dealing with meta-predicates, side-effects, delay declarations, constraints, dynamic predicates, and other such features which may appear in practical languages. In the discussion we will draw both from the literature and from our experience and that of others in the development and use of the CIAO system analyzer. In order to emphasize the practical aspects of the solutions discussed, the presentation of several concepts will be illustrated by examples run on the CIAO system, which makes extensive use of global analysis and assertions.

Las lecturas de Sáenz de Oíza. Desde Torres Blancas al Banco de Bilbao a través de una selección de textos hecha por el propio arquitecto.

El 29 de enero de 2000 Francisco Javier Sáenz de Oíza ofrece su última conferencia en el salón de actos del edificio sede del BBVA en el Paseo de la Castellana de Madrid. Esta conferencia inaugura el ciclo “El arquitecto enseña su obra”, organizado por el Colegio Oficial de Arquitectos de Madrid (C.O.A.M.) y la Escuela Técnica Superior de Arquitectura de Madrid (E.T.S.A.M.). Las obras en concreto que Oíza 'enseña' en este evento son Torres Blancas (Madrid, 1961- 1968) y Banco de Bilbao (Madrid, 1971-1980). Antes de la conferencia, blandiendo una carpeta, Oíza dice: Traigo aquí los textos de siempre, los que siempre he usado, (...) yo no he escrito ni una línea, solo he subrayado ciertos pasajes, en la medida de lo posible me gustaría leer alguno. Pero como aquí hay como para cinco horas, pues no se qué hacer. Citarlo sí, porque de ustedes el que quiera penetrar un poco en mi conocimiento, pues que vea las citas que yo hago aquí, qué pasajes, o qué libros o qué artículos propongo. 1 La carpeta que lleva Oíza en su mano contiene veinticuatro fichas mecanografiadas por él mismo. Las fichas son pasajes de textos; en su mayoría de textos literarios o poéticos, e incluyen una referencia bibliográfica que menciona: título de libro, edición y número de página. Además, en cada ficha están resaltados los pasajes que Oíza pretende leer. 2 Antes del comienzo de la conferencia Oíza dice: Tengo aquí citas de lecturas que le recomendaría a quien quiera enterarse de cómo es este edificio. 3 Durante la conferencia Oíza no parece hablar sobre las obras que debe enseñar; en cambio se dedica, casi exclusivamente, a leer en público. Esta tesis nace de lo sugerido por el propio Oíza. El objetivo general, siguiendo sus propias palabras, es 'penetrar un poco' en su conocimiento a partir de citas y recomendaciones de lecturas realizadas por él mismo al tratar sobre arquitectura. La hipótesis central plantea que por medio de sus lecturas Oíza sí habla de arquitectura, y sostiene también que a partir de sus textos es posible 'enterarse', al menos en parte, de cómo es un edificio, en particular Torres Blancas y Banco de Bilbao. Más aún, se plantea la hipótesis de que Oíza, maestro ágrafo y de carácter socrático, ha construido, no obstante, un 'discurso teórico' arquitectónico suficientemente sistemático. De modo que aún cuando Oíza no ha dejado una 'teoría' escrita es posible reconstruirla, en cierta medida, a partir de su elocución y a partir de la comprensión de sus 'lecturas'. Las fuentes primarias de esta tesis son: a) Las lecturas que Oíza recomienda en su conferencia de enero de 2000. b) Torres Blancas y Banco de Bilbao. c) Las lecturas en público realizadas por Oíza en conferencias, cursos, debates, mesas redondas, programas de TV, etc. El tema que se investiga es la relación entre los textos recomendados por Oíza y su arquitectura, y la pregunta guía de la investigación es cómo y en qué medida los textos pueden contribuir a la comprensión del pensamiento, del discurso y de la obra de Oíza. Torres Blancas y Banco de Bilbao son, en todo momento, las dos principales obras utilizadas para la observación y el contraste de los resultados de la investigación teórica en el desarrollo de la tesis. El soporte teórico y metodológico de la tesis está dado por la hermenéutica en tanto disciplina encargada de la interpretación y correcta comprensión de textos y obras, en particular por la filosofía hermenéutica de Hans-Georg Gadamer expuesta en Verdad y método. La relevancia, el aspecto original y la posible aportación al conocimiento de esta tesis consiste en una aproximación a Oíza y a su arquitectura, desde un punto de vista hasta ahora no investigado de forma sistemática, esto es, a partir de las lecturas de Oíza. ABSTRACT On 29th January 2000 Francisco Javier Sáenz de Oíza gave his last lecture in the Auditorium at BBVA headquarters located in Paseo de la Castellana avenue in Madrid. That lecture opened the series The Architect Shows his Work (El arquitecto enseña su obra) organised by the COAM Official College of Architects and the ETSAM Architecture School of Madrid. The specific works that Oíza 'shows' in his lecture were Torres Blancas (Madrid, 1961- 1968) and Banco de Bilbao (Madrid, 1971-1980). Before the lecture, waving a folder in his hand, Oíza says: I've got here the texts I've always used, (…) I haven't written a line, I've only underlined certain passages, I would like to read some of them to the extent possible. But I have here about five hours of reading, so I don't know what to do. I can cite them, yes, and anyone of you who want to delve a little into my knowledge can look at the citations I make here, the passages, books or articles I recommend. 1 The folder in Oíza's hand contains 24 files typed by the architect himself. The files consist of text passages -most of which are literary or poetry texts- and include the bibliographic citation with book the title, edition and page number. In addition, the passages Oíza intends to read are highlighted. Before starting his lecture Oíza says: I've got here citations of readings I'd recommend to those who want to realise how this building is. 2 During the lecture Oíza doesn't seem to be talking about the works he has to show, on the contrary, he focuses almost exclusively on reading texts to the audience. This thesis is the result of a suggestion made by Oíza himself. The broad aim is to 'delve a little into' his knowledge using citations and reading recommendations made by Oíza when dealing with the architecture subject. The main hypothesis proposes that Oíza talks about architecture through his readings and that starting from 'his' texts it is possible to 'realise', at least in part, how a building is, Torres Blancas and Banco de Bilbao in particular. Moreover, it is proposed the hypothesis that Oíza, as a Socratic teacher reluctant to write down his ideas, has nevertheless built a systematic 'theoretical discourse' on architecture. As a result, even when he has not written a 'theory', it is possible to reconstruct it to a certain degree, starting from his speech and from the understanding of his readings. The primary sources for this thesis are: a) The readings that Oíza recommends in his lecture of January 2000. b) The Torres Blancas and Banco de Bilbao. c) The readings done by Oíza in presentations, lectures, debates, panel discussions, television programmes, etc. The subject under research is the relationship between the texts that Oíza recommends and his architecture. The guiding question for the research is how and to what extent the texts can contribute to the understanding of Oíza's thoughts, discourse and work. Torres Blancas and Banco de Bilbao are the two main works considered along the thesis and they have been used for observation and to test the results of the theoretical research as it progresses. The thesis theoretical and methodological framework is based on the hermeneutics -as the discipline that deals with the interpretation and the correct understanding of texts and works-, in particular the hermeneutics philosophy of Hans-Georg Gadamer in Truth and Method. The relevance, the original element and the possible contribution of this thesis is given by the approach to Oíza and his architecture through Oíza's readings, a perspective that hasn't been yet systematically researched.