Correspondance de Curry-Howard
167076
30699794
2008-06-16T15:15:13Z
Chaoborus
108951
+lien
La '''correspondance de Curry-Howard''', appelée également '''correspondance preuve/programme''' ou correspondance '''formule/type''', est une série de résultats à la frontière entre la [[logique mathématique]], l'[[informatique théorique]] et la [[théorie de la calculabilité]] établissant une relation entre les démonstrations formelles d'un [[Logique mathématique#Système logique|système logique]] et les programmes d'un [[Théorie de la calculabilité#Modèles de calcul|modèle de calcul]]. Les premiers exemples de correspondance de Curry-Howard remontent à 1958 date à laquelle Curry remarqua l'analogie formelle entre les démonstrations des [[systèmes à la Hilbert]] et la [[logique combinatoire]], puis à 1969 où [[William Alvin Howard]] remarqua que les démonstrations en [[déduction naturelle|déduction naturelle intuitionniste]] pouvaient formellement se voir comme des termes du [[lambda-calcul#Le lambda-calcul simplement typé|lambda-calcul typé]].
La correspondance de Curry-Howard a joué un rôle important en logique, car elle a établi un pont entre [[théorie de la démonstration]] et informatique théorique. On la retrouve utilisée sous une forme ou une autre dans de très nombreux travaux allant des années 60 à nos jours : [[sémantique dénotationnelle]], [[logique linéaire]], [[réalisabilité]], [[démonstration automatique]]...
== Logique implicative minimale ==
Par exemple, en [[lambda-calcul#Le lambda-calcul simplement typé|lambda calcul simplement typé]], si on associe à chaque type de base une variable propositionnelle et que l'on associe l'implication logique <math>\Rightarrow</math> au constructeur de type <math>\rightarrow</math> alors les propositions démontrables de la [[Logique intuitionniste#La logique implicative minimale|logique implicative minimale]] (où le seul connecteur est l'implication) correspondent aux types des [[lambda-calcul#Variables libres et variables liées|termes clos]] du lambda calcul.
Par exemple, à la proposition <math>A \Rightarrow A</math> on associe le lambda-terme <math>\lambda x^A .x : A \rightarrow A</math>.
En revanche, il n'y a pas de lambda terme clos associé à la proposition <math>\,A</math> ou à la proposition <math>((A\Rightarrow B)\Rightarrow A)\Rightarrow A</math> ([[Loi de Peirce]]), car elles ne peuvent pas être démontrées en logique implicative minimale.
Mais la correspondance s'étend aussi aux démontrations et aux normalisations de démonstrations comme suit :
* les types sont les propositions ;
* les termes sont les démonstrations ;
* les réductions des termes sont les normalisations de démonstrations.
== Calcul propositionnel ==
Si on étend le lambda calcul au produit cartésien, on aura parallèlement le ''et'' logique. Si on rajoute la somme disjointe (types somme ou structures) on aura le ''ou'' logique. Dans les lambda-calculs d'ordre supérieurs on rajoute des variables de types donc des quantificateurs. Cela donne les ''pour tout''.
== Calcul du second ordre ==
Grâce à cette correspondance on peut prouver la cohérence d'une [[logique#Mathématiques|logique]] en démontrant la normalisation forte du lambda-calcul associé (aucun terme ne se réduit infiniment). C'est ainsi que [[Jean-Yves Girard]] a résolu la ''conjecture de Takeuti'', à savoir démontrer la cohérence de l'arithmétique du second ordre ; il l'a fait en établissant la normalisation forte du [[Système F]].
== Correspondances ==
{| class="wikitable" style="text-align:center;"
|+ Quelques correspondances entre systèmes fonctionnels et systèmes formels
! Système fonctionnel
! Système formel
|-
| [[Calcul des constructions]] ([[Thierry Coquand]])
| ?
|-
| [[Système F]] ([[Jean-Yves Girard]])
| Arithmétique de Peano du second ordre / Logique intuitionniste du second ordre
|-
| [[Système T]] ([[Kurt Gödel]])
| Arithmétique de Peano du premier ordre / Logique intuitionniste du premier ordre
|-
| [[Système T1]]
| ?
|-
| T0 ([[Fonction récursive primitive|Récursion primitive]]) ([[Stephen Cole Kleene]] ? [[Thoralf Skolem]] ?)
| Arithmétique primitive récursive
|-
| [[Lambda-calcul#Le lambda-calcul simplement typé|Lambda-calcul simplement typé]]
| Calcul propositionnel minimal implicatif ([[déduction naturelle]])
|-
| [[Logique combinatoire]]
| Calcul propositionnel minimal implicatif (à la Hilbert)
|-
| Calcul lambda-µ de Parigot
| Déduction naturelle en calcul propositionnel classique
|-
| Calcul lambda-µ-µ~ de Curien et Herbelin
| [[Calcul des séquents]] classique
|-
| Calcul symétrique de Berardi et calcul dual de Wadler
| Calcul des séquents avec <math>\vee</math> et <math>\wedge</math>
|}
== Logique et informatique ==
Le logicien français, [[Jean-Louis Krivine]] a fait le rapport entre différents théorèmes mathématiques et les programmes informatiques qu'ils représentent.
* l'absurde (appelé « bottom » : <math>\perp</math>) a pour lambda-terme λx.x, ce qui correspond à « pour tout x, x » c’est-à-dire que tout est vrai. Comme on utilise un système [[logique mathématique | cohérent]] ceci est toujours faux. En informatique, cela correspond à une instruction d'échappement, d'[[Système de gestion d'exceptions|exception]].
* le [[théorème d'incomplétude de Gödel]] qui dit qu'il y a des théorèmes que l'on ne peut pas démontrer correspond à un programme de réparation de fichiers.
* le théorème de complétude de Gödel correspond lui à un désassembleur de programmes.
== Références ==
Le livre de référence est le [http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html livre de Girard- Lafont-Taylor] connu sous le nom de Girafon.
{{Portail|logique|informatique}}
[[Catégorie:Calculabilité]]
[[Catégorie:Logique mathématique]]
[[Catégorie:Théorie des types]]
[[en:Curry-Howard correspondence]]
[[pl:Izomorfizm Curry'ego-Howarda]]
[[zh:Curry-Howard同构]]