Il collegamento profondo che equipara prove matematiche e programmi per computer | Rivista Quanti

Alcune scoperte scientifiche sono importanti perché rivelano qualcosa di nuovo: la struttura a doppia elica del DNA, per esempio, o l’esistenza dei buchi neri. Tuttavia, alcune rivelazioni sono profonde perché mostrano che due vecchi concetti, una volta ritenuti distinti, sono in realtà gli stessi. Prendiamo le equazioni di James Clerk Maxwell che mostrano che l'elettricità e il magnetismo sono due aspetti di un singolo fenomeno, o il collegamento della gravità con uno spazio-tempo curvo secondo la relatività generale.

La corrispondenza Curry-Howard fa lo stesso ma su scala più ampia, collegando non solo concetti separati all’interno di un campo, ma intere discipline: Informatica ed logica matematica. Conosciuto anche come isomorfismo di Curry-Howard (un termine che significa che esiste una sorta di corrispondenza uno a uno tra due cose), stabilisce un collegamento tra dimostrazioni matematiche e programmi per computer.

In parole povere, la corrispondenza Curry-Howard presuppone che due concetti dell’informatica (tipi e programmi) siano equivalenti, rispettivamente, a proposizioni e dimostrazioni: concetti della logica.

Una conseguenza di questa corrispondenza è che la programmazione – spesso vista come un mestiere personale – è elevata al livello idealizzato della matematica. Scrivere un programma non è semplicemente “codificare”, diventa un atto di dimostrazione di un teorema. Ciò formalizza l'atto di programmazione e fornisce modi per ragionare matematicamente sulla correttezza dei programmi.

La corrispondenza prende il nome dai due ricercatori che l'hanno scoperta indipendentemente. Nel 1934, il matematico e logico Haskell Curry notò una somiglianza tra le funzioni in matematica e la relazione di implicazione in logica, che assume la forma di affermazioni “se-allora” tra due proposizioni.

Ispirato dall'osservazione di Curry, il logico matematico William Alvin Howard scoprì un legame più profondo tra calcolo e logica nel 1969, dimostrando che eseguire un programma per computer è molto simile a semplificare una dimostrazione logica. Quando un programma per computer viene eseguito, ogni riga viene “valutata” per produrre un singolo output. Allo stesso modo, in una dimostrazione, si inizia con affermazioni complesse che è possibile semplificare (eliminando passaggi ridondanti, ad esempio, o sostituendo espressioni complesse con espressioni più semplici) finché non si arriva a una conclusione: un'affermazione più condensata e concisa derivata da molte affermazioni intermedie. .

Sebbene questa descrizione trasmetta un senso generale della corrispondenza, per comprenderla appieno dobbiamo imparare qualcosa in più su ciò che gli informatici chiamano “teoria dei tipi”.

Cominciamo con un famoso paradosso: in un villaggio vive un barbiere che rade tutti gli uomini che non si radono da soli, e solo loro. Il barbiere si rade da solo? Se la risposta è sì, allora non deve radersi (perché rade solo gli uomini che non si radono da soli). Se la risposta è no, allora deve radersi da solo (perché rade tutti gli uomini che non si radono da soli). Questa è una versione informale di un paradosso scoperto da Bertrand Russell mentre cercava di stabilire i fondamenti della matematica utilizzando un concetto chiamato insiemi. Cioè è impossibile definire un insieme che contenga tutti gli insiemi che non contengono se stessi senza incontrare contraddizioni.

Per evitare questo paradosso, ha dimostrato Russell, possiamo usare i “tipi”. In parole povere, si tratta di categorie i cui valori specifici sono chiamati oggetti. Ad esempio, se esiste un tipo chiamato "Nat", che significa numeri naturali, i suoi oggetti sono 1, 2, 3 e così via. I ricercatori in genere utilizzano i due punti per denotare il tipo di oggetto. Il numero 7, di tipo intero, può essere scritto come “7: Intero”. Puoi avere una funzione che prende un oggetto di tipo A e sputa fuori un oggetto di tipo B, o una che combina una coppia di oggetti di tipo A e di tipo B in un nuovo tipo, chiamato "A × B".

Un modo per risolvere il paradosso, quindi, è mettere queste tipologie in una gerarchia, in modo che possano contenere solo elementi di “livello inferiore” rispetto a loro. Allora un tipo non può contenere se stesso, il che evita l'autoreferenzialità che crea il paradosso.

Nel mondo della teoria dei tipi, dimostrare che un'affermazione è vera può apparire diverso da ciò a cui siamo abituati. Se vogliamo dimostrare che l'intero 8 è pari, allora si tratta di mostrare che 8 è effettivamente un oggetto di un tipo specifico chiamato "Pari", dove la regola per l'appartenenza è essere divisibile per 2. Dopo aver verificato che 8 è divisibile per 2 possiamo concludere che 8 è effettivamente un “abitante” del tipo Pari.

Curry e Howard hanno dimostrato che i tipi sono fondamentalmente equivalenti alle proposizioni logiche. Quando una funzione “abita” un tipo, ovvero quando puoi definire con successo una funzione che è un oggetto di quel tipo, stai effettivamente dimostrando che la proposizione corrispondente è vera. Quindi le funzioni che ricevono un input di tipo A e danno un output di tipo B, indicato come tipo A → B, devono corrispondere a un’implicazione: “Se A, allora B”. Prendiamo ad esempio la proposizione “Se piove, il terreno è bagnato”. Nella teoria dei tipi, questa proposizione sarebbe modellata da una funzione del tipo “Piove → Il terreno è bagnato”. Le formulazioni dall'aspetto diverso sono infatti matematicamente le stesse.

Per quanto astratto possa sembrare questo collegamento, non solo ha cambiato il modo in cui i professionisti della matematica e dell’informatica pensano al proprio lavoro, ma ha anche portato a diverse applicazioni pratiche in entrambi i campi. Per l'informatica, fornisce una base teorica per la verifica del software, il processo volto a garantire la correttezza del software. Inquadrando i comportamenti desiderati in termini di proposizioni logiche, i programmatori possono dimostrare matematicamente che un programma si comporta come previsto. Fornisce inoltre una solida base teorica per la progettazione di linguaggi di programmazione funzionale più potenti.

E per la matematica la corrispondenza ha portato alla nascita di assistenti di prova, detti anche dimostratori di teoremi interattivi. Si tratta di strumenti software che aiutano nella costruzione di dimostrazioni formali, come Coq e Lean. In Coq, ogni passaggio della dimostrazione è essenzialmente un programma e la validità della dimostrazione viene verificata con algoritmi di controllo del tipo. Anche i matematici utilizzano assistenti di dimostrazione, in particolare il Dimostratore di teoremi snello — formalizzare la matematica, che implica la rappresentazione di concetti, teoremi e dimostrazioni matematiche in un formato rigoroso e verificabile dal computer. Ciò consente ai computer di controllare il linguaggio talvolta informale della matematica.

I ricercatori stanno ancora esplorando le conseguenze di questo legame tra matematica e programmazione. La corrispondenza originale di Curry-Howard fonde la programmazione con un tipo di logica chiamata logica intuizionistica, ma risulta che anche più tipi di logica potrebbero essere suscettibili di tali unificazioni.

"Ciò che è successo nel secolo successivo all'intuizione di Curry è che continuiamo a scoprire sempre più casi in cui 'il sistema logico X corrisponde al sistema computazionale Y'", ha affermato Michael Clarkson, uno scienziato informatico della Cornell University. I ricercatori hanno già collegato la programmazione ad altri tipi di logica come la logica lineare, che include il concetto di “risorse”, e la logica modale, che si occupa dei concetti di possibilità e necessità.

E sebbene questa corrispondenza porti i nomi di Curry e Howard, non sono affatto gli unici ad averlo scoperto. Ciò attesta la natura fondamentale della corrispondenza: le persone continuano a notarla ancora e ancora. "Non sembra essere un caso che esista un profondo legame tra calcolo e logica", ha detto Clarkson.