Higher-Order Concurrency: Expressiveness and Decidability Results

Higher-order process calculi are formalisms for concurrency in which processes can be passed around in communications. Higher-order (or process-passing) concurrency is often presented as an alternative paradigm to the first order (or name-passing) concurrency of the pi-calculus for the description of mobile systems. These calculi are inspired by, and formally close to, the lambda-calculus, whose basic computational step ---beta-reduction--- involves term instantiation. The theory of higher-order process calculi is more complex than that of first-order process calculi. This shows up in, for instance, the definition of behavioral equivalences. A long-standing approach to overcome this burden is to define encodings of higher-order processes into a first-order setting, so as to transfer the theory of the first-order paradigm to the higher-order one. While satisfactory in the case of calculi with basic (higher-order) primitives, this indirect approach falls short in the case of higher-order process calculi featuring constructs for phenomena such as, e.g., localities and dynamic system reconfiguration, which are frequent in modern distributed systems. Indeed, for higher-order process calculi involving little more than traditional process communication, encodings into some first-order language are difficult to handle or do not exist. We then observe that foundational studies for higher-order process calculi must be carried out directly on them and exploit their peculiarities. This dissertation contributes to such foundational studies for higher-order process calculi. We concentrate on two closely interwoven issues in process calculi: expressiveness and decidability. Surprisingly, these issues have been little explored in the higher-order setting. Our research is centered around a core calculus for higher-order concurrency in which only the operators strictly necessary to obtain higher-order communication are retained. We develop the basic theory of this core calculus and rely on it to study the expressive power of issues universally accepted as basic in process calculi, namely synchrony, forwarding, and polyadic communication.

Molecular architecture of fur binding to iron-induced and - repressed genes in Helicobacter pylori

The ferric uptake regulator protein Fur regulates iron-dependent gene expression in bacteria. In the human pathogen Helicobacter pylori, Fur has been shown to regulate iron-induced and iron-repressed genes. Herein we investigate the molecular mechanisms that control this differential iron-responsive Fur regulation. Hydroxyl radical footprinting showed that Fur has different binding architectures, which characterize distinct operator typologies. On operators recognized with higher affinity by holo-Fur, the protein binds to a continuous AT-rich stretch of about 20 bp, displaying an extended protection pattern. This is indicative of protein wrapping around the DNA helix. DNA binding interference assays with the minor groove binding drug distamycin A, point out that the recognition of the holo-operators occurs through the minor groove of the DNA. By contrast, on the apo-operators, Fur binds primarily to thymine dimers within a newly identified TCATTn10TT consensus element, indicative of Fur binding to one side of the DNA, in the major groove of the double helix. Reconstitution of the TCATTn10TT motif within a holo-operator results in a feature binding swap from an holo-Fur- to an apo-Fur-recognized operator, affecting both affinity and binding architecture of Fur, and conferring apo-Fur repression features in vivo. Size exclusion chromatography indicated that Fur is a dimer in solution. However, in the presence of divalent metal ions the protein is able to multimerize. Accordingly, apo-Fur binds DNA as a dimer in gel shift assays, while in presence of iron, higher order complexes are formed. Stoichiometric Ferguson analysis indicates that these complexes correspond to one or two Fur tetramers, each bound to an operator element. Together these data suggest that the apo- and holo-Fur repression mechanisms apparently rely on two distinctive modes of operator-recognition, involving respectively the readout of a specific nucleotide consensus motif in the major groove for apo-operators, and the recognition of AT-rich stretches in the minor groove for holo-operators, whereas the iron-responsive binding affinity is controlled through metal-dependent shaping of the protein structure in order to match preferentially the major or the minor groove.

Estimating persistent Betti numbers for discrete shape analysis

Persistent Topology is an innovative way of matching topology and geometry, and it proves to be an effective mathematical tool in shape analysis. In order to express its full potential for applications, it has to interface with the typical environment of Computer Science: It must be possible to deal with a finite sampling of the object of interest, and with combinatorial representations of it. Following that idea, the main result claims that it is possible to construct a relation between the persistent Betti numbers (PBNs; also called rank invariant) of a compact, Riemannian submanifold X of R^m and the ones of an approximation U of X itself, where U is generated by a ball covering centered in the points of the sampling. Moreover we can state a further result in which, this time, we relate X with a finite simplicial complex S generated, thanks to a particular construction, by the sampling points. To be more precise, strict inequalities hold only in "blind strips'', i.e narrow areas around the discontinuity sets of the PBNs of U (or S). Out of the blind strips, the values of the PBNs of the original object, of the ball covering of it, and of the simplicial complex coincide, respectively.

An Analysis of Living Conditions in Rural Villages in China. A New Geography of the Country.

Analysts, politicians and international players from all over the world look at China as one of the most powerful countries on the international scenario, and as a country whose economic development can significantly impact on the economies of the rest of the world. However many aspects of this country have still to be investigated. First the still fundamental role played by Chinese rural areas for the general development of the country from a political, economic and social point of view. In particular, the way in which the rural areas have influenced the social stability of the whole country has been widely discussed due to their strict relationship with the urban areas where most people from the countryside emigrate searching for a job and a better life. In recent years many studies have mostly focused on the urbanization phenomenon with little interest in the living conditions in rural areas and in the deep changes which have occurred in some, mainly agricultural provinces. An analysis of the level of infrastructure is one of the main aspects which highlights the principal differences in terms of living conditions between rural and urban areas. In this thesis, I first carried out the analysis through the multivariate statistics approach (Principal Component Analysis and Cluster Analysis) in order to define the new map of rural areas based on the analysis of living conditions. In the second part I elaborated an index (Living Conditions Index) through the Fuzzy Expert/Inference System. Finally I compared this index (LCI) to the results obtained from the cluster analysis drawing geographic maps. The data source is the second national agricultural census of China carried out in 2006. In particular, I analysed the data refer to villages but aggregated at province level.

Trait emotional intelligence: Evidence from italian adolescents and adults

Emotional intelligence (EI) represents an attribute of contemporary attractiveness for the scientific psychology community. Of particular interest for the present thesis are the conundrum related to the representation of this construct conceptualized as a trait (i.e., trait EI), which are in turn reflected in the current lack of agreement upon its constituent elements, posing significant challenges to research and clinical progress. Trait EI is defined as an umbrella personality-alike construct reflecting emotion-related dispositions and self-perceptions. The Trait Emotional Intelligence Questionnaire (TEIQue) was chosen as main measure, given its strong theoretical and psychometrical basis, including superior predictive validity when compared to other trait EI measures. Studies 1 and 2 aimed at validating the Italian 153-items forms of the TEIQue devoted to adolescents and adults. Analyses were done to investigate the structure of the questionnaire, its internal consistencies and gender differences at the facets, factor, and global level of both versions. Despite some low reliabilities, results from Studies 1 and 2 confirm the four-factor structure of the TEIQue. Study 3 investigated the utility of trait EI in a sample of adolescents over internalizing conditions (i.e., symptoms of anxiety and depression) and academic performance (grades at math and Italian language/literacy). Beyond trait EI, concurrent effects of demographic variables, higher order personality dimensions and non-verbal cognitive ability were controlled for. Study 4a and Study 4b addressed analogue research questions, through a meta-analysis and new data in on adults. In the latter case, effects of demographics, emotion regulation strategies, and the Big Five were controlled. Overall, these studies showed the incremental utility of the TEIQue in different domains beyond relevant predictors. Analyses performed at the level of the four-TEIQue factors consistently indicated that its predictive effects were mainly due to the factor Well-Being. Findings are discussed with reference to potential implication for theory and practice.

From emerging adults' unmet psychosocial needs to their problematic use of social networking sites: the mediating role of Fear of Missing Out

Fear of Missing Out (FoMO) is a pervasive apprehension that others might be having rewarding experiences from which one is absent. Consequently, individuals experiencing FoMO wish to stay constantly in contact with what others are doing and engage with social networking sites for this purpose. In recent times, FoMO has received increased attention from psychological research, as a minority of users experiencing high levels of FoMO - particularly young people - might develop a problematic social networking site use, defined as the maladaptive and excessive use of social networking sites, resulting in symptoms associated with other addictions. According to the theoretical framework of the Interaction of Person-Affect-Cognition- Execution (I-PACE) model, FoMO and certain motives for use may foster problematic use in individuals who display unmet psychosocial needs. However, to date, the I-PACE model has only conceptualized the general higher-order mechanisms related to the development of problematic use. Consistently, the overall purpose of this dissertation was to deepen the understanding of the mediating role of FoMO between specific predisposing variables and problematic social networking sites use. Adopting a psychological approach, two empirical and exploratory cross-sectional studies, conceived as independent research, were conducted through path analysis.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Studio e validazione di una nuova metodica per la valutazione dello stato di forma

We observed 82 healthy subjects, from both sexes, aged between 19 and 77 years. All subjects performed two different tests: for being scientifically acknowledged, the first one was used as a reference and it was a stress test (CPX). During the entire test, heart rate and gas exchange were recorded continuously; the second, the actual object of this study, was a submaximal test (TOP). Only heart rate was recorded continuously. The main purpose was to determinate an index of physical fitness as result of TOP. CPX test allowed us to individuate anaerobic threshold. We used an incremental protocol of 10/20 Watt/min, different by age. For our TOP test we used an RHC400 UPRIGHT BIKE, by Air Machine. Each subject was monitored for heart frequency. After 2 minutes of resting period there was a first step: 3 minutes of pedalling at a constant rate of 60 RPM, (40 watts for elder subjects and 60 watts for the younger ones). Then, the subject was allowed to rest for a recovery phase of 5 minutes. Third and last step consisted of 3 minutes of pedalling again at 60 RPM but now set to 60 watts for elder subjects and 80 watts for the young subjects. Finally another five minutes of recovery. A good correlation was found between TOP and CPX results especially between punctua l heart rate reserve (HRR’) and anaerobic threshold parameters such as Watt, VO2, VCO2 . HRR’ was obtained by subtracting maximal heart rate during TOP from maximal theoretic heart rate (206,9-(0,67*age)). Data were analyzed through cluster analysis in order to obtain 3 homogeneous groups. The first group contains the least fit subjects (inactive, women, elderly). The other groups contain the “average fit” and the fittest subjects (active, men, younger). Concordance between test resulted in 83,23%. Afterwards, a linear combinations of the most relevant variables gave us a formula to classify people in the correct group. The most relevant result is that this submaximal test is able to discriminate subjects with different physical condition and to provide information (index) about physical fitness through HRR’. Compared to a traditional incremental stress test, the very low load of TOP, short duration and extended resting period, make this new method suitable to very different people. To better define the TOP index, it is necessary to enlarge our subject sample especially by diversifying the age range.

Politiche Antitrust e crescita economica

Negli ultimi anni le istituzioni e la regolamentazione hanno svolto un ruolo sempre più importante nell’analisi della crescita economica. Tuttavia, non è facile interpretare le istituzioni e gli effetti dei regolamenti sulla crescita attraverso indicatori che tendono a “misurare” le istituzioni. Lo scopo di questa ricerca è analizzare la relazione di lungo periodo tra la crescita economica e la regolamentazione e il ruolo della regolamentazione antitrust sulla crescita economica. La stima econometrica dei modelli di crescita con la concorrenza e gli indicatori di potere di mercato si base su un dataset appositamente costruito che copre 211 Paesi, su un arco temporale massimo di 50 anni (da 1960 a 2009). In particolare, cerchiamo di identificare un quadro analitico volto a integrare l’analisi istituzionale ed economica al fine di valutare il ruolo della regolamentazione e, più in generale, il ruolo delle istituzioni nella crescita economica. Dopo una revisione della letteratura teorica ed empirica sulla crescita e le istituzioni, vi presentiamo l’analisi dell'impatto normativo (RIA) in materia di concorrenza, e analizziamo le principali misure di regolamentazione, la governance e le misure antitrust. Per rispondere alla nostra domanda di ricerca si stimano modelli di crescita prendendo in considerazione tre diverse misure di regolamentazione: la Regulation Impact (RI), la Governance (GOV), e la libertà economica (LIB). Nel modello a effetti fissi, RI, gli effetti della legislazione antitrust sulla crescita economica sono significativi e positivi, e gli effetti di durata antitrust sono significativi, ma negativi. Nel pannel dinamico, GOV, gli effetti dell’indicatore di governance sulla crescita sono notevoli, ma negativo. Nel pannel dinamico, LIB, gli effetti della LIB sono significativi e negativi.

Social learning and action understanding in human observers: contributions of sensori-motor constraints and prior information

The aim of this thesis was to investigate the respective contribution of prior information and sensorimotor constraints to action understanding, and to estimate their consequences on the evolution of human social learning. Even though a huge amount of literature is dedicated to the study of action understanding and its role in social learning, these issues are still largely debated. Here, I critically describe two main perspectives. The first perspective interprets faithful social learning as an outcome of a fine-grained representation of others’ actions and intentions that requires sophisticated socio-cognitive skills. In contrast, the second perspective highlights the role of simpler decision heuristics, the recruitment of which is determined by individual and ecological constraints. The present thesis aims to show, through four experimental works, that these two contributions are not mutually exclusive. A first study investigates the role of the inferior frontal cortex (IFC), the anterior intraparietal area (AIP) and the primary somatosensory cortex (S1) in the recognition of other people’s actions, using a transcranial magnetic stimulation adaptation paradigm (TMSA). The second work studies whether, and how, higher-order and lower-order prior information (acquired from the probabilistic sampling of past events vs. derived from an estimation of biomechanical constraints of observed actions) interacts during the prediction of other people’s intentions. Using a single-pulse TMS procedure, the third study investigates whether the interaction between these two classes of priors modulates the motor system activity. The fourth study tests the extent to which behavioral and ecological constraints influence the emergence of faithful social learning strategies at a population level. The collected data contribute to elucidate how higher-order and lower-order prior expectations interact during action prediction, and clarify the neural mechanisms underlying such interaction. Finally, these works provide/open promising perspectives for a better understanding of social learning, with possible extensions to animal models.

Il principio di continuità nel diritto amministrativo

Il presente lavoro si propone principalmente di fornire un’analisi delle declinazioni assunte dal principio di continuità nel diritto amministrativo, tentando di metterne in luce al contempo le basi fondanti che caratterizzano ogni principio generale e le sfumature più attuali emerse dall’elaborazione della dottrina e della giurisprudenza più recenti. Partendo dal fondamentale presupposto secondo cui la maggior parte degli interpreti si è interessata al principio di continuità in campo amministrativo con prevalente riferimento all’ambito organizzativo-strutturale, si è tentato di estendere l’analisi sino a riconoscervi una manifestazione di principi chiave della funzione amministrativa complessivamente intesa quali efficienza, buon andamento, realizzazione di buoni risultati. La rilevanza centrale della continuità discende dalla sua infinita declinabilità, ma in questo lavoro si insiste particolarmente sul fatto che di essa possono darsi due fondamentali interpretazioni, tra loro fortemente connesse, che si influenzano reciprocamente: a quella che la intende come segno di stabilità perenne, capace di assicurare certezza sul modus operandi delle pubbliche amministrazioni e tutela degli affidamenti da esse ingenerati, si affianca una seconda visione che ne privilegia invece l’aspetto dinamico, interpretandola come il criterio che impone alla P.A. di assecondare la realtà che muta, evolvendo contestualmente ad essa, al fine di assicurare la permanenza del risultato utile per la collettività, in ossequio alla sua missione di cura. In questa prospettiva, il presente lavoro si propone di analizzare, nella sua prima parte, i risultati già raggiunti dall’elaborazione esegetica in materia di continuità amministrativa, con particolare riferimento alle sue manifestazioni nel campo dell’organizzazione e dell’attività amministrative, nonché ad alcune sue espressioni concrete nel settore degli appalti e dei servizi pubblici. La seconda parte è invece dedicata a fornire alcuni spunti ed ipotesi per nuove interpretazioni del principio in chiave sistematica, in relazione a concetti generali quali il tempo, lo spazio e il complessivo disegno progettuale della funzione amministrativa.

Caratterizzazione e simulazione di processi di colata in sabbia di ghise sferoidali

L’oggetto principale delle attività di tesi è la caratterizzazione numerico-sperimentale di processi di colata in sabbia di ghisa sferoidale. Inizialmente è stata effettuata un’approfondita indagine bibliografica per comprendere appieno le problematiche relative all’influenza dei parametri del processo fusorio (composizione chimica, trattamento del bagno, velocità di raffreddamento) sulle proprietà microstrutturali e meccaniche di getti ottenuti e per valutare lo stato dell’arte degli strumenti numerici di simulazione delle dinamiche di solidificazione e di previsione delle microstrutture. Sono state definite, realizzate ed impiegate attrezzature sperimentali di colata per la caratterizzazione di leghe rivolte alla misura ed alla differenziazione delle condizioni di processo, in particolare le velocità di raffreddamento, ed atte a validare strumenti di simulazione numerica e modelli previsionali. Inoltre sono stati progettati ed impiegati diversi sistemi per l’acquisizione ed analisi delle temperature all’interno di getti anche di grandi dimensioni. Lo studio, mediante analisi metallografica, di campioni di materiale ottenuto in condizioni differenziate ha confermato l’effetto dei parametri di processo considerati sulle proprietà microstrutturali quali dimensioni dei noduli di grafite e contenuto di ferrite e perlite. In getti di grandi dimensioni si è riscontrata anche una forte influenza dei fenomeni di macrosegregazione e convezione della lega su microstrutture e difettologie dei getti. Le attività si sono concentrate principalmente nella simulazione numerica FEM dei processi fusori studiati e nell’impiego di modelli empirico-analitici per la previsione delle microstrutture. I dati misurati di temperature di processo e di microstrutture sono stati impiegati per la validazione ed ottimizzazione degli strumenti numerici previsionali impiegati su un ampio intervallo di condizioni di processo. L’impiego di strumenti affidabili di simulazione del processo fusorio, attraverso l’implementazione di correlazioni sperimentali microstrutture-proprietà meccaniche, permette la valutazione di proprietà e difettologie dei getti, fornendo un valido aiuto nell’ottimizzazione del prodotto finito e del relativo processo produttivo.