Convergenza e divergenza in un linguaggio funzionale prototipale

Nella tesi viene proposto uno studio circa la convergenza e divergenza di termini nel linguaggio PCF descritte tramite le interpretazioni induttiva e co-induttiva del sistema inferenziale. La prima parte dell'elaborato presenta il linguaggio nelle sue caratteristiche principali e mostra come a partire dall'utilizzo di definizioni induttive della semantica small-step e della semantica big-step sia possibile descrivere il comportamento di termini convergenti in PCF. La seconda parte riguarda invece la necessità di una definizione co-induttiva per dettagliare il comportamento delle semantiche in caso di termini divergenti. Viene infine introdotto l'operatore co-induttivo co* in grado di coniugare convergenza e divergenza di termini.