Search

Trent’anni or sono il concetto di ottimalità venne formulato in senso teorico da Lévy, ma solo un decennio dopo Lamping riesce a darne elegante implementazione algoritmica. Realizza un sistema di riduzione su grafi che si scoprirà poi avere interessanti analogie con la logica lineare presentata nello stesso periodo da Girard. Ma l’ottimalità è davvero ottimale? In altre parole, l’implementazione ottimale del λ calcolo realizzata attraverso i grafi di condivisione, è davvero la migliore strategia di riduzione, in termini di complessità? Dopo anni di infondati dubbi e di immeritato oblìo, alla conferenza LICS del 2007, Baillot, Coppola e Dal Lago, danno una prima risposta positiva, seppur parziale. Considerano infatti il caso particolare delle logiche affini elementare e leggera, che possiedono interessanti proprietà a livello di complessità intrinseca e semplificano l’arduo problema. La prima parte di questa tesi presenta, in sintesi, la teoria dell’ottimalità e la sua implementazione condivisa. La seconda parte affronta il tema della sua complessità, a cominciare da una panoramica dei più importanti risultati ad essa legati. La successiva introduzione alle logiche affini, e alle relative caratteristiche, costituisce la necessaria premessa ai due capitoli successivi, che presentano una dimostrazione alternativa ed originale degli ultimi risultati basati appunto su EAL e LAL. Nel primo dei due capitoli viene definito un sistema intermedio fra le reti di prova delle logiche e la riduzione dei grafi, nel secondo sono dimostrate correttezza ed ottimalità dell’implementazione condivisa per mezzo di una simulazione. Lungo la trattazione sono offerti alcuni spunti di riflessione sulla dinamica interna della β riduzione riduzione e sui suoi legami con le reti di prova della logica lineare.

Presentiamo la classe di modelli di computazione astratti delle Macchine a puntatori mettendole in relazione con i classici modelli computazionali.In particolare ci chiediamo se appartengano alla classe descritta della Tesi di Invarianza. A questo scopo illustriamo la simulazioni di una Macchina di Turing attraverso una Macchina di Schönhage e presentiamo alcuni teoremi riguardanti l'utilizzo dello spazio. Questi risultati mettono in luce come le macchine a puntatori possano essere considerate più potenti rispetto alle Macchine di Turing e alle RAM. Presentiamo poi le Macchine di Kolmogorv-Uspensky, le prime macchine a puntatori inventate, mettendo in luce la riflessione che ne ha portato all'ideazione. Ne presentiamo infine una implementazione biologica tramite il Physarum Polycephalum con l'intento di mostrare come questo modello, grazie alla sua particolare struttura, si presti ad essere un utile strumento per la comprensione di sistemi fisici.

Nell'ultimo decennio il trend topic nell'ambito dell'insegnamento dell'informatica è il pensiero computazionale. Concetto già presente, è stato risaltato nel 2006 da Jeannette Wing, che ha mostrato come l'informatica abbia portato alla scienza non solo strumenti (computer e linguaggi di programmazione) ma anche innovazioni nel modo di pensare (es. algoritmo shotgun per sequenziamento del DNA umano). Il pensiero computazionale è il processo mentale coinvolto nel formulare problemi e loro soluzioni, rappresentate in una forma che sia effettivamente eseguibile da un agente che processa informazioni. Si tratta di “pensare come un informatico” quando si affronta un problema. Dopo aver passato in rassegna la letteratura sul pensiero computazionale, viene proposta una definizione del concetto. Si prende atto che la ricerca in questi anni sia rimasta molto legata ai linguaggi di programmazione, concetto centrale dell’Informatica. Vengono allora proposte due strade. La prima strada consiste nella riesumazione di tutta una serie di studi di Psicologia della Programmazione, in particolare: studi sulle misconcezioni, che si occupano di individuare i concetti che sono compresi male dai programmatori novizi, e studi sul commonsense computing, che cercano di capire come persone che non hanno mai ricevuto nozioni di programmazione - o più in generale di informatica – esprimano (in linguaggio naturale) concetti e processi computazionali. A partire da queste scoperte, si forniscono una serie di consigli per insegnare al meglio la programmazione (con i linguaggi attuali, con nuovi linguaggi appositamente progettati, con l'aiuto di strumenti ed ambienti ad-hoc) al più ampio pubblico possibile. La seconda strada invece porta più lontano: riconoscere il pensiero computazionale come quarta abilità di base oltre a leggere, scrivere e calcolare, dandogli dunque grande importanza nell’istruzione. Si vuole renderlo “autonomo” rispetto alla programmazione, fornendo consigli su come insegnarlo

La presente tesi è incentrata sui principi di rappresentazione digitale attraverso l’utilizzo dei LEGO. Negli anni l’insegnamento dell’informatica è andato sempre più ad evolversi, da una materia per poche persone, sta diventando una disciplina da insegnare anche ai bambini più piccoli, al fine di introdurre da subito i suoi principi. Il principale obiettivo della tesi è quello di spiegare il mondo binario sfruttando i LEGO, sfruttandone le caratteristiche in termini di duttilità, forme e colori. Questo elaborato propone attraverso l’uso dei LEGO, un metodo di insegnamento innovativo attraverso l’utilizzo del concetto di un mondo formato solamente da 0 e da 1 chiamato mondo binario e volto ad introdurre ai bambini classificati K-6, attraverso la facilitazione del metodo d’apprendimento, la conoscenza dei numeri binari e delle operazioni elementari. Infatti è stato delineato il metodo per spiegare i numeri binari e le loro proprietà utilizzando proprio “mattoncini preferiti” attraverso tre regole da seguire per poter “costruire” un numero binario con i LEGO e dopo aver definito come “creare” i numeri binari partendo da dei semplici pezzi LEGO, è stato trovato il modo di trasformare questi numeri in base decimale, associando ad ogni numero in binario il suo corrispondente numero in decimale e infine è sorta anche la procedura per capire le varie operazioni elementari quali somma e differenza binaria. Sfruttando quindi le caratteristiche principali dei LEGO e lavorando su metodi e scritti già presenti in varie aree di interesse informatico (logico, matematico, creativo) è stato proposto un metodo semplice ed efficace per facilitare l’apprendimento degli argomenti come la conoscenza dei numeri binari e delle operazioni elementari.

The research and development of embodied agents with advanced relational capabilities is constantly evolving. In recent years, the development of behavioural signal generation models to be integrated in social robots and virtual characters, is moving from rule-based to data-driven approaches, requiring appropriate and reliable evaluation techniques. This work proposes a novel machine learning approach for the evaluation of speech-to-gestures models that is independent from the audio source. This approach enables the measurement of the quality of gestures produced by these models and provides a benchmark for their evaluation. Results show that the proposed approach is consistent with evaluations made through user studies and, furthermore, that its use allows for a reliable comparison of speech-to-gestures state-of-the-art models.

Nell'ambito delle neuroscienze vengono effettuati sempre più studi al fine di comprendere meglio le reti cerebrali e le loro dinamiche. La comunità scientifica ha condotto numerosi studi ed esperimenti sulle normali funzioni cerebrali umane, ma solo recentemente un discreto numero di ricercatori ha rivolto la propria attenzione all'analisi di diversi disturbi cerebrali, tra cui i disturbi della coscienza (Disorders of Consciousness o DoC). Un DoC è uno stato in cui viene meno la capacità psichica e cognitiva della persona e quest'ultima non mostra segni di veglia e/o di consapevolezza. Questa tesi mira a sviluppare un modello che consente di analizzare la connettività neurale tra le diverse aree cerebrali e fare inferenze sullo stato dei pazienti affetti da DOC al fine di supportare e affiancare gli attuali criteri diagnostici e migliorare così il processo decisionale medico. L'approccio utilizzato per raggiungere questo obiettivo si basa sul concetto di causalità di Granger (G-causality). Questo metodo permette l'identificazione delle interazioni causali all'interno del cervello e può essere tracciato attraverso un modello autoregressivo a media mobile (ARMA) basato sull'algoritmo delle trasformazioni di Fourier (FT). In particolare, in questa tesi è stata implementata una peculiare normalizzazione della G-causality denominata coerenza parziale diretta (PDC). La PDC mira a stimare la connettività tra coppie di neuroni e i risultati mostrano quanto siano forti tali connessioni, permettendo così l'identificazione di pattern e la comparazione fra i diversi stati tipici dei disturbi della coscienza.

Molti metodi di compressione lossless si basano sulle idee che nel 1977 i ricercatori israeliani Abraham Lempel e Jacob Ziv hanno presentato nell’articolo “A universal Algorithm for sequential Data Compression”. In questa tesi viene descritto il metodo di fattorizzazione LZ77, illustrato appunto da Lempel e Ziv, e vengono esposte le strutture dati fondamentali per la sua realizzazione. Sono inoltre descritti due algoritmi CPS1 e CPS2 che realizzano LZ77. Infine, sfruttando i dati raccolti sperimentalmente da Al-Haffedh et al. in “A Comparison of Index-Based Lempel-Ziv LZ77 Factorization Algorithms” [2012], gli algoritmi descritti vengono confrontati in termini di spazio e tempo.

In questa tesi è trattato il tema della soddisfacibilità booleana o proposizionale, detta anche SAT, ovvero il problema di determinare se una formula booleana è soddisfacibile o meno. Soddisfacibile significa che è possibile assegnare le variabili in modo che la formula assuma il valore di verità vero; viceversa si dice insoddisfacibile se tale assegnamento non esiste e se quindi la formula esprime una funzione identicamente falsa. A tal fine si introducono degli strumenti preliminari che permetteranno di affrontare più approfonditamente la questione, partendo dalla definizione basilare di macchina di Turing, affrontando poi le classi di complessità e la riduzione, la nozione di NP-completezza e si dimostra poi che SAT è un problema NP-completo. Infine è fornita una definizione generale di SAT-solver e si discutono due dei principali algoritmi utilizzati a tale scopo.

Partiamo dal lavoro di Kolmogorov per definire una misura della quantità di informazione contenuta in una stringa tramite un approccio computazionale: la complessità di una stringa è la lunghezza del più corto programma capace di produrla. Vediamo poi gli sviluppi moderni di questa teoria, in particolare i contributi di Chaitin, e notiamo subito i forti legami con la teoria della probabilità e con l'entropia di Shannon. Successivamente proponiamo di identificare le stringhe casuali (nel senso intuitivo) con quelle algoritmicamente incomprimibili, seguendo l'idea che minore comprimibilità significhi minore regolarità e dunque maggiore casualità. Infine vediamo che, in effetti, le stringhe incomprimibili soddisfano tutte le proprietà stocastiche effettivamente verificabili, cioè le proprietà che la teoria della probabilità attribuisce a successioni di variabili aleatorie indipendenti e identicamente distribuite. Facciamo ciò in maniera generale utilizzando la notevole teoria di Martin-Löf e poi vediamo in dettaglio l'aspetto della normalità di Borel.

Partendo dallo studio del modello computazionale introdotto da Schönhage, la presente tesi si propone di fornire una simulazione delle Evolving Graph Structures di Leivant e Marion che ne conservi le proprietà in termini di complessità computazionale.

La trattazione è volta all'esposizione dell'algoritmo di Lindell per determinare in logspazio se due alberi sono isomorfi. Un'ampia parte introduttiva richiama i prerequisiti teorici necessari alla comprensione della parte di esposizione dell'algoritmo.

Nella tesi vengono descritte le caratteristiche principali del linguaggio di programmazione service-oriented Jolie, analizzandone ampiamente la sintassi e proponendo esempi di utilizzo degli operatori e dei costrutti. Viene fatta una panoramica di SOC, SOA, Web Services, Cloud Computing, Orchestrazione, Coreografia, Deployment e Behaviour, gli ultimi due analizzati in diversi capitoli. La tesi si conclude con un esempio di conversione di servizi WSDL in Jolie, producendo un esempio di utilizzo del Web Service convertito. Nel documento vengono accennati i progressi storici del linguaggio ed i loro sviluppatori, nonché le API fornite dal linguaggio.

Questa tesi vuole fornire un'introduzione alla complessità computazionale e allo studio dei numeri primi riferito a questa materia. Si tratterà della Macchina di Turing e della sua importanza per calcolabilità e complessità, introducendo le classi P ed NP. Queste saranno approfondite studiando prima la classe di problemi NP-completi e successivamente fornendo alcuni esempi importanti. Nella parte finale ci si occuperà esplicitamente del problema dei numeri primi e si guarderà da vicino l'algoritmo AKS, dimostrandone la correttezza.

Indagine sulla varietà sintattica presente all'interno dei formalismi di specifica della semantica operazionale strutturale (SOS) di linguaggi di programmazione e calcolo di processi. Rassegna di tool di implementazione con attenzione al grado di copertura linguistica.

La tesi è uno studio di alcuni aspetti della nuova metodologia “deep inference”, abbinato ad una rivisitazione dei concetti classici di proof theory, con l'aggiunta di alcuni risultati originali orientati ad una maggior comprensione dell'argomento, nonché alle applicazioni pratiche. Nel primo capitolo vengono introdotti, seguendo un approccio di stampo formalista (con alcuni spunti personali), i concetti base della teoria della dimostrazione strutturale – cioè quella che usa strumenti combinatoriali (o “finitistici”) per studiare le proprietà delle dimostrazioni. Il secondo capitolo focalizza l'attenzione sulla logica classica proposizionale, prima introducendo il calcolo dei sequenti e dimostrando il Gentzen Hauptsatz, per passare poi al calcolo delle strutture (sistema SKS), dimostrando anche per esso un teorema di eliminazione del taglio, appositamente adattato dall'autore. Infine si discute e dimostra la proprietà di località per il sistema SKS. Un percorso analogo viene tracciato dal terzo ed ultimo capitolo, per quanto riguarda la logica lineare. Viene definito e motivato il calcolo dei sequenti lineari, e si discute del suo corrispettivo nel calcolo delle strutture. L'attenzione qui è rivolta maggiormente al problema di definire operatori non-commutativi, che mettono i sistemi in forte relazione con le algebre di processo.

Dalla pubblicazione dell’opera seminale di Seymour Papert, Mindstorms, ad oggi abbiamo assistito a un aumento esponenziale della tecnologia che, sempre di più, è presente in ogni aspetto della nostra vita. È Jeannette Wing che, nel 2006, pubblica l'articolo Computational Thinking e rimarca l'attenzione sull'importanza dello sviluppo del pensiero computazionale e segna l'inizio di un percorso che porterà molti paesi ad apportare modifiche ai propri programmi scolastici in modo che tutti gli studenti diventino cittadini attivi di una società sempre più tecnologica. Il rinnovato interesse per l'informatica e in particolare per la programmazione porta a riflettere sulle potenzialità che esse possono avere nell'insegnamento e nell'apprendimento. La programmazione permette di rendere la matematica più concreta ed accessibile agli studenti, per questo motivo la tesi propone alcune unità didattiche per la costruzione di un curricolo integrato di matematica e programmazione per la scuola secondaria di secondo grado, essa vuole essere solo un punto di partenza per usare la programmazione come rinforzo per l'apprendimento della matematica. Dopo aver analizzato nel primo capitolo il contributo di Seymour Papert e altri ricercatori che, come lui, volevano studiare gli effetti dell'uso del computer nell'apprendimento, nel secondo capitolo abbiamo descritto le principali teorie dello sviluppo al fine di contestualizzare la teoria Costruzionista dell'apprendimento sviluppata dallo stesso Papert. Nel terzo capitolo entriamo nel vivo della tesi descrivendo le nostre proposte di unità didattiche per l'apprendimento dell'aritmetica modulare, del principio di induzione e della probabilità.

Scanning people and generating realistic face models is becoming nowadays an important branch in Computer Graphics. The main applications are the creation of 3D selfies that can be immediately viewed or printed in 3D, the creation of 3D avatars for augmented or virtual reality applications, content creation for games or movies, or the developing of 3D face authentication algorithms (more robust respect to the 2D counterpart). This thesis provides an overview on a common issue that arises when scanning people wearing glasses and in turn proposes different solutions to solve or at least bypass the original problem, showing the strengths and the weaknesses. Distinct techniques for automatically putting a pair of glasses on a human face are also present. Furthermore, a study on the physical properties of glasses is documented, involving both the frame and the lenses, along with a brief description of the Blender software and its main features that were essential during the development.

Dopo aver illustrato i concetti chiave della teoria delle varie classi di complessità computazionale, l'elaborato si pone come obiettivo quello di inserire in una classe di complessità il seguente problema: "Quanto è difficile salvare la principessa in Super Mario Bros?". Analizzeremo 3 varianti diversi del gioco, e per ognuna di essi daremo un risultato.

Many sonification systems face a number of common design challenges. These are addressed in every project with different, specific-purpose solutions. We present Panson – an interactive sonification framework implemented in Python that can ease the development of sonification systems. Panson allows the user to implement sonifications using the sc3nb library as interface to the SuperCollider sound synthesis engine. The framework provides support for both offline and online (real-time) sonification through a set of composable classes; these classes are designed to natively support interaction in Jupyter Notebooks. Using Panson, we will show an example of its application by implementing a facial expression sonification Jupyter Notebook based on OpenFace 2.0.

La presente tesi è incentrata sui principi di rappresentazione digitale attraverso l’utilizzo dei LEGO. Negli anni l’insegnamento dell’informatica è andato sempre più ad evolversi, da una materia per poche persone, sta diventando una disciplina da insegnare anche ai bambini più piccoli, al fine di introdurre da subito i suoi principi. Il principale obiettivo della tesi è quello di spiegare il mondo binario sfruttando i LEGO, sfruttandone le caratteristiche in termini di duttilità, forme e colori. Questo elaborato propone attraverso l’uso dei LEGO, un metodo di insegnamento innovativo attraverso l’utilizzo del concetto di un mondo formato solamente da 0 e da 1 chiamato mondo binario e volto ad introdurre ai bambini classificati K-6, attraverso la facilitazione del metodo d’apprendimento, la conoscenza dei numeri binari e delle operazioni elementari. Infatti è stato delineato il metodo per spiegare i numeri binari e le loro proprietà utilizzando proprio “mattoncini preferiti” attraverso tre regole da seguire per poter “costruire” un numero binario con i LEGO e dopo aver definito come “creare” i numeri binari partendo da dei semplici pezzi LEGO, è stato trovato il modo di trasformare questi numeri in base decimale, associando ad ogni numero in binario il suo corrispondente numero in decimale e infine è sorta anche la procedura per capire le varie operazioni elementari quali somma e differenza binaria. Sfruttando quindi le caratteristiche principali dei LEGO e lavorando su metodi e scritti già presenti in varie aree di interesse informatico (logico, matematico, creativo) è stato proposto un metodo semplice ed efficace per facilitare l’apprendimento degli argomenti come la conoscenza dei numeri binari e delle operazioni elementari.

The research and development of embodied agents with advanced relational capabilities is constantly evolving. In recent years, the development of behavioural signal generation models to be integrated in social robots and virtual characters, is moving from rule-based to data-driven approaches, requiring appropriate and reliable evaluation techniques. This work proposes a novel machine learning approach for the evaluation of speech-to-gestures models that is independent from the audio source. This approach enables the measurement of the quality of gestures produced by these models and provides a benchmark for their evaluation. Results show that the proposed approach is consistent with evaluations made through user studies and, furthermore, that its use allows for a reliable comparison of speech-to-gestures state-of-the-art models.

Nell'ambito delle neuroscienze vengono effettuati sempre più studi al fine di comprendere meglio le reti cerebrali e le loro dinamiche. La comunità scientifica ha condotto numerosi studi ed esperimenti sulle normali funzioni cerebrali umane, ma solo recentemente un discreto numero di ricercatori ha rivolto la propria attenzione all'analisi di diversi disturbi cerebrali, tra cui i disturbi della coscienza (Disorders of Consciousness o DoC). Un DoC è uno stato in cui viene meno la capacità psichica e cognitiva della persona e quest'ultima non mostra segni di veglia e/o di consapevolezza. Questa tesi mira a sviluppare un modello che consente di analizzare la connettività neurale tra le diverse aree cerebrali e fare inferenze sullo stato dei pazienti affetti da DOC al fine di supportare e affiancare gli attuali criteri diagnostici e migliorare così il processo decisionale medico. L'approccio utilizzato per raggiungere questo obiettivo si basa sul concetto di causalità di Granger (G-causality). Questo metodo permette l'identificazione delle interazioni causali all'interno del cervello e può essere tracciato attraverso un modello autoregressivo a media mobile (ARMA) basato sull'algoritmo delle trasformazioni di Fourier (FT). In particolare, in questa tesi è stata implementata una peculiare normalizzazione della G-causality denominata coerenza parziale diretta (PDC). La PDC mira a stimare la connettività tra coppie di neuroni e i risultati mostrano quanto siano forti tali connessioni, permettendo così l'identificazione di pattern e la comparazione fra i diversi stati tipici dei disturbi della coscienza.

Dalla pubblicazione dell’opera seminale di Seymour Papert, Mindstorms, ad oggi abbiamo assistito a un aumento esponenziale della tecnologia che, sempre di più, è presente in ogni aspetto della nostra vita. È Jeannette Wing che, nel 2006, pubblica l'articolo Computational Thinking e rimarca l'attenzione sull'importanza dello sviluppo del pensiero computazionale e segna l'inizio di un percorso che porterà molti paesi ad apportare modifiche ai propri programmi scolastici in modo che tutti gli studenti diventino cittadini attivi di una società sempre più tecnologica. Il rinnovato interesse per l'informatica e in particolare per la programmazione porta a riflettere sulle potenzialità che esse possono avere nell'insegnamento e nell'apprendimento. La programmazione permette di rendere la matematica più concreta ed accessibile agli studenti, per questo motivo la tesi propone alcune unità didattiche per la costruzione di un curricolo integrato di matematica e programmazione per la scuola secondaria di secondo grado, essa vuole essere solo un punto di partenza per usare la programmazione come rinforzo per l'apprendimento della matematica. Dopo aver analizzato nel primo capitolo il contributo di Seymour Papert e altri ricercatori che, come lui, volevano studiare gli effetti dell'uso del computer nell'apprendimento, nel secondo capitolo abbiamo descritto le principali teorie dello sviluppo al fine di contestualizzare la teoria Costruzionista dell'apprendimento sviluppata dallo stesso Papert. Nel terzo capitolo entriamo nel vivo della tesi descrivendo le nostre proposte di unità didattiche per l'apprendimento dell'aritmetica modulare, del principio di induzione e della probabilità.

Presentiamo la classe di modelli di computazione astratti delle Macchine a puntatori mettendole in relazione con i classici modelli computazionali.In particolare ci chiediamo se appartengano alla classe descritta della Tesi di Invarianza. A questo scopo illustriamo la simulazioni di una Macchina di Turing attraverso una Macchina di Schönhage e presentiamo alcuni teoremi riguardanti l'utilizzo dello spazio. Questi risultati mettono in luce come le macchine a puntatori possano essere considerate più potenti rispetto alle Macchine di Turing e alle RAM. Presentiamo poi le Macchine di Kolmogorv-Uspensky, le prime macchine a puntatori inventate, mettendo in luce la riflessione che ne ha portato all'ideazione. Ne presentiamo infine una implementazione biologica tramite il Physarum Polycephalum con l'intento di mostrare come questo modello, grazie alla sua particolare struttura, si presti ad essere un utile strumento per la comprensione di sistemi fisici.

Scanning people and generating realistic face models is becoming nowadays an important branch in Computer Graphics. The main applications are the creation of 3D selfies that can be immediately viewed or printed in 3D, the creation of 3D avatars for augmented or virtual reality applications, content creation for games or movies, or the developing of 3D face authentication algorithms (more robust respect to the 2D counterpart). This thesis provides an overview on a common issue that arises when scanning people wearing glasses and in turn proposes different solutions to solve or at least bypass the original problem, showing the strengths and the weaknesses. Distinct techniques for automatically putting a pair of glasses on a human face are also present. Furthermore, a study on the physical properties of glasses is documented, involving both the frame and the lenses, along with a brief description of the Blender software and its main features that were essential during the development.

Molti metodi di compressione lossless si basano sulle idee che nel 1977 i ricercatori israeliani Abraham Lempel e Jacob Ziv hanno presentato nell’articolo “A universal Algorithm for sequential Data Compression”. In questa tesi viene descritto il metodo di fattorizzazione LZ77, illustrato appunto da Lempel e Ziv, e vengono esposte le strutture dati fondamentali per la sua realizzazione. Sono inoltre descritti due algoritmi CPS1 e CPS2 che realizzano LZ77. Infine, sfruttando i dati raccolti sperimentalmente da Al-Haffedh et al. in “A Comparison of Index-Based Lempel-Ziv LZ77 Factorization Algorithms” [2012], gli algoritmi descritti vengono confrontati in termini di spazio e tempo.

In questa tesi è trattato il tema della soddisfacibilità booleana o proposizionale, detta anche SAT, ovvero il problema di determinare se una formula booleana è soddisfacibile o meno. Soddisfacibile significa che è possibile assegnare le variabili in modo che la formula assuma il valore di verità vero; viceversa si dice insoddisfacibile se tale assegnamento non esiste e se quindi la formula esprime una funzione identicamente falsa. A tal fine si introducono degli strumenti preliminari che permetteranno di affrontare più approfonditamente la questione, partendo dalla definizione basilare di macchina di Turing, affrontando poi le classi di complessità e la riduzione, la nozione di NP-completezza e si dimostra poi che SAT è un problema NP-completo. Infine è fornita una definizione generale di SAT-solver e si discutono due dei principali algoritmi utilizzati a tale scopo.

Partiamo dal lavoro di Kolmogorov per definire una misura della quantità di informazione contenuta in una stringa tramite un approccio computazionale: la complessità di una stringa è la lunghezza del più corto programma capace di produrla. Vediamo poi gli sviluppi moderni di questa teoria, in particolare i contributi di Chaitin, e notiamo subito i forti legami con la teoria della probabilità e con l'entropia di Shannon. Successivamente proponiamo di identificare le stringhe casuali (nel senso intuitivo) con quelle algoritmicamente incomprimibili, seguendo l'idea che minore comprimibilità significhi minore regolarità e dunque maggiore casualità. Infine vediamo che, in effetti, le stringhe incomprimibili soddisfano tutte le proprietà stocastiche effettivamente verificabili, cioè le proprietà che la teoria della probabilità attribuisce a successioni di variabili aleatorie indipendenti e identicamente distribuite. Facciamo ciò in maniera generale utilizzando la notevole teoria di Martin-Löf e poi vediamo in dettaglio l'aspetto della normalità di Borel.

La trattazione è volta all'esposizione dell'algoritmo di Lindell per determinare in logspazio se due alberi sono isomorfi. Un'ampia parte introduttiva richiama i prerequisiti teorici necessari alla comprensione della parte di esposizione dell'algoritmo.

Partendo dallo studio del modello computazionale introdotto da Schönhage, la presente tesi si propone di fornire una simulazione delle Evolving Graph Structures di Leivant e Marion che ne conservi le proprietà in termini di complessità computazionale.

Nell'ultimo decennio il trend topic nell'ambito dell'insegnamento dell'informatica è il pensiero computazionale. Concetto già presente, è stato risaltato nel 2006 da Jeannette Wing, che ha mostrato come l'informatica abbia portato alla scienza non solo strumenti (computer e linguaggi di programmazione) ma anche innovazioni nel modo di pensare (es. algoritmo shotgun per sequenziamento del DNA umano). Il pensiero computazionale è il processo mentale coinvolto nel formulare problemi e loro soluzioni, rappresentate in una forma che sia effettivamente eseguibile da un agente che processa informazioni. Si tratta di “pensare come un informatico” quando si affronta un problema. Dopo aver passato in rassegna la letteratura sul pensiero computazionale, viene proposta una definizione del concetto. Si prende atto che la ricerca in questi anni sia rimasta molto legata ai linguaggi di programmazione, concetto centrale dell’Informatica. Vengono allora proposte due strade. La prima strada consiste nella riesumazione di tutta una serie di studi di Psicologia della Programmazione, in particolare: studi sulle misconcezioni, che si occupano di individuare i concetti che sono compresi male dai programmatori novizi, e studi sul commonsense computing, che cercano di capire come persone che non hanno mai ricevuto nozioni di programmazione - o più in generale di informatica – esprimano (in linguaggio naturale) concetti e processi computazionali. A partire da queste scoperte, si forniscono una serie di consigli per insegnare al meglio la programmazione (con i linguaggi attuali, con nuovi linguaggi appositamente progettati, con l'aiuto di strumenti ed ambienti ad-hoc) al più ampio pubblico possibile. La seconda strada invece porta più lontano: riconoscere il pensiero computazionale come quarta abilità di base oltre a leggere, scrivere e calcolare, dandogli dunque grande importanza nell’istruzione. Si vuole renderlo “autonomo” rispetto alla programmazione, fornendo consigli su come insegnarlo

Nella tesi vengono descritte le caratteristiche principali del linguaggio di programmazione service-oriented Jolie, analizzandone ampiamente la sintassi e proponendo esempi di utilizzo degli operatori e dei costrutti. Viene fatta una panoramica di SOC, SOA, Web Services, Cloud Computing, Orchestrazione, Coreografia, Deployment e Behaviour, gli ultimi due analizzati in diversi capitoli. La tesi si conclude con un esempio di conversione di servizi WSDL in Jolie, producendo un esempio di utilizzo del Web Service convertito. Nel documento vengono accennati i progressi storici del linguaggio ed i loro sviluppatori, nonché le API fornite dal linguaggio.

Questa tesi vuole fornire un'introduzione alla complessità computazionale e allo studio dei numeri primi riferito a questa materia. Si tratterà della Macchina di Turing e della sua importanza per calcolabilità e complessità, introducendo le classi P ed NP. Queste saranno approfondite studiando prima la classe di problemi NP-completi e successivamente fornendo alcuni esempi importanti. Nella parte finale ci si occuperà esplicitamente del problema dei numeri primi e si guarderà da vicino l'algoritmo AKS, dimostrandone la correttezza.

La tesi è uno studio di alcuni aspetti della nuova metodologia “deep inference”, abbinato ad una rivisitazione dei concetti classici di proof theory, con l'aggiunta di alcuni risultati originali orientati ad una maggior comprensione dell'argomento, nonché alle applicazioni pratiche. Nel primo capitolo vengono introdotti, seguendo un approccio di stampo formalista (con alcuni spunti personali), i concetti base della teoria della dimostrazione strutturale – cioè quella che usa strumenti combinatoriali (o “finitistici”) per studiare le proprietà delle dimostrazioni. Il secondo capitolo focalizza l'attenzione sulla logica classica proposizionale, prima introducendo il calcolo dei sequenti e dimostrando il Gentzen Hauptsatz, per passare poi al calcolo delle strutture (sistema SKS), dimostrando anche per esso un teorema di eliminazione del taglio, appositamente adattato dall'autore. Infine si discute e dimostra la proprietà di località per il sistema SKS. Un percorso analogo viene tracciato dal terzo ed ultimo capitolo, per quanto riguarda la logica lineare. Viene definito e motivato il calcolo dei sequenti lineari, e si discute del suo corrispettivo nel calcolo delle strutture. L'attenzione qui è rivolta maggiormente al problema di definire operatori non-commutativi, che mettono i sistemi in forte relazione con le algebre di processo.

Indagine sulla varietà sintattica presente all'interno dei formalismi di specifica della semantica operazionale strutturale (SOS) di linguaggi di programmazione e calcolo di processi. Rassegna di tool di implementazione con attenzione al grado di copertura linguistica.