Implementazione di un algoritmo lineare per l’α-equivalenza di λ-termini con sharing

L'argomento di studio interessa i lambda- termini del lambda-calcolo, il quale rappresenta il prototipo di ogni linguaggio di programmazione funzionale. In particolare la tesi affronta una problematica relativa al costo computazionale delle lambda-riduzioni, ed esattamente la possibilità di implementare in tempo lineare la riduzione dei lambda-termini con sharing sul numero di passi di beta-riduzione, oggetto di studio. L’obiettivo di questa tesi è la prima implementazione dell'algoritmo proposto dal Prof. Claudio Sacerdoti Coen e dal Dott. Ricercatore Beniamino Accattoli, che risolve in tempo lineare sul numero di passi di beta-riduzione il problema della lambda riduzione dei lambda-termini con sharing, detta anche alpha-conversione. Il lavoro svolto consiste nell' implementazione dell'algoritmo in C#, nell’esecuzione dei relativi test funzionali e di efficienza dell'algoritmo. Nella tesi vengono descritte: le strutture dati utilizzate e l'implementazione dell'algoritmo con il relativo codice sorgente; le modalità di test e di verifica funzionale dell'algoritmo; l'analisi dei risultati ottenuti al fine di valutare l'efficienza dell'algoritmo.