Vés al contingut

Correspondència Curry-Howard

De la Viquipèdia, l'enciclopèdia lliure
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

[modifica]

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

[modifica]

Enllaços externs

[modifica]