Le lien profond entre la logique mathématique et le code des programmes informatiques : des images miroir les unes des autres

Certaines découvertes scientifiques revêtent une grande importance car quelque chose de nouveau est révélé, comme la structure en double hélice de l'ADN ou l'existence de trous noirs. Mais ces révélations ont une signification plus profonde, car elles montrent que deux vieux concepts qui semblaient auparavant très différents sont en réalité les mêmes. Par exemple, le système d'équations découvert par James Clerk Maxwell a montré que l'électricité et le magnétisme sont deux aspects différents d'un même phénomène, tandis que la relativité générale reliait la gravité à l'espace-temps courbe.

Il en va de même pour la correspondance Curry-Howard, et elle relie non seulement deux concepts différents dans un même domaine, mais deux disciplines complètes : l'informatique et la logique mathématique. Cette correspondance est également connue sous le nom d'isomorphisme de Curry-Howard (l'isomorphisme fait référence à une certaine correspondance biunivoque entre deux choses), qui établit un certain lien entre les preuves mathématiques et les programmes informatiques.

En termes simples, la correspondance Currie-Howard estime que deux concepts en informatique (types et programmes) sont équivalents à deux concepts en logique (propositions et preuves).

L'un des résultats de cette correspondance est que le développement de programmes a été élevé à un niveau mathématique idéalisé, alors qu'avant, les gens pensaient généralement que le développement de programmes n'était qu'un travail artisanal. Le développement de programmes ne consiste pas seulement à « écrire du code », c'est devenu l'acte de prouver des théorèmes. Cela formalise le comportement du développement du programme et fournit un moyen de raisonner mathématiquement sur l'exactitude du programme.

Le nom de cette correspondance vient de deux chercheurs, qui ont découvert indépendamment cette correspondance. En 1934, le mathématicien et logicien Haskell Curry remarqua la similitude entre les fonctions en mathématiques et la relation d'implication en logique. La forme d'une relation d'implication est une déclaration « si-alors » entre deux propositions.

Inspiré par les observations de Currie, le logicien mathématique William Alvin Howard a découvert en 1969 un lien plus profond entre le calcul et la logique ; ses recherches ont montré que : Les programmes informatiques ressemblent beaucoup à des preuves logiques simplifiées. Lorsque vous exécutez un programme informatique, chaque ligne de code est « évaluée » pour produire une sortie. De même, lorsque vous travaillez sur une preuve, vous commencez par une déclaration complexe, puis vous la simplifiez (par exemple, en éliminant les étapes redondantes ou en remplaçant les expressions complexes par des expressions plus simples) jusqu'à ce que vous parveniez à une conclusion - parmi de nombreuses. Une déclaration transitionnelle mène à une formulation plus concise. déclaration.

Bien que cette description donne une idée approximative de ce que signifie cette correspondance, la comprendre pleinement nécessite d'en savoir plus sur ce que les informaticiens appellent la « théorie des types ».

Commençons par un fameux paradoxe : Il y avait un barbier dans un village qui se rasait pour et seulement pour tous ceux qui ne se rasaient pas. Alors, ce coiffeur se rase-t-il ? Si la réponse est oui, alors il ne doit pas se raser (car il ne se rase que pour les personnes qui ne se rasent pas). Si la réponse est non, alors il doit se raser (car il rase tous ceux qui ne se rasent pas). Il s'agit d'une version informelle d'un paradoxe découvert par Bertrand Russell alors qu'il tentait de former les bases des mathématiques en utilisant un concept appelé ensembles. Autrement dit : il est impossible de définir un ensemble qui contient tous les ensembles qui ne se contiennent pas lui-même, et des contradictions surviendront inévitablement dans ce processus.

Les recherches de Russell montrent que pour éviter ce paradoxe, nous pouvons utiliser des types. En gros, les types sont des catégories dont les valeurs concrètes sont appelées objets. Par exemple, s'il existe un type Nat représentant des nombres naturels, alors ses objets sont 1, 2, 3, etc. Les chercheurs utilisent souvent des deux-points pour indiquer le type d'objet. Par exemple, pour la valeur de type entier 7, elle peut être écrite sous la forme « 7 : Integer ». Nous pouvons utiliser une fonction pour convertir un objet de type A en un objet de type B, ou nous pouvons utiliser une fonction pour combiner deux objets de types A et B en un nouvel objet de type "A×B".

Donc, pour résoudre ce paradoxe, une solution consiste à superposer ces types afin qu'ils ne contiennent que des éléments un niveau en dessous d'eux-mêmes. Un type ne peut alors pas se contenir, ce qui évite l'auto-référence qui crée le paradoxe ci-dessus.

Dans le monde de la théorie des types, le processus permettant de prouver qu'une déclaration est vraie peut être différent de ce à quoi nous sommes habitués. Si nous voulons prouver que l'entier 8 est un nombre pair, alors la clé du problème est de prouver que 8 est en fait un objet de type « pair », et la règle de ce type définit que les éléments sont divisibles par 2. . Après avoir vérifié que 8 est divisible par 2, on peut conclure que 8 est un « résident » de type « pair ».

Currie et Howard ont prouvé que les types sont fondamentalement équivalents aux propositions logiques. Lorsqu'une fonction « habite » un certain type, c'est-à-dire lorsqu'elle est un objet de ce type, nous pouvons effectivement prouver que la proposition correspondante est vraie. Par conséquent, une fonction qui prend un objet de type A en entrée et un objet de type B en sortie (noté type A → B) doit correspondre à une implication : « Si A, alors B Par exemple, supposons qu'il y ait le. » proposition « S'il pleut, alors le sol est mouillé. » En théorie des types, cette proposition sera modélisée en fonction du type « pluie → sol est mouillé ». Ces deux représentations semblent différentes, mais sont mathématiquement identiques.

Bien que ce lien puisse paraître abstrait, il change non seulement la façon dont les praticiens des mathématiques et de l'informatique envisagent leur travail, mais conduit également à des applications pratiques dans les deux domaines. En informatique, cette connexion fournit une base théorique pour la vérification des logiciels, le processus permettant de garantir l'exactitude des logiciels. En décrivant le comportement souhaité en termes de propositions logiques, les développeurs de programmes peuvent prouver mathématiquement si un programme se comporte comme prévu. Et cette connexion fournit également une base théorique solide pour concevoir des langages de programmation fonctionnels plus puissants.

Dans le domaine des mathématiques, cette correspondance a donné naissance à l'outil d'assistant de preuve, également connu sous le nom de prouveur de théorème interactif. Ces outils logiciels peuvent aider à créer des preuves formelles, par exemple Coq et Lean. En Coq, chaque étape de preuve est essentiellement un programme, et la validité de la preuve est vérifiée via un algorithme de vérification de type. Les mathématiciens utilisent également des assistants de preuve (en particulier des démonstrateurs de théorèmes Lean) pour formaliser les mathématiques, ce qui implique de représenter des concepts mathématiques, des théorèmes et des preuves dans un format rigoureux pouvant être vérifié par un ordinateur. Cela permet parfois à un langage mathématique informel d'être testé par des ordinateurs.

Les chercheurs explorent également les résultats potentiels de ce lien entre les mathématiques et la programmation. La correspondance originale Curry-Howard unissait le développement de programmes à un type de logique appelé logique intuitionniste, mais il s'avère qu'il existe de nombreux autres types de logique qui peuvent être unifiés.

Michael Clarkson, informaticien de l'Université Cornell, a déclaré : « Au cours du siècle qui s'est écoulé depuis que Currie a tiré ses idées, nous avons continué à trouver de plus en plus d'exemples du « système logique X correspond au système informatique Y ». » Les auteurs de recherche ont également lié la programmation. à d'autres types de logique, comme la logique linéaire impliquant le concept de « ressources » et la logique modale impliquant les concepts de possibilité et de nécessité.

Et bien que cette correspondance porte le nom de Curry et Howard, ils ne sont en aucun cas les seuls découvreurs de cette correspondance. Cela démontre le caractère fondamental de cette correspondance : les gens la remarquent encore et encore. Clarkson a déclaré : "Le lien profond entre l'informatique et la logique ne semble pas être accidentel

."

Ce qui précède est le contenu détaillé de. pour plus d'informations, suivez d'autres articles connexes sur le site Web de PHP en chinois!