Correspondència Curry-Howard

De Viquipèdia
Dreceres ràpides: navegació, cerca
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 a isomorfisme Curry-Howard o equivalència Curry-Howard o proposicions Curry-Howard) està 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[modifica | modifica el codi]

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 a estil deducció del sistema de Hilbert, coincideix en algun fragment al fragment de tipus d'un estàndard model de càlcul conegut com a 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 a 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 és que de fet son estructuralment la mateixa classe d'objectes.

Bibliografia[modifica | modifica el codi]

Enllaços externs[modifica | modifica el codi]

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