Curry-Howard, isomorfismo di

Enciclopedia della Matematica (2013)

Curry-Howard, isomorfismo di


Curry-Howard, isomorfismo di corrispondenza fra dimostrazioni logiche e programmi informatici che si assume come nesso fra la logica e l’informatica teorica. In base a tale isomorfismo, ogni prova della logica intuizionista corrisponde a un termine del λ-calcolo semplicemente tipato, che a sua volta può essere pensato come un programma. L’esecuzione di questo programma corrisponde al processo di eliminazione del taglio dalla prova (→ taglio, regola del).

Tag
Vocabolario
curry
curry ‹kḁ′ri› s. ingl. [voce anglo-indiana, propr. grafia ingl. della voce tamilica kari «salsa»], usato in ital. al masch. – Condimento, originario dell’Asia tropicale e composto di varie polveri vegetali aromatiche e piccanti (curcuma,...
iṡomorfismo
isomorfismo iṡomorfismo s. m. [comp. di iso- e -morfismo]. – 1. In cristallochimica, il fenomeno per cui due o più sostanze che hanno analoga formula chimica (e simili dimensioni relative di anioni e cationi) si presentano in cristalli...