Correspondance de Curry-Howard

La correspondance de Curry-Howard, appelée^[1] également isomorphisme de Curry-de Bruijn-Howard, 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é. Ils établissent des relations entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958, lorsque Haskell Curry remarqua l'analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969, quand William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du 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 1960 à nos jours : sémantique dénotationnelle, logique linéaire, réalisabilité, démonstration automatique, etc.

Historique[modifier | modifier le code]

La correspondance de Curry-Howard était formulée par Curry pour la logique combinatoire dès la fin des années 1940. Howard a publié en 1980^[2] un article qui présente formellement la correspondance pour le lambda calcul simplement typé, mais il n'a fait que rendre public un document qui avait déjà circulé dans le monde des logiciens. Elle était connue indépendamment de Joachim Lambek pour les catégories cartésiennes fermées, de Girard pour le système F et de de Bruijn pour le système Automath. Au moins ces cinq noms pourraient être associés à ce concept.

Logique implicative minimale[modifier | modifier le code]

Par exemple, en lambda calcul simplement typé, si on associe à chaque type de base une variable propositionnelle et que l'on associe l'implication logique $\Rightarrow$ au constructeur de type $\rightarrow$ alors les propositions démontrables de la logique implicative minimale (où le seul connecteur est l'implication) correspondent aux types des termes clos du lambda calcul.

Par exemple, à la proposition $A\Rightarrow A$ on associe le lambda-terme $\lambda x^{A}.x:A\rightarrow A$ .

En revanche, il n'y a pas de lambda terme clos associé à la proposition $\,A$ ou à la proposition $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ (loi de Peirce), car elles ne peuvent pas être démontrées en logique implicative minimale.

Mais la correspondance s'étend aussi aux démonstrations 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.

Terminaison de réductions de preuves en déduction modulo[modifier | modifier le code]

Cette correspondance est notamment utile afin de montrer la réduction (ou démonstration) de certaines preuves dans des théories de la déduction modulo. Ainsi, dans le cas où les preuves (propositions) sont exprimées par des termes (appelés preuves-termes) en lambda calcul simplement typé, il est nécessaire de considérer les preuves comme des algorithmes. Les preuves de $A\Rightarrow B$ sont désormais des algorithmes qui, à des preuves de $A$ , associent des preuves de $B$ . Le type de $A\Rightarrow B$ s'exprime alors de la manière suivante

$\Phi (A\Rightarrow B)=\Phi (A)\rightarrow \Phi (B)$

Sans perte de généralité, la correspondance s'exprime par un isomorphisme $\Phi$ de l'ensemble des preuves-termes vers l'ensemble des types de preuves-termes. La terminaison de la $\beta$ -réduction du lambda calcul simplement typé permet dès lors de conclure sur la terminaison de diverses réductions de preuves dans des théories en déduction modulo.

Calcul propositionnel[modifier | modifier le code]

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[modifier | modifier le code]

Grâce à cette correspondance on peut prouver la cohérence d'une 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[modifier | modifier le code]

Quelques correspondances entre systèmes fonctionnels et systèmes formels
Système fonctionnel	Système formel
Calcul des constructions (Thierry Coquand)	Logique intuitionniste d'ordre supérieur
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 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 $\vee$ et $\wedge$
Réalisabilité classique / Lambda-calcul avec contrôle / Machine de Krivine	Logique classique du deuxième ordre

Logique et informatique[modifier | modifier le code]

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 » : $\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 propositions qui sont indécidables correspond à un programme de réparation de fichiers^{[réf. nécessaire]} ;
le théorème de complétude de Gödel correspond lui à un désassembleur interactif de programmes^[3].

Conséquences juridiques[modifier | modifier le code]

Comme l'a relevé Bernard Lang^[4], la correspondance de Curry-Howard constitue un argument contre la brevetabilité du logiciel. Puisque les algorithmes sont des méthodes mathématiques, et que ces dernières sont exclues par nature du champ de la brevetablilité, alors les algorithmes ne peuvent être brevetés.

Bibliographie[modifier | modifier le code]

Le livre de référence est le livre de Girard-Lafont-Taylor connu sous le nom de « Girafon ».

Jean-Yves Girard, Le Point Aveugle, Cours de Logique, éd. Hermann, Paris, collection « Visions des Sciences », tome 1 : Vers la Perfection, 2006, 280 p. Ce cours de théorie de la démonstration s'ouvre sur une réflexion sur l'état actuel de la logique (essentialisme et existentialisme, théorème d'incomplétude de Gödel, calcul des séquents), poursuit sur la Correspondance de Curry-Howard (système F, interprétation catégorique), puis motive et décrit la logique linéaire (espaces cohérents, système LL, réseaux de démonstration).

Notes et références[modifier | modifier le code]

↑ La terminologie isomorphisme de Curry-Howard employée dans les années 1990, est devenue moins courante.
↑ Howard, W., The formulas--as--types notion of construction, in Essays on Combinatory Logic, Lambda Calculus, and Formalism, Seldin, J. P. and Hindley, J. R. ed., Academic Press (1980), pp. 479--490.
↑ [PDF] 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).
↑ Bernard Lang, « Internet libère les logiciels », La recherche, n^o 328,‎ février 2000 (lire en ligne)

[1] La terminologie isomorphisme de Curry-Howard employée dans les années 1990, est devenue moins courante.

[2] Howard, W., The formulas--as--types notion of construction, in Essays on Combinatory Logic, Lambda Calculus, and Formalism, Seldin, J. P. and Hindley, J. R. ed., Academic Press (1980), pp. 479--490.

[3] [PDF] 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).

[4] Bernard Lang, « Internet libère les logiciels », La recherche, n^o 328,‎ février 2000 (lire en ligne)

[1]

[2]

[3]

[4]

v · m Informatique théorique
Codage	Codage de l'information Compression de données Chiffrement Cryptanalyse Cryptographie Théorie de l'information
Modèles de calcul	Calculabilité Décidabilité et indécidabilité Ensemble récursif Problème de l'arrêt Ensemble récursivement énumérable Machine de Turing Thèse de Church Automate cellulaire Réseau de neurones artificiels Réduction polynomiale Problème NP-complet Principe de Church-Turing-Deutsch
Algorithmique	Algorithmique Algorithme glouton Algorithme probabiliste Algorithme génétique Complexité algorithmique Analyse d'algorithme Diviser pour régner Heuristique Programmation dynamique Géométrie algorithmique Algorithmes de tri Algorithmique du texte Exploration de données Science des données Apprentissage profond Test de primalité Structure de données Arbre enraciné Concurrence Parallélisme
Syntaxe	Réécriture Compilation Expression régulière Grammaire formelle Langage rationnel Ensemble rationnel Théorie des langages Théorie des automates Automate fini Automate sur les mots infinis Automate d'arbres Automate à pile Hiérarchie de Chomsky Linguistique informatique
Sémantique	Interprétation abstraite Méthodes formelles Vérification de modèles Sémantique des langages de programmation Sémantique dénotationnelle Sémantique axiomatique Sémantique opérationnelle
Logique mathématique	Assistant de preuve Calcul des prédicats Correspondance de Curry-Howard Fonction récursive Lambda-calcul Théorèmes d'incomplétude de Gödel Théorie des types
Mathématiques discrètes	Combinatoire Algorithme du simplexe Optimisation combinatoire Théorie des graphes Algorithmes de la théorie des graphes Recherche opérationnelle Théorie de la décision Analyse numérique