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.

Il criterio di efficienza e l'attività delle autorità antitrust

E’ stato in primo luogo definito il criterio di efficienza dal punto di vista economico (con una accenno anche ai parametri elaborati dagli studiosi di discipline aziendali), nelle sue varie accezioni, ponendo altresì ciascuna di queste in relazione alle condizioni di concorrenza perfetta. Le nozioni di efficienza che sono state definite a tal fine sono quelle di efficienza allocativa, efficienza tecnica, efficienza dinamica ed efficienza distributiva. Ciascuna di esse é stata inquadrata a livello teorico secondo le definizioni fornite dalla letteratura, esaminandone le ipotesi sottostanti. E’ stata altresì descritta, contestualizzandola temporalmente, l’evoluzione della nozione, e ne sono state evidenziate le implicazioni ai fini della ricerca della forma di mercato più “efficiente”. Sotto quest’ultimo aspetto l’attenzione dello scrivente si é incentrata sul rapporto tra le diverse accezioni di efficienza economica oggetto di analisi e la desiderabilità o meno di un regime di concorrenza perfetta. Il capitolo si conclude con una breve panoramica sulle metodologie di misurazione finalizzata ad individuare i principali parametri utilizzati per determinare il livello di efficienza, di un mercato, di un’attività produttiva o di un’impresa, posto che, come verrà specificato nel prosieguo della tesi, la valutazione di efficienza in ambito antitrust deve essere verificata, ove possibile, anche basandosi sull’evidenza empirica delle singole imprese esaminate, come richiede il criterio della rule of reason. Capitolo 2 Presupposto per avere una regolazione che persegua l’obiettivo di avere una regolazione efficiente ed efficace, è, a parere di chi scrive, anche l’esistenza di autorità pubbliche deputate a esercitare la funzione regolatoria che rispettino al proprio interno e nel proprio agire la condizione di efficienza definita rispetto ai pubblici poteri. Lo sviluppo di questa affermazione ha richiesto in via preliminare, di definire il criterio di efficienza in ambito pubblicistico individuandone in particolare l’ambito di applicazione, il suo rapporto con gli altri principi che reggono l’azione amministrativa (con particolare riferimento al criterio di efficacia). Successivamente é stato collocato nel nostro ordinamento nazionale, ponendolo in relazione con il principio di buon andamnento della Pubblica Amministrazione, benchè l’ordinamento italiano, per la sua specificità non costituisca un esempio estendibile ad ordinamenti. Anche con riferimento al criterio di efficienza pubblica, un paragrafo é stato dedicato alle metodologie di misurazione di questa, e, nello specifico sull’Analisi Costi-Benefici e sull’Analisi di Impatto della Regolazione Una volta inquadrata la definizione di efficienza pubblica, questa é stata analizzata con specifico riferimento all’attività di regolazione dell’economia svolta dai soggetti pubblici, ambito nella quale rientra la funzione antitrust. Si é provato in particolare ad evidenziare, a livello generale, quali sono i requisiti necessari ad un’autorità amministrativa antitrust, costituita e dotata di poteri ad hoc, affinché essa agisca, nella sua attività di regolazione, secondo il principio di efficienza, Il capitolo si chiude allargando l’orizzonte della ricerca verso una possibile alternativa metodologica al criterio di efficienza precedentemente definito: vi si é infatti brevemente interrogati circa lo schema interpretativo nel quale ci muoviamo, affrontando la questione definitoria del criterio di efficienza, ponendolo in relazione con l’unico modello alternativo esistente, quello sviluppatosi nella cultura cinese. Non certo per elaborare un’applicazione in “salsa cinese” del criterio di efficienza alla tutela della concorrenza, compito al quale lo scrivente non sarebbe stato in grado di ottemperare, bensì, più semplicemente per dare conto di un diverso approccio alla questione che il futuro ruolo di superpotenza economica della Cina imporrà di prendere in considerazione. Capitolo 3 Nel terzo capitolo si passa a definire il concetto di concorrenza come istituto oggetto di tutela da parte della legge antitrust, per poi descrivere la nascita e l’evoluzione di tale legislazione negli Stati Uniti e della sua applicazione, posto che il diritto antitrust statunitense ancora oggi costituisce il necessario punto di riferimento per lo studioso di questa materia. L’evoluzione del diritto antitrust statunitense é stata analizzata parallelamente allo sviluppo delle principali teorie di law and economics che hanno interpretato il diritto della concorrenza quale possibile strumento per conseguire l’obiettivo dell’efficienza economica: la Scuola di Harvard e il paradigma strutturalista, la teoria evoluzionista della Scuola Austriaca, la Scuola di Chicago; le c.d. teorie “Post-Chicago”. Nel terzo capitolo, in altri termini, si é dato conto dell’evoluzione del pensiero economico con riferimento alla sua applicazione al diritto antitrust, focalizzando l’attenzione su quanto avvenuto negli Stati Uniti, paese nel quale sono nati sia l’istituto giuridico della tutela della concorrenza sia l’analisi economica del diritto. A conclusione di questa ricostruzione dottrinale ho brevemente esaminato quelle che sono le nuove tendenze dell’analisi economica del diritto, e specificatamente la teoria del comportamento irrazionale, benché esse non abbiano ancora ricevuto applicazione al diritto antitrust. Chi scrive ritiene infatti che queste teorie avranno ricadute anche in questa materia poiché essa costituisce uno dei principali ambiti applicativi della law and economics. Capitolo 4 Nel quarto capitolo é stata effettuata una disanima della disciplina comunitaria antitrust sottolineando come l’Unione Europea si proponga attraverso la sua applicazione, soprattutto in materia di intese, di perseguire fini eterogenei, sia economici che non economici, tra loro diversi e non di rado contrastanti, e analizzando come questa eterogeneità di obiettivi abbia influito sull’applicazione del criterio di efficienza. Attenendomi in questo capitolo al dato normativo, ho innanzitutto evidenziato l’ampiezza dell’ambito di applicazione della disciplina comunitaria antitrust sia dal punto di vista soggettivo che territoriale (dottrina dell’effetto utile), sottolineando come la norma giustifichi esplicitamente il ricorso al criterio di efficienza solo nella valutazione delle intese: il comma 3 dell’art. 81 del Trattato include, infatti, tra i requisiti di una possibile esenzione dall’applicazione del divieto per le intese qualificate come restrittive della concorrenza, la possibilità di ottenere incrementi di efficienza tecnica e/o dinamica attraverso l’implementazione delle intese in questione. Tuttavia la previsione da parte dello stesso art. 81 (3) di altri requisiti che devono contemporaneamente essere soddisfatti affinché un intesa restrittiva della concorrenza possa beneficiare dell’esenzione, nonché la possibile diversa interpretazione della locuzione “progresso tecnico ed economico”, impone, o comunque ammette, il perseguimento di altri obiettivi, contestualmente a quello dell’efficienza, giustificando così quell’eterogeneità dei fini che contraddistingue la politica della concorrenza dell’Unione Europea. Se la disciplina delle intese aiuta a comprendere il ruolo del criterio di efficienza nell’applicazione dei precetti antitrust da parte degli organi comunitari, l’art. 82 del Trattato non contiene invece alcun riferimento alla possibilità di utilizzare il criterio di efficienza nella valutazione delle condotte unilaterali poste in essere da imprese in posizione dominante sul mercato rilevante. Si è peraltro dato conto della consultazione recentemente avviata dalla Commissione Europea finalizzata all’elaborazione di Linee Guida che definiscano i criteri di interpretazione che l’organo comunitario dovrà seguire nella valutazione dei comportamenti unilaterali. A parere dello scrivente, anzi, l’assenza di un preciso schema cui subordinare la possibilità di ricorrere al criterio di efficienza nella valutazione della fattispecie, attribuisce alle autorità competenti un più ampio margine di discrezionalità nell’utilizzo del suddetto criterio poiché manca il vincolo della contestuale sussistenza delle altre condizioni di cui all’art. 81(3). Per quanto concerne infine la disciplina delle concentrazioni, essa, come abbiamo visto, prevede un riferimento ai possibili incrementi di efficienza (tecnica e dinamica) derivanti da operazioni di fusione, utilizzando la nozione utilizzata per le intese, così come nel precedente Regolamento 4064/89. Si é infine analizzato il nuovo Regolamento in materia di concentrazioni che avrebbe potuto costituire l’occasione per recepire nella disciplina comunitaria l’attribuzione della facoltà di ricorrere all’efficiency defense in presenza di una fattispecie, quella della fusione tra imprese, suscettibile più di altre di essere valutata secondo il criterio di efficienza, ma che si é invece limitato a riprendere la medesima locuzione presente nell’art. 81(3). Il capitolo attesta anche l’attenzione verso l’istanza di efficienza che ha riguardato il meccanismo di applicazione della norma antitrust e non il contenuto della norma stessa; a questo profilo attiene, infatti, l’innovazione apportata dal Regolamento 1/2003 che ha permesso, a parere dello scrivente, un’attribuzione più razionale della competenza nella valutazione dei casi tra la Commissione e le autorità nazionali degli Stati membri; tuttavia pone alcune questioni che investono direttamente il tema dei criteri di valutazione utilizzati dalle autorità competenti. Capitolo 5 L’analisi del quarto capitolo é stata condotta, sebbene in forma più sintetica, con riferimento alle normative antitrust dei principali Stati membri della Comunità Europea (Germania, Gran Bretagna, Spagna, Francia e Italia), rapportando anche queste al criterio di efficienza, ove possibile. Particolare attenzione é stata dedicata ai poteri e alle competenze attribuite alle autorità nazionali antitrust oggetto di studio dall’ordinamento giuridico cui appartengono e al contesto, in termini di sistema giuridico, nel quale esse operano. Capitolo 6 Si é provato ad effettuare una valutazione del livello di efficienza delle autorità prese in esame, la Commissione e le diverse autorità nazionali e ciò con particolare riferimento alla idoneità di queste a svolgere i compiti istituzionali loro affidati (criterio di efficienza dal punto di vista giuridico): affinchè un’autorità si possa ispirare al criterio di efficienza economica nell’adozione delle decisioni, infatti, è preliminarmente necessario che essa sia idonea a svolgere il compito che le è stato affidato dall’ordinamento. In questo senso si é osservata la difficoltà dei paesi di civil law a inquadrare le autorità indipendenti all’interno di un modello, quello appunto di civil law, ispirato a una rigida tripartizione dei poteri. Da qui la difficile collocazione di queste autorità che, al contrario, costituiscono un potere “ibrido” che esercita una funzione di vigilanza e garanzia non attribuibile integralmente né al potere esecutivo né a quello giurisdizionale. Si rileva inoltre una certa sovrapposizione delle competenze e dei poteri tra autorità antitrust e organi ministeriali, in particolare nel campo delle concentrazioni che ingenera un rischio di confusione e bassa efficienza del sistema. Mantenendo, infatti, un parziale controllo politico si rischia, oltre all’introduzione di criteri di valutazione politica che prescindono dagli effetti delle fattispecie concrete sul livello di concorrenza ed efficienza del mercato, anche di dare luogo a conflitti tra le diverse autorità del sistema che impediscano l’adozione e l’implementazione di decisioni definitive, incrementando altresì i costi dell’intervento pubblico. Un giudizio a parte è stato infine formulato con riguardo alla Commissione Europea, istituzione, in quanto avente caratteristiche e poteri peculiari. Da un lato l’assenza di vincolo di mandato dei Commissari e l’elevata preparazione tecnica dei funzionari costituiscono aspetti che avvicinano la Commissione al modello dell’autorità indipendenti, e l’ampiezza dei poteri in capo ad essa le permette di operare efficientemente grazie anche alla possibilità di valersi dell’assistenza delle autorità nazionali. Dall’altra parte, tuttavia la Commissione si caratterizza sempre di più come un organo politico svolgente funzioni esecutive, di indirizzo e di coordinamento che possono influenzare gli obiettivi che essa persegue attraverso l’attività antitrust, deviandola dal rispetto del criterio di efficienza. Capitolo 7 Una volta definito il contesto istituzionale di riferimento e la sua idoneità a svolgere la funzione affidatagli dall’ordinamento comunitario, nonché da quelli nazionali, si è proceduto quindi all’analisi delle decisioni adottate da alcune delle principali autorità nazionali europee competenti ad applicare la disciplina della concorrenza dal punto di vista dell’efficienza. A tal fine le fattispecie rilevanti a fini antitrust dal punto di vista giuridico sono state classificate utilizzando un criterio economico, individuando e definendo quelle condotte che presentano elementi comuni sotto il profilo economico e per ciascuna di esse sono state inquadrate le problematiche rilevanti ai fini dell’efficienza economica sulla scorta dei contributi teorici e delle analisi empiriche svolte dalla letteratura. 6 Con riferimento a ciascuna condotta rilevante ho esaminato il contenuto di alcune delle decisioni antitrust più significative e le ho interpretate in base al criterio di efficienza. verificando se e in quale misura le autorità antitrust prese in esame utilizzano tale criterio, cercando altresì di valutare l’evoluzione dei parametri di valutazione occorsa nel corso degli anni. Le decisioni analizzate sono soprattutto quelle adottate dalla Commissione e le eventuali relative sentenze della Corte di Giustizia Europea; ciò sia per la maggior rilevanza dei casi trattati a livello comunitario, sia in quanto le autorità nazionali, con qualche rara eccezione, si conformano generalmente ai criteri interpretativi della Commissione. Riferimenti a decisioni adottate dalle autorità nazionali sono stati collocati allorquando i loro criteri interpretativi si discostino da quelli utilizzati dagli organi comunitari. Ne è emerso un crescente, anche se ancora sporadico e incostante, ricorso al criterio di efficienza da parte degli organi europei preposti alla tutela della concorrenza. Il tuttora scarso utilizzo del criterio di efficienza nello svolgimento dell’attività antitrust è motivato, a parere di chi scrive, in parte dall’eterogeneità degli obiettivi che l’Unione Europea persegue attraverso la politica della concorrenza comunitaria (completamento del mercato unico, tutela del consumatore, politica industriale, sviluppo delle aree svantaggiate), in parte dall’incapacità (o dall’impossibilità) delle autorità di effettuare coerenti analisi economiche delle singole fattispecie concrete. Anche le principali autorità nazionali mostrano una crescente propensione a tendere conto dell’efficienza nella valutazione dei casi, soprattutto con riferimento agli accordi verticali e alle concentrazioni, sulla scia della prassi comunitaria. Più innovativa nell’applicazione del criterio di efficienza economica così come nella ricerca di uso ottimale delle risorse si è finora dimostrato l’OFT, come vedremo anche nel prossimo capitolo. Al contrario sembra più lenta l’evoluzione in questo senso dell’Ufficio dei Cartelli tedesco sia a causa delle già citate caratteristiche della legge antitrust tedesca, sia a causa del persistente principio ordoliberale della prevalenza del criterio della rule of law sulla rule of reason. Peraltro, anche nei casi in cui le Autorità siano propense ad utilizzare il criterio di efficienza nelle loro valutazioni, esse si limitano generalmente ad un’analisi teorica dell’esistenza di precondizioni che consentano alle imprese in questione di ottenere guadagni di efficienza. La sussistenza di tali pre-condizioni viene infatti rilevata sulla base della capacità potenziale della condotta dell’impresa (o delle imprese) di avere un effetto positivo in termini di efficienza, nonché sulla base delle caratteristiche del mercato rilevante. Raramente, invece, si tiene conto della capacità reale dei soggetti che pongono in essere la pratica suscettibile di essere restrittiva della concorrenza di cogliere effettivamente queste opportunità, ovvero se la struttura e l’organizzazione interna dell’impresa (o delle imprese) non è in grado di mettere in pratica ciò che la teoria suggerisce a causa di sue carenza interne o comunque in ragione delle strategie che persegue. Capitolo 8 Poiché l’approccio ispirato al criterio di efficienza economica non può prescindere dalle caratteristiche del settore e del mercato in cui operano l’impresa o le imprese che hanno posto in essere la condotta sotto esame, e poiché una valutazione approfondita di tutti i settori non era effettuabile per quantità di decisioni adottate dalle autorità, ho infine ritenuto di svolgere un’analisi dettagliata dell’attività delle autorità con riferimento ad uno specifico settore. La scelta è caduta sul settore dei trasporti in quanto esso presenta alcune problematiche che intrecciano l’esigenza di efficienza con la tutela della concorrenza, nonché per la sua importanza ai fini dello sviluppo economico. Tanto più alla luce del fenomeno della crescente apertura dei mercati che ha enfatizzato la triplice funzione dei trasporti di merci, di livellamento nello spazio dei prezzi di produzione, di redistribuzione nello spazio dell’impiego dei fattori della produzione, e soprattutto di sollecitazione al miglioramento delle tecnologie utilizzate nella produzione stessa in quanto contribuiscono alla divisione territoriale del lavoro e alla specializzazione produttiva. A loro volta, d’altra parte, i miglioramenti tecnici e organizzativi intervenuti nel settore negli ultimi trenta anni hanno reso possibile il fenomeno della globalizzazione nella misura in cui lo conosciamo. Così come le riduzioni di costo e di tempo conseguite nel trasporto di persone hanno consentito massicci spostamenti di lavoratori e più in generale di capitale umano da una parte all’altra del globo, e favorito altresì la spettacolare crescita del settore turistico. Ho quindi condotto un’analisi delle decisioni antitrust relative al settore dei trasporti, suddividendo la casistica in base al comparto al quale esse si riferivano, cercando sempre di non perdere di vista i crescenti legami che esistono tra i vari comparti alla luce dell’ormai affermato fenomeno del trasporto multimodale. Dall’analisi svolta emerge innanzitutto come l’assoggettamento del settore dei trasporti alla disciplina di tutela della concorrenza sia un fenomeno relativamente recente rispetto alle altre attività economiche, laddove la ragione di tale ritardo risiede nel fatto che tradizionalmente questo settore era caratterizzato da un intervento pubblico diretto e da una pervasiva regolamentazione, a sua volta giustificata da vari fattori economici: le caratteristiche di monopolio naturale delle infrastrutture; le esigenze di servizio pubblico connesse all’erogazione di molti servizi di trasporto; il ruolo strategico svolto dal trasporto sia di persone che di merci ai fini della crescita economica di un sistema. Si concretizza, inoltre, con riferimento ai trasporti marittimi e aerei, l’inadeguatezza della dimensione nazionale e comunitaria delle autorità competenti rispetto a comportamenti di impresa che spesso hanno effetti letteralmente globali. Le imprese marittime e aeree coinvolte nelle fattispecie da noi esaminate, infatti, in molti casi predisponevano, direttamente o mediatamente, tramite “alleanze”, collegamenti tra tutte le aree del mondo, individuando nell’Europa solo un nodo di un network ben più ampio Da questa constatazione discende, a parere dello scrivente, l’impossibilità per l’autorità comunitaria e ancor più per quella nazionale di individuare tutti gli effetti in termini di efficienza che la fattispecie concreta può provocare, non includendo pertanto solo quelli evidenti sul mercato comunitario. Conseguentemente una reale applicazione del criterio di efficienza all’attività antitrust nel settore dei trasporti non può prescindere da una collaborazione tra autorità a livello mondiale sia a fini di indagine che a fini di individuazione di alcuni principi fondamentali cui ispirarsi nello svolgimento della loro missione istituzionale. Capitolo 9. Conclusioni L’opera si chiude con l’individuazione delle evidenze e degli elementi emersi dalla trattazione considerati dallo scrivente maggiormente rilevanti nell’ambito dell’attuale dibattito di economia positiva circa le principali problematiche che affiggono l’intervento antitrust con particolare riferimento al suo rispetto del criterio di efficienza. Sono state altresì proposte alcune soluzioni a quelle che sono, a parere dello scrivente, le principali carenze dell’attuale configurazione dell’intervento antitrust a livello europeo, sempre in una prospettiva di efficienza sia delle autorità competenti sia dei mercati in cui le autorità stesse cercano di mantenere o ripristinare condizioni di concorrenza effettiva. Da un lato il modello costituito dalla Commissione Europea, l’autorità antitrust comunitaria, non replicabile né esente da critiche: la Commissione, infatti, rappresenta il Governo dell’Unione Europea e come tale non può ovviamente costituire un esempio di autorità indipendente e neutrale recepibile da parte degli Stati membri. Ciò anche a prescindere dalla questione della sua legittimazione, che in questa sede non affrontiamo. Dall’altro in una prospettiva di efficienza dei mercati la crescente applicazione delle teorie economiche da parte delle autorità esaminate è rimasta a un livello astratto, senza porre la dovuta attenzione alle specificità dei mercati rilevanti né tantomeno alle dinamiche interne alle singole imprese, con particolare riferimento alla loro capacità di rendere effettivi i guadagni di efficienza individuabili a livello potenziale, così come prescrive la più recente teoria economica applicata al diritto antitrust. Sotto il profilo dell’applicazione del criterio di efficienza si può comunque affermare che l’evoluzione che ha avuto la prassi decisionale e la giurisprudenza, comunitaria e degli Stati membri, in materia antitrust è stata caratterizzata dal loro progressivo avvicinamento alle tendenze sviluppatesi nelle agencies e nella giurisprudenza statunitense a partire dagli anni’70, caratterizzate dalla valutazione degli effetti, piuttosto che della forma giuridica, dal riconoscimento del criterio di efficienza e dalla rule of reason quale approccio metodologico. L’effetto è stato quello di determinare una significativa riduzione delle differenze inizialmente emerse tra le due esperienze, nate inizialmente sotto diverse prospettive politiche. Per quanto concerne specificatamente i trasporti sono emersi sotto il profilo economico due aspetti rilevanti, oltre al perdurante ritardo con cui il processo di liberalizzazione del trasporto ferroviario che limita fortemente l’intervento antitrust nel comparto, ma che esula dalla competenza delle stesse autorità antitrust. Il primo consiste nella spesso troppo rigida separazione tra comparti adottata dalle autorità. Il secondo è l’estensivo ricorso all’essential facility doctrine nelle fattispecie riguardanti infrastrutture portuali e aeroportuali: la massimizzazione dell’efficienza dinamica consiglierebbe in questi casi una maggiore cautela, in quanto si tratta di un paradigma che, una volta applicato, disincentiva la duplicazione e l’ampliamento di tali infrastrutture autoalimentandone il carattere di essenzialità. Ciò soprattutto laddove queste infrastrutture possono essere sostituite o duplicate piuttosto facilmente da un punto di vista tecnico (meno da un punto di vista economico e giuridico), essendo esse nodi e non reti. E’stata infine sottolineata l’inadeguatezza della dimensione nazionale e comunitaria delle autorità competenti rispetto a comportamenti di impresa che con riferimento ai trasporti marittimi ed aerei hanno effetti letteralmente globali. E’ di tutta evidenza che le autorità comunitarie e tantomeno quelle nazionali non sono da sole in grado di condurre le analisi quantitative necessarie ad una valutazione di tali condotte ispirata a un criterio di efficienza che tenga conto degli effetti di lungo periodo della fattispecie concreta. Né tali autorità sono sufficientemente neutre rispetto alla nazionalità delle imprese indagate per poter giudicare sulla liceità o meno della condotta in questione senza considerare gli effetti della loro decisione sull’economia interna, rendendo così ancora più improbabile un corretto utilizzo del criterio di efficienza. Da ultimo ho constatato come l’applicazione del concetto di efficienza giuridica imporrebbe di concepire autorità antitrust del tutto nuove, sganciate quanto più possibile dall’elemento territoriale, in grado di elaborare regole e standards minimi comuni e di permettere il controllo dei comportamenti di impresa in un contesto ampliato rispetto al tradizionale mercato unico, nonchè ai singoli mercati nazionali. Il processo di armonizzazione a livello globale è difficile e il quadro che attualmente viene formato è ancora confuso e incompleto. Vi sono tuttavia sparsi segnali attraverso i quali é possibile intravedere i lineamenti di una futura global governance della concorrenza che permetterà, sperabilmente, di incrementare l’efficienza di un sistema, quello antitrust, che tanto più piccolo è l’ambito in cui opera quanto più si sta dimostrando inadeguato a svolgere il compito affidatogli. Solo il futuro, peraltro, ci consentirà di verificare la direzione di sviluppo di questi segnali.

A tuple space implementation for large-scale infrastructures

Coordinating activities in a distributed system is an open research topic. Several models have been proposed to achieve this purpose such as message passing, publish/subscribe, workflows or tuple spaces. We have focused on the latter model, trying to overcome some of its disadvantages. In particular we have applied spatial database techniques to tuple spaces in order to increase their performance when handling a large number of tuples. Moreover, we have studied how structured peer to peer approaches can be applied to better distribute tuples on large networks. Using some of these result, we have developed a tuple space implementation for the Globus Toolkit that can be used by Grid applications as a coordination service. The development of such a service has been quite challenging due to the limitations imposed by XML serialization that have heavily influenced its design. Nevertheless, we were able to complete its implementation and use it to implement two different types of test applications: a completely parallelizable one and a plasma simulation that is not completely parallelizable. Using this last application we have compared the performance of our service against MPI. Finally, we have developed and tested a simple workflow in order to show the versatility of our service.

Self-organising coordination systems

Many research fields are pushing the engineering of large-scale, mobile, and open systems towards the adoption of techniques inspired by self-organisation: pervasive computing, but also distributed artificial intelligence, multi-agent systems, social networks, peer-topeer and grid architectures exploit adaptive techniques to make global system properties emerge in spite of the unpredictability of interactions and behaviour. Such a trend is visible also in coordination models and languages, whenever a coordination infrastructure needs to cope with managing interactions in highly dynamic and unpredictable environments. As a consequence, self-organisation can be regarded as a feasible metaphor to define a radically new conceptual coordination framework. The resulting framework defines a novel coordination paradigm, called self-organising coordination, based on the idea of spreading coordination media over the network, and charge them with services to manage interactions based on local criteria, resulting in the emergence of desired and fruitful global coordination properties of the system. Features like topology, locality, time-reactiveness, and stochastic behaviour play a key role in both the definition of such a conceptual framework and the consequent development of self-organising coordination services. According to this framework, the thesis presents several self-organising coordination techniques developed during the PhD course, mainly concerning data distribution in tuplespace-based coordination systems. Some of these techniques have been also implemented in ReSpecT, a coordination language for tuple spaces, based on logic tuples and reactions to events occurring in a tuple space. In addition, the key role played by simulation and formal verification has been investigated, leading to analysing how automatic verification techniques like probabilistic model checking can be exploited in order to formally prove the emergence of desired behaviours when dealing with coordination approaches based on self-organisation. To this end, a concrete case study is presented and discussed.

Semantic coordination through programmable Tuple spaces

Two of the main features of today complex software systems like pervasive computing systems and Internet-based applications are distribution and openness. Distribution revolves around three orthogonal dimensions: (i) distribution of control|systems are characterised by several independent computational entities and devices, each representing an autonomous and proactive locus of control; (ii) spatial distribution|entities and devices are physically distributed and connected in a global (such as the Internet) or local network; and (iii) temporal distribution|interacting system components come and go over time, and are not required to be available for interaction at the same time. Openness deals with the heterogeneity and dynamism of system components: complex computational systems are open to the integration of diverse components, heterogeneous in terms of architecture and technology, and are dynamic since they allow components to be updated, added, or removed while the system is running. The engineering of open and distributed computational systems mandates for the adoption of a software infrastructure whose underlying model and technology could provide the required level of uncoupling among system components. This is the main motivation behind current research trends in the area of coordination middleware to exploit tuple-based coordination models in the engineering of complex software systems, since they intrinsically provide coordinated components with communication uncoupling and further details in the references therein. An additional daunting challenge for tuple-based models comes from knowledge-intensive application scenarios, namely, scenarios where most of the activities are based on knowledge in some form|and where knowledge becomes the prominent means by which systems get coordinated. Handling knowledge in tuple-based systems induces problems in terms of syntax - e.g., two tuples containing the same data may not match due to differences in the tuple structure - and (mostly) of semantics|e.g., two tuples representing the same information may not match based on a dierent syntax adopted. Till now, the problem has been faced by exploiting tuple-based coordination within a middleware for knowledge intensive environments: e.g., experiments with tuple-based coordination within a Semantic Web middleware (surveys analogous approaches). However, they appear to be designed to tackle the design of coordination for specic application contexts like Semantic Web and Semantic Web Services, and they result in a rather involved extension of the tuple space model. The main goal of this thesis was to conceive a more general approach to semantic coordination. In particular, it was developed the model and technology of semantic tuple centres. It is adopted the tuple centre model as main coordination abstraction to manage system interactions. A tuple centre can be seen as a programmable tuple space, i.e. an extension of a Linda tuple space, where the behaviour of the tuple space can be programmed so as to react to interaction events. By encapsulating coordination laws within coordination media, tuple centres promote coordination uncoupling among coordinated components. Then, the tuple centre model was semantically enriched: a main design choice in this work was to try not to completely redesign the existing syntactic tuple space model, but rather provide a smooth extension that { although supporting semantic reasoning { keep the simplicity of tuple and tuple matching as easier as possible. By encapsulating the semantic representation of the domain of discourse within coordination media, semantic tuple centres promote semantic uncoupling among coordinated components. The main contributions of the thesis are: (i) the design of the semantic tuple centre model; (ii) the implementation and evaluation of the model based on an existent coordination infrastructure; (iii) a view of the application scenarios in which semantic tuple centres seem to be suitable as coordination media.

Numerical analysis of Dielectric Barrier Discharge

A numerical investigation of dielectric barrier discharge aimed to simulate the electro hydro dynamic interaction is presented. A discharge drift diffusive model according to the Townsend avalanche is described and used to duplicate the plasma kinetics of a DBD actuator. The discharge characteristics dependence upon dielectric material and applied voltage are simulated and the EHD force field according to a simplified approach is presented and discussed. The coupling of DBD results with a fluid dynamic code is also shown. Finally, a new non invasive diagnostic technique for EHD interaction based on Schlieren imaging is computationally validated.