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.

Seed image analysis and taxonomy of Diplotaxis DC. (Brassicaceae, Brassiceae)

The genus Diplotaxis, comprising 32 or 34 species, plus several additional infraspecific taxa, displays a considerable degree of heterogeneity in the morphology, molecular markers, chromosome numbers and geographical amplitude of the species. The taxonomic relationships within the genus Diplotaxis were investigated by phenetic characterisation of germplasm belonging to 27 taxa of the genus, because there is an increasing interest in Diplotaxis, since some of its species (D. tenuifolia, D. muralis) are gathered or cultivated for human consumption, whereas others are frequent arable weeds (D. erucoides) in many European vineyards. Using a computer-aided vision system, 33 morpho-colorimetric features of seeds were electronically measured. The data were used to implement a statistical classifier, which is able to discriminate the taxa within the genus Diplotaxis, in order to compare the resulting species grouping with the current infrageneric systematics of this genus. Despite the high heterogeneity of the samples, due to the great intra-population variability, the stepwise Linear Discriminant Analysis method, applied to distinguish the groups, was able to reach over 80% correct identification. The results obtained allowed us to confirm the current taxonomic position of most taxa and suggested the taxonomic position of others for reconsideration.

Approximate Relational Reasoning for Probabilistic Programs

La seguridad verificada es una metodología para demostrar propiedades de seguridad de los sistemas informáticos que se destaca por las altas garantías de corrección que provee. Los sistemas informáticos se modelan como programas probabilísticos y para probar que verifican una determinada propiedad de seguridad se utilizan técnicas rigurosas basadas en modelos matemáticos de los programas. En particular, la seguridad verificada promueve el uso de demostradores de teoremas interactivos o automáticos para construir demostraciones completamente formales cuya corrección es certificada mecánicamente (por ordenador). La seguridad verificada demostró ser una técnica muy efectiva para razonar sobre diversas nociones de seguridad en el área de criptografía. Sin embargo, no ha podido cubrir un importante conjunto de nociones de seguridad “aproximada”. La característica distintiva de estas nociones de seguridad es que se expresan como una condición de “similitud” entre las distribuciones de salida de dos programas probabilísticos y esta similitud se cuantifica usando alguna noción de distancia entre distribuciones de probabilidad. Este conjunto incluye destacadas nociones de seguridad de diversas áreas como la minería de datos privados, el análisis de flujo de información y la criptografía. Ejemplos representativos de estas nociones de seguridad son la indiferenciabilidad, que permite reemplazar un componente idealizado de un sistema por una implementación concreta (sin alterar significativamente sus propiedades de seguridad), o la privacidad diferencial, una noción de privacidad que ha recibido mucha atención en los últimos años y tiene como objetivo evitar la publicación datos confidenciales en la minería de datos. La falta de técnicas rigurosas que permitan verificar formalmente este tipo de propiedades constituye un notable problema abierto que tiene que ser abordado. En esta tesis introducimos varias lógicas de programa quantitativas para razonar sobre esta clase de propiedades de seguridad. Nuestra principal contribución teórica es una versión quantitativa de una lógica de Hoare relacional para programas probabilísticos. Las pruebas de correción de estas lógicas son completamente formalizadas en el asistente de pruebas Coq. Desarrollamos, además, una herramienta para razonar sobre propiedades de programas a través de estas lógicas extendiendo CertiCrypt, un framework para verificar pruebas de criptografía en Coq. Confirmamos la efectividad y aplicabilidad de nuestra metodología construyendo pruebas certificadas por ordendor de varios sistemas cuyo análisis estaba fuera del alcance de la seguridad verificada. Esto incluye, entre otros, una meta-construcción para diseñar funciones de hash “seguras” sobre curvas elípticas y algoritmos diferencialmente privados para varios problemas de optimización combinatoria de la literatura reciente. ABSTRACT The verified security methodology is an emerging approach to build high assurance proofs about security properties of computer systems. Computer systems are modeled as probabilistic programs and one relies on rigorous program semantics techniques to prove that they comply with a given security goal. In particular, it advocates the use of interactive theorem provers or automated provers to build fully formal machine-checked versions of these security proofs. The verified security methodology has proved successful in modeling and reasoning about several standard security notions in the area of cryptography. However, it has fallen short of covering an important class of approximate, quantitative security notions. The distinguishing characteristic of this class of security notions is that they are stated as a “similarity” condition between the output distributions of two probabilistic programs, and this similarity is quantified using some notion of distance between probability distributions. This class comprises prominent security notions from multiple areas such as private data analysis, information flow analysis and cryptography. These include, for instance, indifferentiability, which enables securely replacing an idealized component of system with a concrete implementation, and differential privacy, a notion of privacy-preserving data mining that has received a great deal of attention in the last few years. The lack of rigorous techniques for verifying these properties is thus an important problem that needs to be addressed. In this dissertation we introduce several quantitative program logics to reason about this class of security notions. Our main theoretical contribution is, in particular, a quantitative variant of a full-fledged relational Hoare logic for probabilistic programs. The soundness of these logics is fully formalized in the Coq proof-assistant and tool support is also available through an extension of CertiCrypt, a framework to verify cryptographic proofs in Coq. We validate the applicability of our approach by building fully machine-checked proofs for several systems that were out of the reach of the verified security methodology. These comprise, among others, a construction to build “safe” hash functions into elliptic curves and differentially private algorithms for several combinatorial optimization problems from the recent literature.

A taxonomy of the quality attributes for distributed applications

The software engineering community has paid little attention to non-functional requirements, or quality attributes, compared with studies performed on capture, analysis and validation of functional requirements. This circumstance becomes more intense in the case of distributed applications. In these applications we have to take into account, besides the quality attributes such as correctness, robustness, extendibility, reusability, compatibility, efficiency, portability and ease of use, others like reliability, scalability, transparency, security, interoperability, concurrency, etc. In this work we will show how these last attributes are related to different abstractions that coexist in the problem domain. To achieve this goal, we have established a taxonomy of quality attributes of distributed applications and have determined the set of necessary services to support such attributes.

Replication types: towards a shared taxonomy

Context: The software engineering community is becoming more aware of the need for experimental replications. In spite of the importance of this topic, there is still much inconsistency in the terminology used to describe replications. Objective: Understand the perspectives of empirical researchers about various terms used to characterize replications and propose a consistent taxonomy of terms. Method: A survey followed by plenary discussion during the 2013 International Software Engineering Research Network meeting. Results: We propose a taxonomy which consolidates the disparate terminology. This taxonomy had a high level of agreement among workshop attendees. Conclusion: Consistent terminology is important for any field to progress. This work is the first step in that direction. Additional study and discussion is still necessary.

Hacia una taxonomía constructiva de las tapias de tierra y fábricas encofradas históricas = Towards a constructive taxonomy of the historical rammed-earth and formwork masonry

El objetivo fundamental de la investigación es el estudio de los fundamentos constructivos de las fábricas históricas de tapia de tierra y mampostería encofrada de las fortificaciones bajomedievales. Ante las incertidumbres detectadas en la datación de estas estructuras y frente al excesivo número de excepciones que quedan fuera de las clasificaciones tradicionalmente empleadas para estudiar este tipo de técnicas, el artículo desarrolla una propuesta de tipología o taxonomía constructiva basada en un sistema abierto. Este sistema nace del análisis de un número significativo de fábricas y atiende a diversos parámetros de control para la completa caracterización de cada fábrica: material, grado de compactación, función constructiva, encofrado, acabado superficial, combinación de materiales y situación, profundidad, formación y sección de los agujales. Cada fábrica se clasifica mediante una etiqueta alfanumérica. El sistema permite establecer tipos constructivos con los que se genera una clasificación cronotipológica constructiva. ABSTRACT The principal aim of the research is the study of the constructive reasons of the historical masonries built with rammed earth and formwork masonry, belonging to late medieval fortifications. Uncertainties have been warned about dating the historical masonries and there are excessive exceptions that do not fall in the rankings traditionally employed to study these techniques. Due to these reasons, the article develops a proposal of constructive typology or taxonomy based in an open system that comes from the analysis of a representative number of masonries and that attends to several control parameters tor the complete characterization of each masonry: material, compaction degree, constructive function, formwork, rendering, combination of materials and, last, the situation, deepness, formation and section of the putlogholes. Each masonry is classified through an alphanumeric label. The system allows establishing several constructive types which it is possible to do a cronotypological and constructive classification.

Estratos arquitectónicos : conceptos, lógicas, sinopsis

La presente tesis doctoral se centra en la investigación del "estrato arquitectónico", manejando conceptos, lógicas y sinopsis como puntos organizativos, enlazados y superpuestos, que den paso a un marco propositivo que pueda ser simultáneamente articulado e independiente. Una situación que, ante nuevos desafíos, pretende ir más allá de una estricta definición de estrato o de su noción preconcebida descrita desde la superposición de diversos materiales. Todo ello a fin de revelar los diferentes perfiles del estrato y de la estratificación. Para ello, se abre y amplía el campo de estudio proyectual/procesual desdibujando los límites entre disciplinas –geología, filosofía, tecnología, arquitectura–. Y al mismo tiempo, se construye una cartografía del estrato arquitectónico asociada: a una taxonomía descriptora, a nuevas formulaciones, a pensamientos de personajes reconocibles y/o rescatados –como Rowe/Slutzky, Smithson, Parent/Virilio, Koolhaas, MVRDV, etc.–, y, por último, a nuevas lógicas proyectuales y operativas referidas al estrato, que fusionan conocimientos complejos. Unos contenidos que habitualmente no se presentan en investigaciones doctorales tradicionales –lo que permite afrontar nuevos cambios metodológicos, e imprimir un punto de partida para el desarrollo de futuras investigaciones o de otros posibles caminos emergentes–. Así, el discurso se impregna de nuevos referentes teóricos dentro de una misma mitología común (la del estrato). Un tema abordado con claves híbridas, es decir, con estudios selectivos y escritos coleccionados –analizados a partir de antecedentes encontrados y consolidados–, combinados con interpretaciones subyacentes en la arquitectura contemporánea –que pueden todavía encontrarse en fase experimental–. Una investigación que muestra la adaptación, la evolución y el cambio de la definición de "estrato arquitectónico", así como de su apariencia, utilización y aplicación a lo largo del tiempo, consecuencia de las nuevas necesidades y/o de las nuevas bases ideológicas ocasionadas por nuevos descubrimientos. Estratos arquitectónicos que dotan al espacio de profundidad –desde la bidimensionalidad– mediante la superposición de planos paralelos hacia la construcción de una nueva experiencia de estratificación fenomenológica. Estratos que generan estímulos y cambian su materialidad –de opacos a (en)tramados– creando apariencias y produciendo diversos efectos, para posteriormente exfoliarse y convertirse en estratos habitables. Estratos capturadores del espacio-tiempo, o de las dinámicas internas. Llegando incluso, con un último giro, a la era digital, donde el estrato informacional –que continua siendo independiente, autónomo y diverso, y que puede ser modificado, manipulado, suprimido o activable sin alterar el conjunto–, propicia obtener sistemas flexibles, relacionales, capaces de mutar o adaptarse, asociados a distintos niveles de organización dispositiva, que impulsan acciones y hacen emerger lógicas proyectuales. Estratos que surgen de forma elaborada o espontánea en el territorio urbano o natural (ciudad sobre ciudad, suelo sobre suelo), que se aplican extendiendo e hibridando el territorio (paisajes operativos), que son replanteados artificialmente como mecanismos edificatorios según las exigencias existentes (estratos programáticos, capas especializadas), y que se implantan como capas/layers en los programas informáticos utilizados como herramientas de diseño (multicapas, sistemas de intercambio informacional). Un trabajo que se estructura de manera multicapa lo que permite recorrer la tesis como un mapa de secuencias, saltar entre estratos de información, o seleccionar lecturas según intereses de pensamiento o acción arquitectónica. En consecuencia, una investigación sobre el "estrato arquitectónico" que conecta diversas disciplinas, que recopila distintos posicionamientos teórico/prácticos –lo que implica la introducción de parámetros y datos vivos–, y afronta un posicionamiento estratégico que vuelve a poner en valor el estrato arquitectónico –partiendo de estrategias formales que se han transformado en estrategias experimentales/operativas (a medida que el entorno se ha ido complejizando), siguiendo una estrategia conceptual e intelectual contemporánea, propia y específica–. ABSTRACT This PhD thesis is based on the research of "architectural stratum" using concepts, logical and synopsis as organizational, linked and overlapping points, which give way to a proactive framework that can be articulated and independent simultaneously. A situation that, faced with new challenges, aims to go beyond a strict definition of stratum or their preconceived notion described from the superposition of different materials. All this in order to reveal the different profiles of stratum and stratification. To do this, it opens and widens the field of project/process study, blurring the boundaries between disciplines –geology, philosophy, technology, architecture–. And, at the same time, a cartography of the architectural stratum is constructed, that associates with: descriptor taxonomy, new formulations, thoughts of recognizable and/or rescued characters, –as Rowe/Slutzky, Smithson, Parent/Virilio, Koolhaas, MVRDV, etc.–, and finally, a new project and operational logics referred to stratum, which merge complex knowledge. A content not usually presented in traditional doctoral research –which can face new methodological changes, and creates a starting point for future research or other possible emerging paths–. Thus, the work is imbued with new theoretical framework within a common mythology (stratum’s myth). An issue addressed with hybrid keys, that is, with selective studies and collected writings –analyzed starting from found and consolidated backgrounds–, combined with underlying performances on contemporary architecture –which can still be in experimental phase–. A research that shows adaptation, evolution and change of the definition of "architectural stratum", as well as their appearance, use and application throughout time, result of the new requirements and/or the new ideological foundations caused by new discoveries. Architectural strata that give depth to space –from two-dimensionality– by overlapping parallel planes towards the construction of a new experience of phenomenological stratification. Strata that generate stimuli and change their materiality –from opaque to lattice– creating appearances and producing various effects, for later exfoliating and becoming habitable strata. Strata that capture space-time or internal dynamics. Even reaching, with a final twist, the digital age, where the informational stratum –which remains independent, autonomous and diverse, and can be modified, manipulated, deleted or activated without altering the whole–, contribute to obtaining flexible, relational systems, able to mutate or adapt, associated with different levels of regulatory organization, that drive actions and make emerge project logics. Strata that arise elaborately or spontaneously in urban or natural territory (city upon city, floor upon floor), which apply expanding and hybridizing the territory (operational landscapes), which are artificially restated as building mechanisms according to existing requirements (strata program, specialized layers), which are implemented as layers in the software used as design tools (multilayer, systems of informational interchange). A work that is structured in a multi-layered way, which allows explore the thesis as a sequence map, jump between layers of information, or select readings according to an interest in thought or architectural action. Therefore, an investigation into the "architectural stratum" that connects different disciplines, which collects different theoretical/practical positions –which implies the introduction of live parameters and data– and faces a strategic positioning returning to value the architectural stratum –based on formal strategies that have become experimental/operational strategies (as the environment has become more complex), following a conceptual, intellectual, contemporary, own specific strategy–.