La correspondance de Curry-Howard a établi un pont entre théorie de la démonstration et informatique théorique.
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 [Jean-Louis Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique, Bull. Symb. Log. 2, 4, p. 405-421 (1996)]:
- l'absurde (appelé « bottom » : \perp) correspond à une instruction d'échappement, d'exception, ou à un programme qui ne finit pas (un terme non-typable dans le lambda-calcul simplement typé).
- 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.[réf. souhaitée]
- le théorème de complétude de Gödel correspond lui à un désassembleur interactif de programmes
| 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 (Récursion primitive) (Stephen Cole Kleene ? Thoralf Skolem ?) | Arithmétique primitive récursive |
| 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  et  |
No comments:
Post a Comment