Constraint handling rules. Compositional semantics and program transformation

This thesis intends to investigate two aspects of Constraint Handling Rules (CHR). It proposes a compositional semantics and a technique for program transformation. CHR is a concurrent committed-choice constraint logic programming language consisting of guarded rules, which transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion [Frü06] and it belongs to the declarative languages family. It was initially designed for writing constraint solvers but it has recently also proven to be a general purpose language, being as it is Turing equivalent [SSD05a]. Compositionality is the first CHR aspect to be considered. A trace based compositional semantics for CHR was previously defined in [DGM05]. The reference operational semantics for such a compositional model was the original operational semantics for CHR which, due to the propagation rule, admits trivial non-termination. In this thesis we extend the work of [DGM05] by introducing a more refined trace based compositional semantics which also includes the history. The use of history is a well-known technique in CHR which permits us to trace the application of propagation rules and consequently it permits trivial non-termination avoidance [Abd97, DSGdlBH04]. Naturally, the reference operational semantics, of our new compositional one, uses history to avoid trivial non-termination too. Program transformation is the second CHR aspect to be considered, with particular regard to the unfolding technique. Said technique is an appealing approach which allows us to optimize a given program and in more detail to improve run-time efficiency or spaceconsumption. Essentially it consists of a sequence of syntactic program manipulations which preserve a kind of semantic equivalence called qualified answer [Frü98], between the original program and the transformed ones. The unfolding technique is one of the basic operations which is used by most program transformation systems. It consists in the replacement of a procedure-call by its definition. In CHR every conjunction of constraints can be considered as a procedure-call, every CHR rule can be considered as a procedure and the body of said rule represents the definition of the call. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. We define an unfolding rule, show its correctness and discuss some conditions in which it can be used to delete an unfolded rule while preserving the meaning of the original program. Finally, confluence and termination maintenance between the original and transformed programs are shown. This thesis is organized in the following manner. Chapter 1 gives some general notion about CHR. Section 1.1 outlines the history of programming languages with particular attention to CHR and related languages. Then, Section 1.2 introduces CHR using examples. Section 1.3 gives some preliminaries which will be used during the thesis. Subsequentely, Section 1.4 introduces the syntax and the operational and declarative semantics for the first CHR language proposed. Finally, the methodologies to solve the problem of trivial non-termination related to propagation rules are discussed in Section 1.5. Chapter 2 introduces a compositional semantics for CHR where the propagation rules are considered. In particular, Section 2.1 contains the definition of the semantics. Hence, Section 2.2 presents the compositionality results. Afterwards Section 2.3 expounds upon the correctness results. Chapter 3 presents a particular program transformation known as unfolding. This transformation needs a particular syntax called annotated which is introduced in Section 3.1 and its related modified operational semantics !0t is presented in Section 3.2. Subsequently, Section 3.3 defines the unfolding rule and prove its correctness. Then, in Section 3.4 the problems related to the replacement of a rule by its unfolded version are discussed and this in turn gives a correctness condition which holds for a specific class of rules. Section 3.5 proves that confluence and termination are preserved by the program modifications introduced. Finally, Chapter 4 concludes by discussing related works and directions for future work.

Dall'involucro all'invaso. Lo spazio a pianta centrale nell'opera architettonica di Adalberto Libera

An archetype selected over the centuries Adalberto Libera wrote little, showing more inclination to use the project as the only means of verification. This study uses a survey of the project for purely compositional space in relation to the reason that most other returns with continuity and consistency throughout his work. "The fruit of a type selected over centuries", in the words of Libera, is one of the most widely used and repeated spatial archetypes present in the history of architecture, given its nature as defined by a few consolidated elements and precisely defined with characters of geometric precision and absoluteness, the central space is provided, over the course of evolution of architecture, and its construction aspects as well as symbolic, for various uses, from historical period in which it was to coincide with sacred space for excellence, to others in which it lends itself to many different expressive possibilities of a more "secular". The central space was created on assumptions of a constructive character, and the same exact reason has determined the structural changes over the centuries, calling from time to time with advances in technology, the maximum extent possible and the different applications, which almost always have coincided with the reason for the monumental space. But it’s in the Roman world that the reason for the central space is defined from the start of a series of achievements that fix the character in perpetuity. The Pantheon was seen maximum results and, simultaneously, the archetype indispensable, to the point that it becomes difficult to sustain a discussion of the central space that excludes. But the reason the space station has complied, in ancient Rome, just as exemplary, monuments, public spaces or buildings with very different implications. The same Renaissance, on which Wittkower's proving itself once and for all, the nature and interpretation of sacred space station, and thus the symbolic significance of that invaded underlying interpretations related to Humanism, fixing the space-themed drawing it with the study and direct observation by the four-sixteenth-century masters, the ruins that in those years of renewed interest in the classical world, the first big pieces of excavation of ancient Rome brought to light with great surprise of all. Not a case, the choice to investigate the architectural work of Libera through the grounds of the central space. Investigating its projects and achievements, it turns out as the reason invoked particularly evident from the earliest to latest work, crossing-free period of the war which for many authors in different ways, the distinction between one stage and another, or the final miss. The theme and the occasion for Libera always distinct, it is precisely the key through which to investigate her work, to come to discover that the first-in this case the central plan-is the constant underlying all his work, and the second reason that the quota with or at the same time, we will return different each time and always the same Libera, formed on the major works remained from ancient times, and on this building method, means consciously, that the characters of architectural works, if valid, pass the time, and survive the use and function contingent. As for the facts by which to formalize it, they themselves are purely contingent, and therefore available to be transferred from one work to another, from one project to another, using also the loan. Using the same two words-at-issue and it becomes clear now how the theme of this study is the method of Libera and opportunity to the study of the central space in his work. But there is one aspect that, with respect to space a central plan evolves with the progress of the work of Libera on the archetype, and it is the reason behind all the way, just because an area built entirely on reason centric. It 'just the "center" of space that, ultimately, tells us the real progression and the knowledge that over the years has matured and changed in Libera. In the first phase, heavily laden with symbolic superstructure, even if used in a "bribe" from Free-always ill-disposed to sacrifice the idea of architecture to a phantom-center space is just the figure that identifies the icon represents space itself: the cross, the flame or the statue are different representations of the same idea of center built around an icon. The second part of the work of clearing the space station, changed the size of the orders but the demands of patronage, grows and expands the image space centric, celebratory nature that takes and becomes, in a different way, this same symbol . You see, one in all, as the project of "Civiltà Italiana" or symbolic arch are examples of this different attitude. And at the same point of view, you will understand how the two projects formulated on the reuse of the Mausoleum of Augustus is the key to its passage from first to second phase: the Ara Pacis in the second project, making itself the center of the composition "breaks" the pattern of symbolic figure in the center, because it is itself an architecture. And, in doing so, the transition takes place where the building itself-the central space-to become the center of that space that itself creates and determines, by extending the potential and the expressiveness of the enclosure (or cover) that defines the basin centered. In this second series of projects, which will be the apex and the point of "crisis" in the Palazzo dei Congressi all'E42 received and is no longer so, the symbol at the very geometry of space, but space itself and 'action' will be determined within this; action leading a movement, in the case of the Arco simbolico and the "Civiltà Italiana" or, more frequently, or celebration, as in the great Sala dei Recevimenti all’E42, which, in the first project proposal, is represented as a large area populated by people in suits, at a reception, in fact. In other words, in this second phase, the architecture is no longer a mere container, but it represents the shape of space, representing that which "contains". In the next step-determining the knowledge from which mature in their transition to post-war-is one step that radically changes the way centric space, although formally and compositionally Libera continues the work on the same elements, compounds and relationships in a different way . In this last phase Freedom, center, puts the man in human beings, in the two previous phases, and in a latent, were already at the center of the composition, even if relegated to the role of spectators in the first period, or of supporting actors in the second, now the heart of space. And it’s, as we shall see, the very form of being together in the form of "assembly", in its different shades (up to that sacred) to determine the shape of space, and how to relate the parts that combine to form it. The reconstruction of the birth, evolution and development of the central space of the ground in Libera, was born on the study of the monuments of ancient Rome, intersected on fifty years of recent history, honed on the constancy of a method and practice of a lifetime, becomes itself, Therefore, a project, employing the same mechanisms adopted by Libera; the decomposition and recomposition, research synthesis and unity of form, are in fact the structure of this research work. The road taken by Libera is a lesson in clarity and rationality, above all, and this work would uncover at least a fragment.

The relation between geometry and matter in classical and quantum gravity and cosmology

The present thesis is divided into two main research areas: Classical Cosmology and (Loop) Quantum Gravity. The first part concerns cosmological models with one phantom and one scalar field, that provide the `super-accelerated' scenario not excluded by observations, thus exploring alternatives to the standard LambdaCDM scenario. The second part concerns the spinfoam approach to (Loop) Quantum Gravity, which is an attempt to provide a `sum-over-histories' formulation of gravitational quantum transition amplitudes. The research here presented focuses on the face amplitude of a generic spinfoam model for Quantum Gravity.

Deep geometry of subduction below the Andean belt of Colombia as revealed by seismic tomography

In this study new tomographic models of Colombia were calculated. I used the seismicity recorded by the Colombian seismic network during the period 2006-2009. In this time period, the improvement of the seismic network yields more stable hypocentral results with respect to older data set and allows to compute new 3D Vp and Vp/Vs models. The final dataset consists of 10813 P- and 8614 S-arrival times associated to 1405 earthquakes. Tests with synthetic data and resolution analysis indicate that velocity models are well constrained in central, western and southwestern Colombia to a depth of 160 km; the resolution is poor in the northern Colombia and close to Venezuela due to a lack of seismic stations and seismicity. The tomographic models and the relocated seismicity indicate the existence of E-SE subducting Nazca lithosphere beneath central and southern Colombia. The North-South changes in Wadati-Benioff zone, Vp & Vp/Vs pattern and volcanism, show that the downgoing plate is segmented by slab tears E-W directed, suggesting the presence of three sectors. Earthquakes in the northernmost sector represent most of the Colombian seimicity and concentrated on 100-170 km depth interval, beneath the Eastern Cordillera. Here a massive dehydration is inferred, resulting from a delay in the eclogitization of a thickened oceanic crust in a flat-subduction geometry. In this sector a cluster of intermediate-depth seismicity (Bucaramanga Nest) is present beneath the elbow of the Eastern Cordillera, interpreted as the result of massive and highly localized dehydration phenomenon caused by a hyper-hydrous oceanic crust. The central and southern sectors, although different in Vp pattern show, conversely, a continuous, steep and more homogeneous Wadati-Benioff zone with overlying volcanic areas. Here a "normalthickened" oceanic crust is inferred, allowing for a gradual and continuous metamorphic reactions to take place with depth, enabling the fluid migration towards the mantle wedge.

L'Architettura religiosa di Luis Moya Blanco. La costruzione come principio compositivo

La presente ricerca, L’architettura religiosa di Luis Moya Blanco. La costruzione come principio compositivo, tratta i temi inerenti l’edificazione di spazi per il culto della religione cristiana che l’architetto spagnolo progetta e realizza a Madrid dal 1945 al 1970. La tesi è volta ad indagare quali siano i principi alla base della composizione architettonica che si possano considerare immutati, nel lungo arco temporale in cui l’autore si trova ad operare. Tale indagine, partendo da una prima analisi riguardante gli anni della formazione e gli scritti da lui prodotti, verte in particolare sullo studio dei progetti più recenti e ancora poco trattati dalla critica. L’obbiettivo della presente tesi è dunque quello di apportare un contributo originale sull’aspetto compositivo della sua architettura. Ma analizzare la composizione significa, in Moya, analizzare la costruzione che, a dispetto del susseguirsi dei linguaggi, rimarrà l’aspetto principale delle sue opere. Lo studio dei manufatti mediante categorie estrapolate dai suoi stessi scritti – la matematica, il numero, la geometria e i tracciati regolatori - permette di evidenziare punti di contatto e di continuità tra le prime chiese, fortemente caratterizzate da un impianto barocco, e gli ultimi progetti che sembrano cercare invece un confronto con forme decisamente moderne. Queste riflessioni, parallelamente contestualizzate nell’ambito della sua consistente produzione saggistica, andranno a confluire nell’idea finale per cui la costruzione diventi per Luis Moya Blanco il principio compositivo da cui non si può prescindere, la regola che sostanzia nella materia il numero e la geometria. Se la costruzione è dunque la pietrificazione di leggi geometrico-matematiche che sottendono schemi planimetrici; il ricorso allo spazio di origine centrale non risponde all’intenzione di migliorare la liturgia, ma a questioni di tipo filosofico-idealista, che fanno corrispondere alla somma naturalezza della perfezione divina, la somma perfezione della forma circolare o di uno dei suoi derivati come l’ellisse.

Computational tool for three-point hitch geometry optimization

The weight-transfer effect, consisting of the change in dynamic load distribution between the front and the rear tractor axles, is one of the most impairing phenomena for the performance, comfort, and safety of agricultural operations. Excessive weight transfer from the front to the rear tractor axle can occur during operation or maneuvering of implements connected to the tractor through the three-point hitch (TPH). In this respect, an optimal design of the TPH can ensure better dynamic load distribution and ultimately improve operational performance, comfort, and safety. In this study, a computational design tool (The Optimizer) for the determination of a TPH geometry that minimizes the weight-transfer effect is developed. The Optimizer is based on a constrained minimization algorithm. The objective function to be minimized is related to the tractor front-to-rear axle load transfer during a simulated reference maneuver performed with a reference implement on a reference soil. Simulations are based on a 3-degrees-of-freedom (DOF) dynamic model of the tractor-TPH-implement aggregate. The inertial, elastic, and viscous parameters of the dynamic model were successfully determined through a parameter identification algorithm. The geometry determined by the Optimizer complies with the ISO-730 Standard functional requirements and other design requirements. The interaction between the soil and the implement during the simulated reference maneuver was successfully validated against experimental data. Simulation results show that the adopted reference maneuver is effective in triggering the weight-transfer effect, with the front axle load exhibiting a peak-to-peak value of 27.1 kN during the maneuver. A benchmark test was conducted starting from four geometries of a commercially available TPH. As result, all the configurations were optimized by above 10%. The Optimizer, after 36 iterations, was able to find an optimized TPH geometry which allows to reduce the weight-transfer effect by 14.9%.