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.

Kinematic description of the rupture from strong motion data: strategies for a robust inversion

We present a non linear technique to invert strong motion records with the aim of obtaining the final slip and rupture velocity distributions on the fault plane. In this thesis, the ground motion simulation is obtained evaluating the representation integral in the frequency. The Green’s tractions are computed using the discrete wave-number integration technique that provides the full wave-field in a 1D layered propagation medium. The representation integral is computed through a finite elements technique, based on a Delaunay’s triangulation on the fault plane. The rupture velocity is defined on a coarser regular grid and rupture times are computed by integration of the eikonal equation. For the inversion, the slip distribution is parameterized by 2D overlapping Gaussian functions, which can easily relate the spectrum of the possible solutions with the minimum resolvable wavelength, related to source-station distribution and data processing. The inverse problem is solved by a two-step procedure aimed at separating the computation of the rupture velocity from the evaluation of the slip distribution, the latter being a linear problem, when the rupture velocity is fixed. The non-linear step is solved by optimization of an L2 misfit function between synthetic and real seismograms, and solution is searched by the use of the Neighbourhood Algorithm. The conjugate gradient method is used to solve the linear step instead. The developed methodology has been applied to the M7.2, Iwate Nairiku Miyagi, Japan, earthquake. The estimated magnitude seismic moment is 2.6326 dyne∙cm that corresponds to a moment magnitude MW 6.9 while the mean the rupture velocity is 2.0 km/s. A large slip patch extends from the hypocenter to the southern shallow part of the fault plane. A second relatively large slip patch is found in the northern shallow part. Finally, we gave a quantitative estimation of errors associates with the parameters.

Evoluzione Morfotettonica delle Aree Alpine "Sempione" e "Brennero" attraverso Studi Termocronologici di bassa temperatura

E’ mostrata l’analisi e la modellazione di dati termocronologici di bassa temperatura da due regioni Alpine: il Sempione ed il Brennero. Le faglie distensive presenti bordano settori crostali profondi appartenenti al dominio penninico: il duomo metamorfico Lepontino al Sempione e la finestra dei Tauri al Brennero. I dati utilizzati sono FT e (U-Th)/He su apatite. Per il Sempione i dati provengono dalla bibliografia; per il Brennero si è provveduto ad un nuovo campionamento, sia in superficie che in sotterraneo. Gli attuali lavori per la galleria di base del Brennero (BBT), hanno consentito, per la prima volta, di raccogliere dati di FT e (U-Th)/He in apatite in sottosuolo per la finestra dei Tauri occidentale. Le analisi sono state effettuate tramite un codice a elementi finiti, Pecube, risolvente l’equazione di diffusione del calore per una topografia evolvente nel tempo. Il codice è stato modificato per tener conto dei dati sotterranei. L’inversione dei dati è stata effettuata usando il Neighbourhood Algorithm (NA), per ottenere il più plausibile scenario di evoluzione morfotettonico. I risultati ottenuti per il Sempione mostrano: ipotetica evoluzione dello stile tettonico della faglia del Sempione da rolling hinge a low angle detachment a 6.5 Ma e la cessazione dell’attività a 3 Ma; costruzione del rilievo fino a 5.5 Ma, smantellamento da 5.5 Ma ad oggi, in coincidenza dei cambiamenti climatici Messiniani e relativi all’inizio delle maggiori glaciazioni; incremento dell’esumazione da 0–0.6 mm/anno a 0.6–1.2 mm/anno a 2.4 Ma nell’emisfero settentrionale. I risultati al Brennero mostrano: maggiore attività tettonica della faglia del Brennero (1.3 mm/anno), maggiore attività esumativa (1–2 mm/anno) prima dei 10 Ma; crollo dell’attività della faglia del Brennero fra 10 Ma e oggi (0.1 mm/anno) e dell’attività esumativa nello stesso periodo (0.1–0.3 mm/anno); nessun aumento del tasso esumativo o variazioni topografiche negli ultimi 5 Ma.

Le campagne di Piacenza tra VII e IX secolo: insediamenti e comunità

Al centro della seguente ricerca c'è il Piacentino, ossia il territorio che faceva capo alla città di Placentia in età altomedievale, più precisamente tra VII e IX secolo. L'aspetto su cui è concentrata l’analisi è quello dell’insediamento, rapportando le forme insediative alle comunità rurali e alle strutture del potere. Il Piacentino costituisce un contesto particolare, sia per la vicinanza alla capitale Pavia, sia per la presenza di enti patrimoniali molto importanti, quale il monastero di Bobbio, sia per l'estensione di vallate appenniniche che ne hanno protetto l'isolamento e impedito, fino al secolo IX inoltrato, l'insediamento di una forte aristocrazia. Ciò che sembra dedursi dall’analisi della documentazione (informatizzata) di VIII, ma soprattutto di IX secolo, è che la civitas di Piacenza, sede del conte e centro della diocesi, non costituiva di fatto il punto di riferimento per gli abitanti dell’intero territorio rurale. Dal punto di vista del possesso fondiario molti insediamenti erano autonomi. Ciò vale soprattutto per i siti di alcune zone collinari e per quelli dell’Appennino, mentre il discorso è da porsi in modo più sfumato per la pianura e per la zona dei prata vel campanea Placentina, ubicati immediatamente al di fuori della civitas. Lo studio della media e grande proprietà fondiaria ha permesso di registrare la frammentarietà dei possedimenti, ossia la loro dispersione nel sistema insediativo del comitato, la loro ubicazione e l’articolato intreccio proprietario, che in alcune zone sembra avere permesso l’esistenza di comunità locali piuttosto forti. L’attento esame della documentazione e il sicuro rimando alla bibliografia di riferimento hanno portato a risultati originali e significativi.

L’abitare come relazione sociale: il significato della casa e i processi di coesione sociale di vicinato

Se le trasformazioni sociali in atto tendono a esasperare il senso di incertezza, sradicamento ed individualismo, sussistono pratiche che si contrappongono alle tendenze dominanti, finalizzate a ricucire i legami sociali su scala locale. La progettazione urbano-architettonica interiorizza il nuovo bisogno di comunità originando soluzioni abitative tese a favorire gli scambi informali fra vicini, facendo leva sul concetto di capitale sociale, attaccamento al quartiere, identità del luogo e partecipazione. La casa, simbolo di stabilità e sicurezza ma anche di privacy, privatismo familiare, diventa sempre più oggetto di studi, domanda sociale e intervento politico. Soprattutto è sempre più intesa come un nodo di relazioni familiari in una rete di relazioni sociali più ampie. Casa e quartiere incidono nella esperienza di benessere e socialità familiare? In che modo gli spazi urbani e architettonici influenzano la coesione sociale? Quale il ruolo degli abitanti nello sviluppare socialità e integrazione? Sono queste le domande che ci siamo posti per rilevare le dinamiche sociali e culturali dell’abitare attraverso uno studio di caso condotto in due quartieri simili. Dalla ricerca emerge come il significato della casa non sia univoco ma cambi rispetto al ciclo di vita familiare e a quello economico e ciò incide nella partecipazione alle attività di quartiere. Mostriamo inoltre come lo spazio fisico costruito crea importanti opportunità per gli scambi informali e per il benessere familiare e individuale dei bambini ma che, il contesto sociale sia una discriminate fondamentale. Nel quartiere dove è presente una organizzazione di abitanti il numero delle relazioni di vicinato aumenta, cambiano anche la qualità delle relazioni e le distanze fisiche fra i vicini. Emerge inoltre che la reciprocità è il principale strumento di costruzione della coesione comunitaria interna e crea un atteggiamento di apertura e fiducia che va al di là dei confini di quartiere.

La documentazione monetale come fonte per la storia di Classe (Ravenna) Gli scavi condotti nell’area portuale (anni 2001-2005) e nell’area della basilica di San Severo (anni 2006-2010)

Gli scavi effettuati a Classe, a sud di Ravenna, presso i siti archeologici dell'area portuale e della Basilica di San Severo, hanno portato alla luce un numero abbondante di moneta, 2564 dall'area portuale e 224 dalla basilica, un totale di 2788 reperti monetali, di cui solo 863 sono leggibili e databili. La datazione dei materiali dell’area portuale, fondata agli inizi del V secolo, parte dal II secolo a.C. fino all’VIII secolo d.C.. La maggior parte dei reperti è relativa al periodo tra il IV e il VII secolo, il momento di massima importanza del porto commerciale, con testimonianza di scambi con altri porti del bacino mediterraneo, in particolare con l’Africa del Nord e il Vicino Oriente. La documentazione proveniente dalla Basilica di San Severo, fondata alla fine del VI secolo per la custodia delle reliquie del santo, mostra un trend diverso dal precedente, con monetazione che copre un arco cronologico dal I secolo a.C. fino al XIV secolo d.C.. La continuità dell’insediamento è dimostrato dall’evidenza numismatica, seppur scarsa, fino alla costruzione del monastero a sud della basilica, l’area dalla quale provengono la maggior parte delle monete. I quantitativi importanti di monetazione tardoantica, ostrogota e bizantina, in particolare di tipi specifici come il Felix Ravenna, ipoteticamente coniato a Roma, oppure il ½ e il 1/4 di follis di produzione saloniana emesso da Giustiniano I, hanno concesso uno studio dettagliato per quello che riguarda il peso, le dimensioni e lo stile di produzione di queste emissioni. Questi dati e la loro distribuizione sul territorio ha suggerito nuove ipotesi per quello che riguarda la produzione di questi due tipi presso la zecca di Ravenna. Un altro dato importante è il rinvenimento di emissioni di Costantino VIII, alcune rare e altre sconosciute, rinvenute solo nel territorio limitrofo a Classe e Ravenna.

Non-normal modal logics, quantification, and deontic dilemmas. A study in multi-relational semantics

This dissertation is devoted to the study of non-normal (modal) systems for deontic logics, both on the propositional level, and on the first order one. In particular we developed our study the Multi-relational setting that generalises standard Kripke Semantics. We present new completeness results concerning the semantic setting of several systems which are able to handle normative dilemmas and conflicts. Although primarily driven by issues related to the legal and moral field, these results are also relevant for the more theoretical field of Modal Logic itself, as we propose a syntactical, and semantic study of intermediate systems between the classical propositional calculus CPC and the minimal normal modal logic K.