Implementazione di un Algoritmo su Grafi per la Conversione di λ-Termini

Il lavoro svolto consiste nell'implementazione di un algoritmo di conversione che determini se due λ-espressioni sono equivalenti. Per determinare tale conversione computa le due λ-espressioni elaborando ognuno dei λ-termini contenuti e dove possibile applica una serie di regole di riduzione per convertire i λ-termini. Una volta ridotti compara i due λ-termini testando tutte le condizioni necessarie. L’output dell’algoritmo è un booleano che riporta se tali espressioni sono effettivamente differenti o se rappresentano la stessa espressione ridotta. Due λ-espressioni vengono considerate equivalenti a meno di riduzioni e α-rinominazioni ovvero di comparare i λ-termini dopo aver applicato le regole di riduzione e rinominando le variabili ad essi legate. Quindi due λ-espressioni equivalenti verranno denominate bi-simili. Lo scopo dell'algoritmo è di combinare la sharing equality di due λ-espressioni con la valutazione dei λ-termini contenuti in esse cercando di mantenere la complessità bi-lineare. Nel seguito del documento verranno illustrate le regole di riduzione, i costrutti e le tecniche utilizzate nell'implementazione dell'algoritmo.