Interpretazione "proofs-as-programs" per l'aritmetica di Presburger

L’intento di questa tesi è quello di interpretare l’aritmetica di Presburger nella teoria dei tipi intuizionista di Per Martin-Löf MLTT. Dopo una breve introduzione sulle origini della teoria dei tipi e sulla sua importanza attuale nei campi della matematica e dell’informatica, passeremo a descrivere in particolare la teoria MLTT con le sue regole e discuteremo delle diverse interpretazioni che può avere una teoria dei tipi. Ci sarà poi un capitolo dedicato all’aritmetica di Presburger in cui ne saranno esposte le caratteristiche principali, quali la sua decidibilità e completezza (caratteristiche non condivise dall’aritmetica di Peano). In particolare definiremo l’aritmetica di Presburger classica sia nella versione originale PrC1 che come frammento del linguaggio dell’aritmetica di Peano PrC. Successivamente considereremo la sua versione intuizionista PrI. Mostreremo poi una traduzione di PrI in MLTT che ha la caratteristica di rendere valido il paradigma proofs-as-programs, ovvero permette di estrarre programmi dalle dimostrazioni di PrI. Componendo questa traduzione di PrI in MLTT con la traduzione della doppia negazione di Göedel di PrC in PrI otterremo anche un’interpretazione proofs-as-programs di PrC in MLTT. Questa tesi pone le basi per formalizzare in teoria dei tipi, come programma funzionale, l’algoritmo di decisione delle formule dell’aritmetica classica di Presburger e per poi dimostrarne la correttezza in modo costruttivo.