Théorie des types et isomorphisme de Curry-Howard : la profonde harmonie entre propositions = types et preuves = programmes

Dans l’histoire de l’informatique et des mathématiques, l’une des découvertes les plus belles et les plus profondes est l’« isomorphisme de Curry-Howard ». Ce concept n’est pas une simple analogie. Il montre que le fait d’« écrire un programme informatique » et de « prouver un théorème mathématique » sont des actes parfaitement identiques, que ce soit d’un point de vue syntaxique, sémantique ou en tant que structure mathématique. Le programme que nous soumettons à un compilateur peut être interprété directement comme une preuve formelle dans un système de démonstration logique.

Dans cet article, nous explorerons l’intersection entre la théorie des types et la logique, en partant du lambda-calcul simplement typé (Simply Typed Lambda Calculus) pour aller vers le Système F (System F), la théorie des types dépendants (Dependent Type Theory) et la pointe des mathématiques modernes : la théorie des types homotopique (Homotopy Type Theory ; HoTT). Nous expliquerons également en détail, à l’aide de formulations rigoureuses de règles d’inférence et d’exemples concrets de code de preuve, comment les assistants de preuve modernes (Coq, Lean 4, etc.) réalisent la forme ultime de la vérification logicielle. À travers ce voyage de plus de 10 000 caractères, venez ressentir la véritable harmonie entre les programmes et les mathématiques.

Chapitre 1 : Le carrefour miraculeux de la logique et du calcul : Histoire et interprétation BHK

La découverte de Haskell Curry et William Alvin Howard

L’isomorphisme de Curry-Howard porte les noms du mathématicien américain Haskell Curry et du logicien William Alvin Howard. En 1934, Curry remarqua une ressemblance mathématique frappante entre la structure des types dans la logique combinatoire (Combinatory Logic) et le système d’axiomes (style de Hilbert) pour les propositions d’implication dans la logique intuitionniste. Plus tard, en 1969, Howard publia un article montrant qu’il existe un isomorphisme parfait entre la « déduction naturelle » (Natural Deduction) formulée par Gerhard Gentzen et le « lambda-calcul » (Lambda Calculus) d’Alonzo Church, établissant fermement ce concept.

La logique intuitionniste et la constructivité rigoureuse de l’interprétation BHK

En logique classique, une proposition possède une valeur de vérité, soit « vrai » soit « faux » (tiers exclu). Cependant, la logique intuitionniste (Intuitionistic Logic), fondée par L. E. J. Brouwer, rejette le concept de valeur de vérité et définit qu’« une proposition est vraie si l’on peut construire sa preuve (évidence) ». La formulation rigoureuse de cette position est l’interprétation BHK (interprétation de Brouwer-Heyting-Kolmogorov).

Selon l’interprétation BHK, la « preuve » de chaque connecteur logique est définie de manière constructive comme suit :

• Une preuve de la proposition $A \land B$ est une paire $(p, q)$, où $p$ est une preuve de $A$ et $q$ est une preuve de $B$.
• Une preuve de la proposition $A \lor B$ est une paire $(0, p)$ ou $(1, q)$, où $p$ est une preuve de $A$ et $q$ une preuve de $B$. L’étiquette (0 ou 1) indique explicitement laquelle a été prouvée.
• Une preuve de la proposition $A \to B$ est une fonction $f$. Cette fonction prend en entrée n’importe quelle preuve $x$ de $A$ et produit une preuve $f(x)$ de $B$.
• Il n’existe pas de preuve de la proposition $\bot$ (contradiction).
• Une preuve de la proposition $\exists x \in D, P(x)$ est une paire $(d, p)$, où $d \in D$ est un objet concret et $p$ est une preuve de $P(d)$.
• Une preuve de la proposition $\forall x \in D, P(x)$ est une fonction $f$. Cette fonction produit une preuve $f(d)$ de $P(d)$ pour n’importe quel $d \in D$.

Si l’on regarde cette interprétation du point de vue de la programmation, une « proposition » n’est autre qu’un « type (Type) » et une « preuve » n’est autre qu’« une valeur (programme, fonction) ayant ce type ». La construction de preuves en logique intuitionniste est exactement la même chose que la construction de structures de données et d’algorithmes.

Chapitre 2 : Tableau comparatif complet et formulation rigoureuse de la déduction naturelle et des règles de typage

Le cœur de la correspondance de Curry-Howard réside dans la coïncidence parfaite entre les règles d’inférence de la déduction naturelle de Gentzen et les règles de typage du lambda-calcul simplement typé. Voici ci-dessous un tableau de comparaison rigoureux des règles d’introduction (Introduction Rule) et des règles d’élimination (Elimination Rule) pour chaque connecteur logique.

Le contexte $\Gamma$ représente l’ensemble des hypothèses (paires de variables et de leurs types). $\Gamma \vdash M : A$ signifie « dans le contexte $\Gamma$, le terme $M$ est de type $A$ (c’est-à-dire qu’il est une preuve de la proposition $A$) ».

Implication ($\to$) et Type de Fonction

Si l’on peut prouver $B$ (terme $M$) en introduisant l’hypothèse $A$ (variable $x$), alors on prouve l’implication de $A$ vers $B$ (fonction $\lambda x:A. M$). C’est exactement la définition d’une fonction anonyme.

Lorsqu’on a une preuve $M$ (fonction) de $A \to B$ et une preuve $N$ (argument) de $A$, on obtient une preuve $M\ N$ de $B$ en les appliquant (Apply). C’est le syllogisme (Modus Ponens).

Conjonction ($\land$) et Type Produit (Product Type / Tuple)

Si l’on dispose d’une preuve de $A$ et d’une preuve de $B$, on prouve $A \land B$ en les mettant en paire.

L’opération $\pi_1$ qui extrait le premier élément de la paire $P$ déduit $A$, tandis que l’opération $\pi_2$ qui extrait le second élément déduit $B$.

Disjonction ($\lor$) et Type Somme (Sum Type / Either / Coproduct)

Si l’on a une preuve de $A$ ou de $B$, on peut construire $A \lor B$. Cela correspond à Left ou Right en Haskell.

Si $A \lor B$ est vérifié, et que l’on peut déduire $C$ à partir de $A$ ainsi que $C$ à partir de $B$, alors on conclut $C$. C’est l’analyse de cas (pattern matching) en programmation.

Contradiction ($\bot$) et Type Vide (Empty Type / Void)

Si la contradiction $\bot$ est prouvée, on peut déduire n’importe quelle proposition $A$. Cela correspond à une fonction virtuelle abort qui produit une valeur arbitraire à partir du type vide (Void) qui n’a aucun élément (en réalité, elle n’est jamais appelée).

Chapitre 3 : Normalisation des preuves (Cut Elimination) et coïncidence mathématique de la $\beta$-réduction

Le « théorème de normalisation » (Normalization Theorem) est un théorème important en déduction naturelle. Gentzen a montré que la « règle de coupure » (Cut Rule) pouvait être éliminée dans le calcul des séquents (Théorème d’élimination des coupures, Gentzen’s Hauptsatz). En déduction naturelle, cela signifie que « les détours (Detours) consistant à appliquer une règle d’élimination immédiatement après une règle d’introduction peuvent être transformés en une preuve directe ».

De manière étonnante, ce processus de « transformation et simplification des preuves » en logique est parfaitement identique à l’« exécution d’un programme (évaluation) » en lambda-calcul, c’est-à-dire la $\beta$-réduction (Beta Reduction).

Normalisation et $\beta$-réduction dans l’implication

Considérons la preuve (programme) suivante contenant un détour :

1. En supposant $x:A$, on dérive $M:B$, et on introduit l’implication ($\to\text{-}I$) pour $A \to B$. C’est-à-dire $\lambda x:A. M$.
2. Immédiatement après, on utilise une preuve $N$ de $A$ pour éliminer l’implication ($\to\text{-}E$). C’est-à-dire $(\lambda x:A. M)\ N$.

D’un point de vue logique, on introduit une hypothèse $x$ pour créer une preuve, et on substitue immédiatement une preuve concrète $N$ à cette hypothèse. C’est redondant ; si on intègre directement $N$ partout où l’hypothèse $x$ apparaît dans $M$, on obtient directement une preuve de $B$. Du point de vue de la science informatique, il s’agit précisément de l’application d’une fonction, où l’argument $N$ est substitué au paramètre $x$ lors de l’exécution.

C’est la $\beta$-réduction. L’« élimination des coupures dans une preuve » en logique est exactement la même étape de calcul effectuée par un programme.

Théorème de normalisation forte et théorème de Church-Rosser

Dans le lambda-calcul simplement typé, tout terme typable atteint nécessairement un état où il ne peut plus être calculé (forme normale, Normal Form) en un nombre fini de $\beta$-réductions. C’est ce qu’on appelle le « Théorème de normalisation forte » (Strong Normalization Theorem). Cela correspond au fait logique que « toute preuve peut toujours être réécrite en une preuve directe sans détours ». De plus, selon le théorème de Church-Rosser, la forme normale finale est unique, quel que soit l’ordre d’évaluation. Dans les systèmes possédant la propriété de normalisation forte, les programmes s’arrêtent toujours (incomplets au sens de Turing). S’il existait une boucle infinie (par exemple, le combinateur Y ou $\Omega = (\lambda x. x\ x)(\lambda x. x\ x)$), cela signifierait logiquement un « paradoxe par auto-référence », ce qui détruirait la cohérence (non-contradiction) du système.

Chapitre 4 : Correspondance entre les Types Dépendants (Dependent Types) et la logique du premier ordre

Les correspondances vues jusqu’à présent se limitaient à la logique propositionnelle (Propositional Logic). L’extension de la correspondance de Curry-Howard à la « logique du premier ordre » (First-Order Logic) est la « théorie des types dépendants » (Dependent Type Theory), construite par Per Martin-Löf et d’autres.

Un type dépendant est un « type qui varie en fonction d’une valeur (terme) ». Par exemple, le type d’un « vecteur de longueur $n$ » dépend de la valeur de l’entier naturel $n$.

Quantificateur universel $\forall$ et Type produit dépendant (Type $\Pi$)

La proposition universelle $\forall x:A, B(x)$, signifiant « pour tout $x \in A$, $B(x)$ est vérifié », peut être vue comme une fonction prenant un argument $x:A$ et renvoyant une valeur de type $B(x)$. Le type de cette fonction est appelé Type $\Pi$ (Pi Type, Dependent Product Type).

Par exemple, la preuve du théorème « pour tout entier naturel $n$, $n+n = 2n$ » est implémentée comme une fonction qui prend un entier naturel $n$ comme argument et renvoie « une preuve de $n+n = 2n$ (une valeur ayant ce type) ».

Quantificateur existentiel $\exists$ et Type somme dépendant (Type $\Sigma$)

La proposition existentielle $\exists x:A, B(x)$, signifiant « il existe un $x \in A$ tel que $B(x)$ soit vérifié », est représentée par une paire composée d’« une valeur concrète $x$ satisfaisant la condition » et de « la preuve que ce $x$ satisfait la condition ». On l’appelle Type $\Sigma$ (Sigma Type, Dependent Sum Type).

Ainsi, une « fonction qui renvoie un tableau trié » ne se contente pas de renvoyer un tableau, mais peut être strictement typée comme une fonction renvoyant une paire $\Sigma$ contenant « le tableau renvoyé $y$ » et « la preuve que $y$ est trié ». C’est la base de la « correction par construction » (Correct-by-Construction).

Chapitre 5 : Preuve de théorèmes mathématiques avec Lean 4 / Coq et explications (Pratique)

Voyons comment les preuves mathématiques réelles sont écrites sous forme de programmes à l’aide d’assistants de preuve modernes basés sur la théorie des types dépendants (comme Lean 4 ou Coq).

Lois de De Morgan (Vérification intuitionniste)

En logique classique, $\neg(A \lor B) \iff \neg A \land \neg B$ est valable, mais en logique intuitionniste, ce sens de l’équivalence est également prouvable. Voici une preuve en Lean 4. Notez que dans Lean, la négation $\neg A$ est définie comme $A \to \bot$ (une fonction qui dérive une contradiction en supposant A).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

-- Lean 4 : Une partie de la loi de De Morgan ¬(A ∨ B) → ¬A ∧ ¬B
theorem de_morgan_1 {A B : Prop} (h : ¬(A ∨ B)) : ¬A ∧ ¬B :=
  -- And.intro est la règle d'introduction (construction de paire) pour la conjonction (∧).
  And.intro
    -- Premier élément : preuve de ¬A (c'est-à-dire A → False)
    (fun (ha : A) =>
      -- Construit A ∨ B à partir de A (Or.inl), l'applique à h pour obtenir une contradiction (False)
      h (Or.inl ha))
    -- Deuxième élément : preuve de ¬B (c'est-à-dire B → False)
    (fun (hb : B) =>
      -- Construit A ∨ B à partir de B (Or.inr), l'applique à h pour obtenir une contradiction (False)
      h (Or.inr hb))

Explication ligne par ligne :

1. h : ¬(A ∨ B) est une fonction de type (A ∨ B) → False.
2. And.intro construit la paire des preuves de ¬A et ¬B.
3. fun (ha : A) => ... est une abstraction lambda (définition de fonction). En utilisant l’argument ha, on crée une preuve de A ∨ B via Or.inl ha, qu’on passe à la fonction h pour renvoyer False.

Ainsi, une preuve n’est rien d’autre que la construction d’une expression lambda totalement sûre au niveau du typage.

Preuve par récurrence de l’associativité de la concaténation de listes

Pour l’opération de concaténation de listes ++ bien connue en programmation, nous allons prouver l’associativité (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) par récurrence mathématique. En théorie des types, la récurrence est implémentée en tant que « fonction récursive » (Recursive Function).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

-- Lean 4 : Associativité de la concaténation de listes
theorem append_assoc {α : Type} (l1 l2 l3 : List α) : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) :=
  match l1 with
  -- Cas de base : si l1 est la liste vide []
  | [] =>
    -- [] ++ l2 se réduit à l2, donc l2 ++ l3 = l2 ++ l3, ce qui est trivial (Reflexivity)
    rfl
  -- Étape d'hérédité : si l1 est de la forme head :: tail
  | head :: tail =>
    -- On utilise l'associativité sur tail comme hypothèse de récurrence (appel récursif)
    have ih : (tail ++ l2) ++ l3 = tail ++ (l2 ++ l3) := append_assoc tail l2 l3
    -- (head :: tail ++ l2) ++ l3 se réduit à head :: ((tail ++ l2) ++ l3)
    -- On réécrit l'expression (rewrite) en utilisant l'hypothèse de récurrence `ih`
    by rw [ih]

Ici, le filtrage par motif match sur la structure de la liste fournit la structure de la récurrence mathématique, et l’appel récursif append_assoc tail l2 l3 correspond à l’hypothèse de récurrence (Induction Hypothesis). Comme la terminaison de la récursivité est garantie, cela constitue une preuve saine.

Chapitre 6 : Système F, lambda-calcul polymorphe, niveaux (univers) et paradoxe de Girard

Pour augmenter encore l’expressivité, on introduit le « polymorphisme » (Polymorphism) qui prend les types comme paramètres. Il s’agit du « Système F » (System F) ou « lambda-calcul du second ordre », découvert indépendamment par Jean-Yves Girard et John Reynolds.

Système F et quantification universelle

Le Système F autorise la quantification universelle $\forall \alpha. \tau$ sur des variables de type en tant que type. Cela a jeté les bases des génériques (Parametric Polymorphism) de langages comme Haskell. Par exemple, le type de la fonction identité polymorphe id est $\forall \alpha. \alpha \to \alpha$. D’un point de vue logique, cela correspond à la « logique propositionnelle du second ordre » (une logique qui permet la quantification sur des variables propositionnelles).

Niveaux (Universe Levels) et paradoxe de Girard

Lors de la conception du Système F ou de la théorie des types dépendants, le type Type, qui représente « l’ensemble de tous les types », peut-il s’avoir lui-même comme type (Type : Type) ? Si l’on permet cela, le « paradoxe de Girard » (Girard’s Paradox), l’équivalent du paradoxe de Russell en théorie des types, se produit. De manière similaire au paradoxe de Burali-Forti, on peut construire l’« ensemble de tous les nombres ordinaux » en utilisant la structure des nombres ordinaux, ce qui conduit à une contradiction (une preuve de $\bot$) par auto-référence.

Cela empêche l’auto-référence et permet d’exprimer des structures mathématiques riches tout en préservant la cohérence du système logique.

Chapitre 7 : Types d’identité et interprétation topologique des chemins en théorie des types homotopique (HoTT)

Au XXIe siècle, la correspondance de Curry-Howard s’est liée à la topologie et à la théorie des catégories, donnant naissance à un nouveau paradigme : la « Théorie des Types Homotopique » (Homotopy Type Theory ; HoTT). Cette théorie, menée par le médaillé Fields Vladimir Voevodsky, cherche à réécrire fondamentalement les bases des mathématiques.

Types d’identité (Identity Types) et chemins (Paths)

En théorie des types dépendants, l’affirmation « $x$ et $y$ sont égaux » est représentée par un type appelé Type d’identité (Identity Type) $Id_A(x, y)$. Habituellement, on considère que cela ne peut être prouvé que par réflexivité ($x = x$) (refl : Id_A(x, x)).

Cependant, dans HoTT, on donne une signification topologique à la preuve $p$ de ce $Id_A(x, y)$. C’est-à-dire que l’on interprète la « preuve $p : Id_A(x, y)$ » comme un « chemin (Path) » du point $x$ au point $y$ dans l’espace $A$. De plus, lorsqu’il existe deux preuves différentes (chemins) $p, q : Id_A(x, y)$, la preuve $\alpha : Id_{Id_A(x, y)}(p, q)$ qu’elles sont égales correspond à une « homotopie (Homotopy) », c’est-à-dire une déformation continue du chemin $p$ vers le chemin $q$. Ainsi, la structure infinie des groupoïdes supérieurs (Higher Groupoid) apparaît naturellement dans la théorie des types.

Éliminateur J et récurrence sur les chemins

La règle d’élimination des types d’identité, appelée éliminateur J (J-eliminator / Path Induction), joue un rôle extrêmement important dans HoTT. C’est une règle qui stipule : « Pour prouver une proposition $P(x, y, p)$ qui dépend de l’égalité $x = y$, il suffit de la prouver pour le cas où $x = x$ et $p = \text{refl}$ (cas de base) ». D’un point de vue topologique, cela correspond au fait qu’« un chemin constant restant au point $x$ peut être déformé continûment en n’importe quel autre chemin (contractibilité) ».

Axiome d’univalence (Univalence Axiom)

La plus grande percée introduite par Voevodsky est l’« axiome d’univalence (Univalence Axiom) ». En mathématiques, les structures isomorphes (Isomorphic) (par exemple, deux ensembles finis ayant le même nombre d’éléments, ou deux groupes ayant la même structure) sont traitées comme « substantiellement identiques ». Cependant, dans la théorie des ensembles classique (ZFC), même si elles sont isomorphes, on ne pouvait pas dire strictement qu’elles étaient « égales ».

En bref, « l’isomorphisme est l’égalité (Equality is Equivalence) ». Grâce à cet axiome, un théorème prouvé pour une représentation donnée peut être automatiquement et sûrement transporté (Transport) le long d’un chemin vers une représentation isomorphe complètement différente. Du point de vue de la programmation, une fois que l’isomorphisme entre deux structures de données est prouvé (par exemple, les nombres naturels en représentation binaire et unaire), toutes les fonctions et théorèmes écrits pour l’une des structures de données peuvent être automatiquement adaptés à l’autre, réalisant ainsi des génériques ultimes.

Conclusion : Programmation et quête de la vérité universelle

La vérité la plus importante que nous enseigne l’isomorphisme de Curry-Howard est le fait que « les mathématiques » et « l’informatique » parlent fondamentalement le même langage. Lorsque nous luttons contre les erreurs de type dans la programmation quotidienne, nous ne faisons rien d’autre que de corriger des contradictions logiques à travers un vérificateur de preuves automatisé appelé compilateur.

• Une proposition (Proposition) est un Type (Type)
• Une preuve (Proof) est un Programme (Program)
• La normalisation des preuves (Cut Elimination) est l’exécution du programme ($\beta$-Reduction)

Les puissants systèmes de types des langages de programmation fonctionnels (Haskell, OCaml, Rust, etc.) bénéficient grandement de cet isomorphisme. Et les assistants de preuve comme Coq ou Lean 4 ont complètement effacé la frontière entre la programmation et les mathématiques. Le code que nous écrivons est à la fois un algorithme exécutable et un certificat (Certificate) de vérité mathématique universelle qui garantit éternellement l’absence de bugs.

Cette profonde harmonie née à l’intersection de la théorie des types et de la logique continue de guider l’ingénierie logicielle, la transformant d’un simple « codage basé sur l’expérience » vers « la construction de vérités basées sur des fondations mathématiques rigoureuses ».