Correspondència Curry-Howard

Una prova escrita com un programa funcional: la prova de la commutativitat de la suma dels nombres naturals en l'assistent de proves Coq. nat_ind significa inducció matemàtica, eq_ind per a la substitució dels iguals i f_equal per haver pres la mateixa funció en ambdós costats de la igualtat. Teoremes anteriors es fa referència al fet que mostra m = m + 0 and S (m + y) = m + S y.

La correspondència Curry-Howard (també coneguda com a isomorfisme Curry-Howard o equivalència Curry-Howard o proposicions Curry-Howard) està ubicada en el camp de la teoria del llenguatge de programació i teoria de la prova, i estableix una relació directa entre els programes d'ordinador i les proves. Es tracta d'una generalització d'una sintàctica analògica entre els sistemes de la lògica formal i els càlculs de còmput. Va ser descoberta pel matemàtic nord-americà Haskell Curry i el lògic William Alvin Howard.

Origen, abast i conseqüències

L'evolució de la correspondència de Curry-Howard és:

1. L'observació el 1934 per Curry que el càlcul lambda mecanografiat dels combinadors podria ser vist com a axioma-esquema per la lògica intuïcionista implicativa,
2. L'observació el 1958 per Curry que un cert tipus de prova de sistema, conegut com a estil deducció del sistema de Hilbert, coincideix en algun fragment amb el tipus d'un model de càlcul estàndard conegut com a lògica combinatòria,
3. L'observació el 1969 per William Alvin Howard que un altre nivell més "alt" de teoria de la prova, conegut com a deducció natural, podia ser interpretat directament en la seva versió intuïcionista com una variant del tipus del model de computació en el càlcul lambda.

En altres paraules, la correspondència de Curry-Howard és l'observació que dues famílies de formalismes que semblaven no relacionats, és a dir, els sistemes de prova, d'una banda, i els models de càlcul, de l'altra, de fet, són estructuralment la mateixa classe d'objectes.

Bibliografia

• edited by Ph. de Groote.. The Curry–Howard Isomorphism. 8. Academia-Bruylant, 1995. ISBN 978-2-87209-363-2. , reprodueix els treballs seminals de Curri-Feys i Howard, un paper pel de Bruijn i uns quants altres documents.
• Sørensen, Morten Heine; Urzyczyn, Paweł. Lectures on the Curry–Howard isomorphism. 149. Elsevier, 2006. ISBN 978-0-444-52077-7. , notes sobre la teoria de la prova i la teoria del tipus, que inclou una presentació de la correspondència de Curry-Howard, amb un enfocament en la correspondència fórmules-com-tipus
• Girard, Jean-Yves (1987–90). Proof and Types Arxivat 2008-04-18 a Wayback Machine.. Translated by and with appendices by Lafont, Yves and Taylor, Paul. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0-521-37181-3, notes sobre la teoria de la prova amb una presentació de la correspondència de Curry-Howard.
• Thompson, Simon (1991). Type Theory and Functional Programming Addison–Wesley. ISBN 0-201-41667-0.

Enllaços externs

A Wikibooks en anglès, hi ha llibres de contingut lliure i altres textos relatius a The Curry–Howard isomorphism.

• La Corresponència Curry–Howard a Haskell Arxivat 2008-08-19 a Wayback Machine.. (anglès)
• The Monad Reader 6: Adventures in Classical-Land: Curri-Howard a Haskell, la llei de Peirce. (anglès)