Per un approccio semiotico ai videogiochi tra memoria culturale e memoria corporea

La tesi propone un approccio semiotico ai videogiochi e indaga le relazioni tra videogioco, memoria e senso, a partire dall’analisi di un ampio corpus di videogiochi, trasversale rispetto ai generi. Il lavoro intende mostrare la proficuità di un incontro tra semiotica e videogiochi sotto un duplice punto di vista: da un lato i videogiochi, in quanto oggetti “nuovi”, rappresentano un buon banco di prova per la teoria e la metodologia semiotica; dall’altro lato la semiotica permette di comprendere meglio i videogiochi, ricostruendo i meccanismi semiotici che contribuiscono a generare gli effetti di senso tipici di questa forma testuale (es. immersività, interattività, flusso…). Il lavoro si propone quindi il duplice obiettivo di individuare le peculiarità del videogioco in quanto oggetto di analisi semiotica (cap. 1) e i meccanismi che in diversi generi videoludici portano alla creazione di effetti di senso peculiari e alla costruzione di una nuova memoria (capp. 3, 4, 5). Il primo capitolo è dedicato a una riflessione teorica e metodologica che intende preparare il campo per l’analisi, provando a “testare” modelli, concetti e strumenti più o meno assestati con lo scopo di riconoscere lo statuto semiotico dei videogiochi e di individuare il modo migliore per analizzarli semioticamente. Inoltre nel cap. 1 si affrontano, ancora in un’ottica generale, le dinamiche tra memoria del gioco e memoria del giocatore e l’importanza dei processi di apprendimento per l’interpretazione videoludica. Gli ultimi tre capitoli sono invece dedicati ai risultati delle analisi, condotte su un corpus ampio di videogiochi, affiancato da un corpus “di controllo” costituito da video di partite concrete, immagini user-generated, interfacce fisiche di gioco e “discorsi su” i videogiochi inseriti nel corpus principale. Il terzo capitolo individua i meccanismi semiotici che contribuiscono a costruire, de-costruire e ricostruire l’identità del giocatore nel corso della partita. Il quarto capitolo affronta la relazione tra tempo del gioco e tempo del giocatore, concentrandosi sulle modalità di configurazione del tempo in atto nei diversi generi videoludici. L’ultimo capitolo è dedicato all’approfondimento di un aspetto particolare della testualità videoludica: la capacità dei videogiochi di generare esperienze embodied, cioè esperienze ‘incarnate’ e ‘situate’.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.