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&nbsp (m + y) =  m +  S y.

La correspondència Curry-Howard (també conegut com isomorfisme Curry-Howard o equivalència Curry-Howard o proposicions Curry-Howard) esta ubicada en el camp de la teoria dels 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 analogica entre els sistemes de la lògica formal i els càlculs de còmput. Va ser descobert 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 mecanografiat càlcul lambda dels combinadors podria ser vist com a axioma-esquemes per la lògica intuicionista implicativa,
2. L'observació el 1958 per Curry que un cert tipus de prova de sistema, conegut com estil deducció del sistema de Hilbert, coincideix en algun fragment al fragment de tipus d'un estàndard model de càlcul conegut com lògica combinatòria,
3. L'observació el 1969 per William Alvin Howard que un altre, més "alt nivell" teoria de la prova, conegut com deducció natural, poden ser interpretats directament en el seu intuicionista la versió com una variant de 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. El resultat es que de fet son estructuralment la mateixa classe d'objectes.

Bibliografia

• edited by Ph. de Groote. (1995), De Groote, Philippe, ed., The Curry–Howard Isomorphism, vol. 8, Cahiers du Centre de Logique (Université catholique de Louvain), Academia-Bruylant, 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ł (2006), Lectures on the Curry–Howard isomorphism, vol. 149, Studies in Logic and the Foundations of Mathematics, Elsevier, ISBN 978-0-444-52077-7, <http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385>, 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. 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

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