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.

En el principio era Távora - : itinerario para la transmisión de una síntesis arquitectónica

La tesis afronta el análisis del itinerario vital de Fernando Távora, una vida entregada apasionadamente a una causa de refundación estética y conceptual de una arquitectura portuguesa condenada a la mediocridad y al ostracismo en el momento en que empieza a ejercer la profesión. La investigación se adentra en todos los aspectos que convergen en su dedicación al logro de aquella misión, pues la que él mismo probablemente llamaría orteguianamente su circunstancia, resulta inseparable de su pensamiento y de su obra. Se pretende establecer la riqueza y complejidad de la figura de Fernando Távora y su importancia como punto de inflexión en la evolución de la arquitectura portuguesa, que ha llegado a alcanzar el reconocimiento internacional en las últimas décadas, fundamentalmente a partir de la consagración de Álvaro Siza Vieira y la denominada Escuela de Oporto. Desde una posición de absoluta autonomía respecto de lo que acontece dentro y fuera de las fronteras portuguesas, su labor se distinguirá por su singularidad teórica y arquitectónica, no dejando por ello de influir decisivamente en su entorno cercano. Dos manifiestos escritos, el juvenil O problema da Casa Portuguesa y el posterior Da Organização do Espaço son elementos estructurantes de un pensamiento teórico que germina en una obra construida inseparable de aquel, de cuya coherencia dan testimonio los aquí considerados verdaderos manifiestos proyectuales del arquitecto. Efectivamente, se analizarán detalladamente como tales la Casa sobre o Mar –manifiesto inicial-, el Pabellón de Tenis –manifiesto de confirmación- y la Casa dos 24 -manifiesto final-, proyectos que vieron la luz en diferentes etapas de su trayectoria y constituyen la aplicación práctica de sus teorías en una sintaxis magistral. En estos tres proyectos es donde verdaderamente la tesis cobra cuerpo, pues suponen el reflejo de la verdadera aportación del arquitecto al pensamiento arquitectónico europeo, la foto fija de la proclamación de resultados de un proyecto arquitectónico integral en momentos muy significativos de su itinerario vital, cuya complejidad se entiende a través de las fases más descriptivas de este documento. Se mostrará cómo para acometer su proyecto integral de arquitectura, una causa de regeneración de la arquitectura portuguesa a partir de la síntesis entre modernidad y tradición, entre universalidad y localidad, tomaría de sus dos personajes más admirados, Le Corbusier y Pessoa, la fuerza moral y la energía que le permitieron acometer apasionadamente tamaña misión. En una infatigable búsqueda en lo global y lo local, Távora conseguirá prestar gran atención al contexto del lugar de intervención sin renunciar a sus convicciones modernas, introduciendo la historia y el dibujo como herramientas de conocimiento del mismo y posteriormente del proceso creativo. El método proyectivo resultante de este modelo, que transmitirá a través de su ejercicio docente a sucesivas generaciones de arquitectos, se convertirá en elemento estructurante de una tendencia surgida de las aulas portuenses, que la crítica internacional acabará denominando Escuela de Oporto en un sentido más amplio. Por su importancia dentro del itinerario profesional del[os] arquitecto[s] portuense[s], las fases más destacadas de su evolución a partir de los años 50 se analizarán en paralelo a una serie de obras representativas de diferentes momentos de la trayectoria de Fernando Távora. En este itinerario vital, a pesar de la originalidad de su pensamiento y su obra, se atisban ciertos paralelismos con grandes arquitectos del siglo XX, que esta tesis afronta. Se puede distinguir entre influencias pasajeras de algunos maestros modernos en los que Távora buscaba la confirmación a sus propias teorías, similitudes con arquitectos coetáneos cuya obra conoció y a los que se encontró cercano por la convergencia de algunos de sus criterios e incluso sorprendentes coincidencias con arquitectos desconocidos para él, entre las que cabe destacar la de los maestros de la Escuela de Madrid Alejandro de la Sota y Javier Sáenz de Oiza. Por último, en una alegoría con los heterónimos de Fernando Pessoa, se analiza desde una perspectiva personal fruto de la investigación y de las entrevistas mantenidas con todos ellos, la importante labor de Álvaro Siza Vieira, Alexandre Alves Costa y su hijo José Bernardo Távora como agentes coadyuvantes en la consecución del proyecto integral de arquitectura [y vida] de Fernando Távora. Sin lugar a dudas, Álvaro Siza constituye el personaje fundamental e imprescindible para que la arquitectura portuguesa alcanzase la privilegiada consideración que en la actualidad ostenta en la escena internacional. Un arquitecto consagrado que ocupa ya, y ocupará siempre, un lugar privilegiado en la breve lista de maestros míticos e irrepetibles de la arquitectura contemporánea. Con todo, cabe afirmar con la paráfrasis bíblica que da título a la tesis que ‘En el principio era Távora...’ ABSTRACT This thesis addresses the analysis of Fernando Távora’s life journey, a life that was passionately devoted to the cause of aesthetically and conceptually overhauling Portuguese architecture, which was doomed to mediocrity and ostracism at the time when he started practicing professionally. This research delves into all aspects converging in his dedication to achieving that mission, since what he himself would probably call his circumstance – in the manner of José Ortega y Gasset – is inseparable from his thinking and his work. This thesis seeks also to establish the richness and complexity of Fernando Távora’s figure and his importance as a turning point in the evolution of Portuguese architecture, which has gone on to achieve international recognition in recent decades, especially after the consecration of Álvaro Siza Vieira and the so-called School of Oporto. From an absolutely autonomous position with regard to what is happening within and outside Portuguese borders, his work will stand out due to its theoretical and architectural uniqueness – this not being a reason to prevent its decisive influence on his close surroundings. Two written manifestos, his early O problema da Casa Portuguesa and his subsequent Da Organização do Espaço, become structural elements of the theoretical thinking that develops into works which are built in parallel with the former. The coherence of this thinking is reflected on the hereby considered the architect’s true project manifestos. Indeed, we will analyse as such the Casa sobre o Mar (initial manifesto), the Tennis Pavilion (confirmation manifesto) and Casa dos 24 (final manifesto), projects which saw the light at different stages of his career and constitute the practical application of his theories in a masterful syntax. These are the three projects where the thesis takes shape, as they become the reflection of the architect’s true contribution to the European architectural school of thought; the still picture of the results proclamation of a whole architectural project at highly significant moments in his life journey, whose complexity can be understood through this document’s most descriptive phases. This study will show how, in order to carry out his architectural project – regenerate Portuguese architecture by synthesizing modernity and tradition, universality and locality –, Távora would take the moral strength and energy from his two most admired figures, Le Corbusier and Pessoa, allowing him to passionately undertake such a colossal mission. In a tireless search within the global and the local, Távora will manage to pay more attention to the context of the intervention place without compromising his modern convictions, by introducing history and drawing as knowledge tools of the place and eventually of the creative process. The resulting projective method of this model, which he will transmit to successive generations of architects through his teaching, will become a structural element of a trend emerged from the Oporto classrooms which international critique will end up denominating School of Porto in a broader sense. Due to its importance within Porto architect[s]’ professional career, the most prominent phases of its evolution as of the 50s will be analysed in parallel to a series of representative works from different moments in Fernando Távora’s career. Despite the originality of his thinking and his work, certain parallelisms with great architects from the 20th century can be found in Távora’s life journey, which this thesis will address. Amongst temporary influences of some modern masters in whom Távora sought confirmation of his own theories, similarities can be spotted with contemporary architects whose work he knew and to whom he felt close because of the convergence of some of his views. It is also possible to see surprising coincidences with architects he did not know, such as Alejandro de la Sota and Javier Sáenz de Oiza, masters from the School of Madrid. Finally, in an allegory with Fernando Pessoa’s heteronyms, this thesis studies – from a personal perspective based on research and the interviews held with all of them – the important work of Álvaro Siza Vieira, Alexandre Alves Costa and his son Jose Bernardo Távora as auxiliaries in the achievement of Fernando Távora’s complete architectural [and life] project. Without the slightest doubt, Álvaro Siza constitutes the essential figure thanks to whom Portuguese architecture would reach the advantaged position it holds nowadays in the international arena. An acclaimed architect, Siza already holds a privileged spot in the brief list of legendary and unrepeatable masters of contemporary architecture. Nevertheless, with the biblical paraphrase that entitles this thesis it can be claimed that ‘In the beginning was Távora…’