Nel corso della stesura di alcuni articoli riguardanti la programmazione funzionale e i suoi rapporti con il lambda-calcolo, mi sono reso conto del fatto che la letteratura in Italiano è a riguardo spesso troppo tecnica e non sufficientemente contestualizzata; ne risulta che alcuni aspetti della teoria del calcolo computazionale e della logica formale si trovano ad essere in ombra, a dispetto della loro importanza fondante. Questi appunti (questo timido esercizio di lettere e matematiche) vorrebbero dare uno “sguardo dall’alto” al cosiddetto Isomorfismo di Curry-Howard.
L’Isomorfismo di Curry-Howard consiste nell’osservazione che due classi di sistemi formali (i modelli di computazione e i sistemi di provabilità), che al tempo della scoperta erano considerate del tutto disgiunte, sono in realtà strutturalmente lo stesso oggetto.
Nel 1958 venne scoperto da Curry un isomorfismo fra la versione tipata del lambda-calcolo e il frammento implicativo della logica costruttiva di Brouwer, indipendentemente poi riscoperto da Howard dieci anni dopo. L’isomorfismo, da allora noto anche come corrispondenza di Curry-Howard, mette in relazione i tipi del calcolo con gli enunciati della logica proposizionale e i termini con le prove: alla riduzione nel lambda-calcolo corrisponde l’eliminazione dei tagli nelle prove.
Da un punto di vista più informale si può dire che una prova è un programma, e la formula che prova è un tipo per il programma. Ovvero, il tipo di ritorno di una funzione è analogo ad un teorema, i cui assiomi sono corrispondenti ai tipi degli argomenti passati alla funzione, e il corpo stesso della funzione è la prova di quel teorema. Questo ha conseguenze importanti sulla programmazione logica, fornendo delle fondamenta solide su cui basarla: le dimostrazioni possono essere rappresentate come programmi (lambda-termini, in particolare), ovvero possono essere eseguite.
La possibilità di estendere l’isomorfismo a logiche sempre più espressive (calcolo dei predicati, logiche di ordine superiore) e corrispondenti calcoli, fanno di questi un prezioso strumento, sul quale si basano nuove applicazioni della logica in ambito informatico, come l’estrazione di programmi dalle corrispondenti prove di correttezza e terminazione. Più recentemente, un’interessante conseguenza dell’isomorfismo ha a che fare con la possibilità di parallelizzare efficientemente l’esecuzione dei programmi scritti in linguaggi funzionali; l’analisi di questa prospettiva è delegata ai prossimi capitoli.