Le lien profond qui assimile les preuves mathématiques et les programmes informatiques | Magazine Quanta

Certaines découvertes scientifiques sont importantes car elles révèlent quelque chose de nouveau – la structure en double hélice de l’ADN, par exemple, ou l’existence de trous noirs. Cependant, certaines révélations sont profondes car elles montrent que deux vieux concepts, autrefois considérés comme distincts, sont en fait identiques. Prenez les équations de James Clerk Maxwell montrant que l'électricité et le magnétisme sont deux aspects d'un même phénomène, ou le lien de la relativité générale entre la gravité et un espace-temps courbe.

La correspondance Curry-Howard fait la même chose mais à une plus grande échelle, reliant non seulement des concepts séparés au sein d'un même domaine, mais des disciplines entières : Informatique et les logique mathématique. Également connu sous le nom d'isomorphisme de Curry-Howard (terme signifiant qu'il existe une sorte de correspondance biunivoque entre deux choses), il établit un lien entre les preuves mathématiques et les programmes informatiques.

En termes simples, la correspondance Curry-Howard postule que deux concepts issus de l'informatique (types et programmes) sont équivalents, respectivement, à des propositions et à des preuves – des concepts issus de la logique.

L’une des ramifications de cette correspondance est que la programmation – souvent considérée comme un métier personnel – est élevée au niveau idéalisé des mathématiques. Écrire un programme n’est pas simplement « coder », cela devient un acte de preuve d’un théorème. Cela formalise l’acte de programmation et fournit des moyens de raisonner mathématiquement sur l’exactitude des programmes.

La correspondance porte le nom des deux chercheurs qui l'ont découverte indépendamment. En 1934, le mathématicien et logicien Haskell Curry remarqua une similitude entre les fonctions en mathématiques et la relation d'implication en logique, qui prend la forme d'énoncés « si-alors » entre deux propositions.

Inspiré par l'observation de Curry, le logicien mathématicien William Alvin Howard a découvert un lien plus profond entre le calcul et la logique en 1969, montrant que l'exécution d'un programme informatique revient un peu à simplifier une preuve logique. Lorsqu'un programme informatique s'exécute, chaque ligne est « évaluée » pour produire une seule sortie. De même, dans une preuve, vous commencez par des déclarations complexes que vous pouvez simplifier (en éliminant les étapes redondantes, par exemple, ou en remplaçant les expressions complexes par des expressions plus simples) jusqu'à ce que vous arriviez à une conclusion - une déclaration plus condensée et succincte dérivée de nombreuses déclarations intermédiaires. .

Bien que cette description donne une idée générale de la correspondance, pour bien la comprendre, nous devons en apprendre un peu plus sur ce que les informaticiens appellent la « théorie des types ».

Commençons par un paradoxe célèbre : dans un village vit un barbier qui rase tous les hommes qui ne se rasent pas, et eux seulement. Le coiffeur se rase-t-il ? Si la réponse est oui, alors il ne doit pas se raser (car il ne rase que les hommes qui ne se rasent pas). Si la réponse est non, alors il doit se raser (car il rase tous les hommes qui ne se rasent pas). Il s’agit d’une version informelle d’un paradoxe découvert par Bertrand Russell en essayant d’établir les fondements des mathématiques à l’aide d’un concept appelé ensembles. Autrement dit, il est impossible de définir un ensemble contenant tous les ensembles qui ne se contiennent pas eux-mêmes sans rencontrer de contradictions.

Pour éviter ce paradoxe, a montré Russell, nous pouvons utiliser des « types ». En gros, ce sont des catégories dont les valeurs spécifiques sont appelées objets. Par exemple, s'il existe un type appelé « Nat », signifiant nombres naturels, ses objets sont 1, 2, 3, etc. Les chercheurs utilisent généralement deux points pour désigner le type d’un objet. Le nombre 7, de type entier, peut s'écrire « 7 : Entier ». Vous pouvez avoir une fonction qui prend un objet de type A et crache un objet de type B, ou une fonction qui combine une paire d'objets de type A et de type B dans un nouveau type, appelé « A × B ».

Une façon de résoudre le paradoxe consiste donc à hiérarchiser ces types, de sorte qu’ils ne puissent contenir que des éléments d’un « niveau inférieur » à eux-mêmes. Un type ne peut alors pas se contenir, ce qui évite l'autoréférentialité qui crée le paradoxe.

Dans le monde de la théorie des types, prouver qu’une déclaration est vraie peut sembler différent de ce à quoi nous sommes habitués. Si l'on veut prouver que l'entier 8 est pair, il s'agit alors de montrer que 8 est bien un objet d'un type spécifique appelé « Pair », dont la règle d'appartenance est d'être divisible par 2. Après avoir vérifié que 8 est divisible par 2, on peut conclure que 8 est bien un « habitant » de type Even.

Curry et Howard ont montré que les types sont fondamentalement équivalents aux propositions logiques. Lorsqu'une fonction « habite » un type — c'est-à-dire lorsque vous pouvez définir avec succès une fonction qui est un objet de ce type — vous montrez effectivement que la proposition correspondante est vraie. Ainsi, les fonctions qui prennent une entrée de type A et donnent une sortie de type B, notée type A → B, doivent correspondre à une implication : « Si A, alors B ». Par exemple, prenons la proposition « S’il pleut, alors le sol est mouillé ». En théorie des types, cette proposition serait modélisée par une fonction de type « Raining → GroundIsWet ». Les formulations d’aspect différent sont en fait mathématiquement les mêmes.

Aussi abstrait que puisse paraître ce lien, il a non seulement changé la façon dont les praticiens des mathématiques et de l’informatique envisagent leur travail, mais a également conduit à plusieurs applications pratiques dans les deux domaines. Pour l’informatique, il fournit une base théorique pour la vérification des logiciels, le processus permettant de garantir l’exactitude des logiciels. En formulant les comportements souhaités en termes de propositions logiques, les programmeurs peuvent prouver mathématiquement qu'un programme se comporte comme prévu. Il fournit également une base théorique solide pour concevoir des langages de programmation fonctionnels plus puissants.

Et pour les mathématiques, la correspondance a donné naissance à assistants de preuve, également appelés prouveurs de théorèmes interactifs. Il s'agit d'outils logiciels qui aident à construire des preuves formelles, comme Coq et Lean. En Coq, chaque étape de la preuve est essentiellement un programme, et la validité de la preuve est vérifiée par des algorithmes de vérification de type. Les mathématiciens utilisent également des assistants de preuve, notamment le Démonstrateur du théorème Lean — formaliser les mathématiques, ce qui implique de représenter des concepts, des théorèmes et des preuves mathématiques dans un format rigoureux et vérifiable par ordinateur. Cela permet de vérifier par ordinateur le langage parfois informel des mathématiques.

Les chercheurs explorent encore les conséquences de ce lien entre mathématiques et programmation. La correspondance originale Curry-Howard fusionne la programmation avec une sorte de logique appelée logique intuitionniste, mais il s'avère que davantage de types de logique pourraient également se prêter à de telles unifications.

"Ce qui s'est passé au cours du siècle qui a suivi la perspicacité de Curry, c'est que nous continuons à découvrir de plus en plus de cas où 'le système logique X correspond au système informatique Y'", a déclaré Michel Clarkson, informaticien à l'Université Cornell. Les chercheurs ont déjà connecté la programmation à d’autres types de logique comme la logique linéaire, qui inclut le concept de « ressources », et la logique modale, qui traite des concepts de possibilité et de nécessité.

Et même si cette correspondance porte les noms de Curry et Howard, ils ne sont en aucun cas les seuls à l'avoir découverte. Cela témoigne du caractère fondamental de la correspondance : les gens ne cessent de la remarquer, encore et encore. "Il ne semble pas que ce soit un hasard s'il existe un lien profond entre le calcul et la logique", a déclaré Clarkson.