David Madore's WebLog: Une introduction à la correspondance de Curry-Howard

Les règles du calcul propositionnel intuitionniste

La logique propositionnelle ou calcul propositionnel, donc, c'est la logique des purs énoncés logiques, formés à partir des connecteurs propositionnels qui sont ‘⇒’ (l'implication logique), ‘∧’ (la conjonction logique, c'est-à-dire le et), ‘∨’ (la disjonction logique, c'est-à-dire le ou — inclusif), ‘⊤’ (le vrai, c'est-à-dire l'affirmation trivialement vraie) et ‘⊥’ (le faux, c'est-à-dire l'affirmation absurde), auxquels on peut éventuellement ajouter ‘¬’ (la négation logique) et ‘⇔’ (l'équivalence logique).

Par exemple, un énoncé comme (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C), que je vais démontrer ci-dessous et qui se lit si A ou B implique C, alors A implique C et B implique C, est un énoncé propositionnel (formé à partir des variables A,B,C…).

En revanche, la logique propositionnelle n'a pas quantificateurs, c'est-à-dire ‘∀’ et ‘∃’ (qui apparaissent dans la logique du premier ordre ou calcul des prédicats, voire la logique d'ordre supérieur[#2]) ; bref, la logique propositionnelle est la logique la plus simple qui soit. Mais pour l'instant (dans cette section) mon but est de parler de ça et uniquement de ça : comment on démontre des choses là-dedans, et comment on convertit ces démonstrations en programmes.

[#2] On peut quand même imaginer qu'il y a une quantification universelle implicite sur toutes les variables propositionnelles de la formule : (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C) signifie, si on veut, ∀A. ∀B. ∀C. (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C). Cette quantification implicite (du simple fait que les variables n'aient pas d'hypothèse) sera rendue explicite dans la partie finale de ce billet, et correspondra après Curry-Howard au polymorphisme, mais je ne rentrerai pas trop dans les détails. Pour l'instant, cette quantification propositionnelle (et le polymorphisme qui va avec) reste implicite et tacite.

Une formule propositionnelle ou simplement propositions, donc, c'est une formule fabriquée à partir de variables propositionnelles (notées, disons, A, B, C… supposées en nombre infini), qui représentent des énoncés opaques non spécifiés, avec les connecteurs propositionnels que je viens de lister : ‘⇒’, ‘∧’, ‘∨’ sont binaires (c'est-à-dire qu'on les place entre deux propositions pour former une nouvelle proposition, avec des parenthèses pour éviter l'ambiguïté éventuelle), et ‘⊤’ et ‘⊥’ sont « nullaires » (c'est-à-dire que ce sont des propositions à eux seuls). On traite ‘¬’ (la négation logique) comme une simple abréviation : ¬P est un raccourci de notation pour P⇒⊥ (si P alors absurde) ; et, si on veut l'autoriser, ‘⇔’ (l'équivalence logique) de même, en décidant que (P⇔Q) abrège ((P⇒Q)∧(Q⇒P)).

Pour qu'on soit bien d'accord sur la syntaxe : les formules propositionnelles sont formées inductivement par : les variables propositionnelles, ou bien l'application d'un connecteur, sous la forme (P⇒Q), (P∧Q), (P∨Q), ⊤ ou ⊥, où P,Q sont elles-mêmes des formules propositionnelles. On se permet d'omettre les parenthèses avec les conventions suivantes : ‘¬’ est prioritaire sur ‘∧’, qui est prioritaire sur ‘∨’, qui est prioritaire sur ‘⇒’ (qui est peut-être lui-même prioritaire sur ‘⇔’ mais c'est de mauvais goût de se servir de ça pour omettre des parenthèses) ; et ‘∧’ et ‘∨’ s'associent à gauche mais ça n'aura pas d'importance, tandis que ‘⇒’ s'associe à droite, c'est-à-dire que P⇒Q⇒R doit se comprendre comme P⇒(Q⇒R) lorsque c'est une formule propositionnelle, et pas (P⇒Q)⇒R ni (P⇒Q)∧(Q⇒R) qui est le sens qu'on lui donne souvent dans un texte informel.

La logique classique, ou en l'occurrence, spécifiquement, le calcul propositionnel classique, est la logique de base des mathématiques : elle autorise notamment le raisonnement par l'absurde (qu'on peut reformuler de différentes manières) ; et on l'appelle aussi logique booléenne car elle peut la modéliser comme un système de calcul avec deux valeurs de vérité (représentées, justement par le vrai et le faux), formalisé par George Boole vers 1847–1854.

La logique intuitionniste est une logique plus faible qui, essentiellement, retire cette possibilité du raisonnement par l'absurde, ou loi du tiers exclu : je ne reviens pas sur l'histoire ou les motivations de l'intuitionnisme que j'ai essayé d'esquisser dans ce billet déjà lié ci-dessus, mais disons que tout ce qui est valable (i.e., démontrable) en logique intuitionniste (par exemple A∧(B∨C) ⇔ (A∧B)∨(A∧C) ou bien (A∨B ⇒ C) ⇔ (A⇒C)∧(B⇒C)) est aussi valable en logique classique ; en revanche, certaines choses valables en logique classique ne le sont pas en logique intuitionniste (par exemple la loi du tiers exclu A∨¬A, justement, ou bien l'élimination de la double négation ¬¬A⇒A, la « décontraposition » (¬B⇒¬A) ⇒ (A⇒B), la loi faible du tiers exclu ¬¬A∨¬A, ou bien encore (A∧B ⇒ C) ⇒ (A⇒C)∨(B⇒C) ni même son cas particulier ¬(A∧B) ⇒ ¬A∨¬B : toutes ces choses sont des théorèmes de la logique classique mais pas de la logique intuitionniste).

Les règles de raisonnement du calcul propositionnel intuitionniste sont les suivantes (ici présentées en style « déduction naturelle ») : on raisonne en permanence avec un certain nombre d'hypothèses, dont peut à tout moment ouvrir de nouvelles, mais les conclusions ne sont alors valables que sous les hypothèses actuellement ouvertes, sauf si une des règles énoncées ci-dessous permet de les décharger (ce sera plus clair avec les exemples après, enfin j'espère) :

(Hypothèse)

Si un énoncé fait partie des hypothèses courantes, alors on peut l'affirmer.

(Introduction du ‘⇒’)

Si sous une hypothèse P (c'est-à-dire : en rajoutant celle-ci aux hypothèses en cours) on a démontré Q, alors, sans cette hypothèse (c'est-à-dire en la déchargeant), on peut en tirer P⇒Q.

(Élimination du ‘⇒’ ou modus ponens)

Si on a démontré P⇒Q et qu'on a démontré P, alors on peut en tirer Q.

(Introduction du ‘∧’)

Si on a démontré Q₁ et Q₂, alors on peut en tirer Q₁∧Q₂.

(Élimination du ‘∧’)

Si on a démontré Q₁∧Q₂, alors on peut en tirer Q₁, et on peut en tirer Q₂ [ce sont là deux règles séparées].

(Introduction du ‘∨’)

Si on a démontré Q₁, ou si on a démontré Q₂, alors on peut en tirer Q₁∨Q₂ [ce sont là deux règles séparées].

(Élimination du ‘∨’ ou raisonnement par cas)

Si on a démontré P₁∨P₂, et si sous l'hypothèse P₁ on a démontré Q et que sous l'hypothèse P₂ on a aussi démontré la même conclusion Q, alors on peut tirer Q de tout ça (sans aucune hypothèse, c'est-à-dire en les déchargeant).

(Introduction du ‘⊤’)

On peut démontrer ⊤. [Il n'y a pas de règle d'élimination du ‘⊤’]

(Élimination du ‘⊥’ ou ex falso quodlibet)

Si on a démontré ⊥, on peut en tirer Q absolument quelconque. [Il n'y a pas de règle d'introduction du ‘⊥’]

Pour obtenir la logique classique, on pourrait par exemple modifier la règle d'élimination du ‘⊥’ en règle de raisonnement par l'absurde : si sous l'hypothèse ¬Q on a démontré ⊥, alors sans cette hypothèse on peut en tirer Q. Mais je répète que je ne veux pas autoriser ça dans ce billet.

Pour illustrer le fonctionnement des règles ci-dessus, voici un exemple de démonstration dans lequel j'ai écrit de façon parfaitement méticuleuse chaque étape du raisonnement : je vais prouver (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C) :

• (1) Faisons l'hypothèse : A∨B ⇒ C
  • (2) Faisons l'hypothèse : A
    • (3) De (2), par introduction gauche du ‘∨’, on tire : A∨B
    • (4) De (1) et (3), par élimination du ‘⇒’, on tire : C
  • (Fin de l'hypothèse A)
  • (5) De la décharge de (2) dans (4), par introduction du ‘⇒’, on tire : A⇒C
  • (6) Faisons l'hypothèse : B
    • (7) De (6), par introduction droite du ‘∨’, on tire : A∨B
    • (8) De (1) et (7), par élimination du ‘⇒’, on tire : C
  • (Fin de l'hypothèse B)
  • (9) De la décharge de (6) dans (8), par introduction du ‘⇒’, on tire : B⇒C
  • (10) De (5) et (9), par introduction du ‘∧’, on tire : (A⇒C)∧(B⇒C)
• (Fin de l'hypothèse A∨B ⇒ C)
• (11) De la décharge de (1) dans (10), par introduction du ‘⇒’, on tire : (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C)

(Informellement, on écrira plutôt : supposons A∨B ⇒ C : alors si on a A on a A∨B donc C par notre hypothèse, ce qui prouve A⇒C, et de même si on a B on a A∨B donc C, ce qui prouve B⇒C, bref, on a (A⇒C)∧(B⇒C), et tout ceci montre (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C)… enfin, à vrai dire, informellement, on écrira plutôt c'est évident.)

Et dans l'autre sens, je prouve (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C) :

• (1) Faisons l'hypothèse : (A⇒C)∧(B⇒C)
  • (2) De (1), par élimination gauche du ‘∧’, on tire : A⇒C
  • (3) De (1), par élimination droite du ‘∧’, on tire : B⇒C
  • (4) Faisons l'hypothèse : A∨B
    • (5) Faisons l'hypothèse : A
      • (6) De (2) et (5), par élimination du ‘⇒’, on tire : C
      • (Fin de l'hypothèse A)
    • (7) Faisons l'hypothèse : B
      • (8) De (3) et (7), par élimination du ‘⇒’, on tire : C
      • (Fin de l'hypothèse B)
    • (9) De (4), de la décharge de (5) dans (6) et de celle de (7) dans (8), par élimination du ‘∨’, on tire : C
  • (Fin de l'hypothèse A∨B)
  • (10) De la décharge de (4) dans (9), par introduction du ‘⇒’, on tire : A∨B ⇒ C
• (Fin de l'hypothèse (A⇒C)∧(B⇒C))
• (11) De la décharge de (1) dans (10), par introduction du ‘⇒’, on tire : (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C)

(Informellement, on écrira plutôt : supposons (A⇒C)∧(B⇒C), donc A⇒C d'une part et B⇒C de l'autre ; si on suppose A∨B, on peut en tirer C dans le cas A parce que A⇒C, et dans le cas B parce que B⇒C, donc dans tous les cas : ceci montre A∨B ⇒ C, donc le tout montre (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C).)

Présentation en « séquents » des règles

Si on souhaite écrire les règles de façon encore plus précise et pointilleuse, et surtout, mémoriser quelles sont les hypothèses ouvertes à un point donné de la démonstration, le mieux est d'utiliser la notation séquent : on note P₁,…,P_r ⊢ Q pour dire on a démontré Q sous les hypothèses P₁,…,P_r. Les règles (toujours de la « déduction naturelle » : ce sont les mêmes règles que ci-dessus) sont alors écrites ainsi (en abrégeant par Γ un ensemble quelconque d'hypothèses ; noter que leur ordre n'a pas d'importance, par contre pour obtenir une correspondance de Curry-Howard parfaite il sera pertinent d'autoriser certaines hypothèses d'y figurer plusieurs fois, auquel cas il faut décider, dans une démonstration, laquelle des hypothèses identiques on a invoquée lorsqu'on en a plusieurs) :

(Hypothèse)

On a Γ,Q ⊢ Q.

(Introduction du ‘⇒’)

Si Γ,P ⊢ Q, alors Γ ⊢ P⇒Q.

(Élimination du ‘⇒’ ou modus ponens)

Si Γ ⊢ P⇒Q et Γ ⊢ P, alors Γ ⊢ Q.

(Introduction du ‘∧’)

Si Γ ⊢ Q₁ et Γ ⊢ Q₂, alors Γ ⊢ Q₁∧Q₂.

(Élimination du ‘∧’)

Si Γ ⊢ Q₁∧Q₂, alors Γ ⊢ Q₁ et Γ ⊢ Q₂ [ce sont là deux règles séparées].

(Introduction du ‘∨’)

Si Γ ⊢ Q₁, ou bien si Γ ⊢ Q₂, alors Γ ⊢ Q₁∨Q₂ [ce sont là deux règles séparées].

(Élimination du ‘∨’ ou raisonnement par cas)

Si Γ ⊢ P₁∨P₂ et Γ,P₁ ⊢ Q et Γ,P₂ ⊢ Q, alors Γ ⊢ Q.

(Introduction du ‘⊤’)

On a Γ ⊢ ⊤.

(Élimination du ‘⊥’ ou ex falso quodlibet)

Si Γ ⊢ ⊥, alors Γ ⊢ Q.

On peut noter que ces règles ont comme conséquence immédiate la règle d'affaiblissement (qui affirme qu'ajouter des hypothèses inutiles ne peut pas corrompre une démonstration) : si Γ ⊢ Q alors Γ,P ⊢ Q.

Par exemple, mes deux exemples de preuves se réécrivent ainsi avec le symbole ‘⊢’ pour indiquer à chaque moment le jeu d'hypothèses ouvertes (au lieu de le faire par l'indentation comme ci-dessus) :

• (1) Par hypothèse : A∨B ⇒ C ⊢ A∨B ⇒ C
• (2) Par hypothèse : A∨B ⇒ C, A ⊢ A
• (3) De (2), par introduction gauche du ‘∨’ : A∨B ⇒ C, A ⊢ A∨B
• (4) De (1) et (3), par élimination du ‘⇒’ : A∨B ⇒ C, A ⊢ C
• (5) De (4), par introduction du ‘⇒’ : A∨B ⇒ C ⊢ A⇒C
• (6) Par hypothèse : A∨B ⇒ C, B ⊢ B
• (7) De (6), par introduction droite du ‘∨’ : A∨B ⇒ C, B ⊢ A∨B
• (8) De (1) et (7), par élimination du ‘⇒’ : A∨B ⇒ C, B ⊢ C
• (9) De (8), par introduction du ‘⇒’ : A∨B ⇒ C ⊢ B⇒C
• (10) De (5) et (9), par introduction du ‘∧’ : A∨B ⇒ C ⊢ (A⇒C)∧(B⇒C)
• (11) De (10), par introduction du ‘⇒’ : ⊢ (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C)

et

• (1) Par hypothèse : (A⇒C)∧(B⇒C) ⊢ (A⇒C)∧(B⇒C)
• (2) De (1), par élimination gauche du ‘∧’ : (A⇒C)∧(B⇒C) ⊢ A⇒C
• (3) De (1), par élimination droite du ‘∧’ : (A⇒C)∧(B⇒C) ⊢ B⇒C
• (4) Par hypothèse : (A⇒C)∧(B⇒C), A∨B ⊢ A∨B
• (5) Par hypothèse : (A⇒C)∧(B⇒C), A∨B, A ⊢ A
• (6) De (2) et (5), par élimination du ‘⇒’ : (A⇒C)∧(B⇒C), A∨B, A ⊢ C
• (7) Par hypothèse : (A⇒C)∧(B⇒C), A∨B, B ⊢ B
• (8) De (3) et (7), par élimination du ‘⇒’ : (A⇒C)∧(B⇒C), A∨B, B ⊢ C
• (9) De (4), (6) et (8), par élimination du ‘∨’ : (A⇒C)∧(B⇒C), A∨B ⊢ C
• (10) De (9), par introduction du ‘⇒’ : (A⇒C)∧(B⇒C) ⊢ A∨B ⇒ C
• (11) De (10), par introduction du ‘⇒’ : ⊢ (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C)

Une notation pour les démonstrations : le λ-terme

La raison pour laquelle j'ai donné ces règles avec autant de détail, c'est pour introduire des notations pour elles, et pour les preuves : c'est en réinterprétant cette notation qu'on va définir la correspondance de Curry-Howard.

Je vais donc maintenant introduire une notation v₁:P₁,…,v_r:P_r ⊢ t:Q pour dire t désigne une preuve de Q dans laquelle les variables libres v₁,…,v_r désignent des hypothèses qui supposent P₁,…,P_r : le point intéressant c'est que t, dans cette histoire, est une expression (ou λ-terme) formée à partir des variables v₁,…,v_r, et cette expression enregistre toute la démonstration (alors que Q n'en est que la conclusion).

Je définis mes notations en reprenant exactement les mêmes règles que ci-dessus, mais en introduisant une notation ad hoc pour chaque règle (mes notations sont un petit peu idiosyncratiques, mais elles le ne sont pas déraisonnablement — au moins celles concernant l'introduction et l'élimination du ‘⇒’ sont très standard) ; je répète que ce qu'il faut surtout bien regarder c'est la partie entre le symbole ‘⊢’ et le ‘:’ qui suit, parce que c'est ça la notation que je suis en train de définir :

(Hypothèse)

On a Γ,v:Q ⊢ v:Q. C'est-à-dire que pour signifier l'utilisation d'une hypothèse, la notation est simplement de reprendre la variable v sous laquelle on a désigné cette hypothèse.

(Introduction du ‘⇒’)

Si Γ,v:P ⊢ t:Q, alors Γ ⊢ λ(v:P).t : P⇒Q (la variable v devient liée dans la notation λ(v:P).t, avec les conventions usuelles sur les variables liées, c'est-à-dire qu'on peut les changer à volonté dans la notation sans que ça change le terme). C'est-à-dire que la décharge de l'hypothèse v qui supposait P pour passer de Q à P⇒Q se dénote en écrivant λ(v:P). devant la preuve de Q (qui utilisait l'hypothèse v).

(Élimination du ‘⇒’ ou modus ponens)

Si Γ ⊢ f : P⇒Q et Γ ⊢ x : P, alors Γ ⊢ (fx) : Q. C'est-à-dire que le modus ponens se dénote en concaténant simplement les preuves f de la majeure P⇒Q et x de la mineure P (les parenthèses servant, bien sûr, à éviter l'ambiguïté).

(Introduction du ‘∧’)

Si Γ ⊢ x₁:Q₁ et Γ ⊢ x₂:Q₂, alors Γ ⊢ ⟨x₁,x₂⟩ : Q₁∧Q₂.

(Élimination du ‘∧’)

Si Γ ⊢ x : Q₁∧Q₂, alors Γ ⊢ (π₁x) : Q₁ et Γ ⊢ (π₂x) : Q₂ [ce sont là deux règles séparées].

(Introduction du ‘∨’)

Si Γ ⊢ x : Q₁, alors Γ ⊢ (ι₁^(Q₁,Q₂)x) : Q₁∨Q₂, et si Γ ⊢ x : Q₂, alors Γ ⊢ (ι₂^(Q₁,Q₂)x) : Q₁∨Q₂ [ce sont là deux règles séparées].

(Élimination du ‘∨’ ou raisonnement par cas)

Si Γ ⊢ x : P₁∨P₂ et Γ,v₁:P₁ ⊢ t₁ : Q et Γ,v₂:P₂ ⊢ t₂ : Q, alors Γ ⊢ (match x with ι₁v₁↦t₁, ι₂v₂↦t₂) : Q (les variables v₁ et v₂, qui peuvent d'ailleurs être la même, deviennent liées dans la notation (match x with ι₁v₁↦t₁, ι₂v₂↦t₂)). Cette règle est un peu compliquée parce qu'on combine trois démonstrations : celle x qui prouve P₁∨P₂, et celles t₁ et t₂ qui prouvent la même conclusion Q à partir des hypothèses P₁ et P₂ respectivement (les deux « cas » du raisonnement par cas), lesquelles sont notées par les variables v₁ et v₂.

(Introduction du ‘⊤’)

On a Γ ⊢ •:⊤.

(Élimination du ‘⊥’ ou ex falso quodlibet)

Si Γ ⊢ x:⊥, alors Γ ⊢ (exfalso^(Q) x) : Q.

Je souligne que les règles usuelles sur les variables liées ont cours : λ(v:U).t est, pour moi, exactement la même chose que λ(w:U).t[v←w] où t[v←w] désigne le terme obtenu en remplaçant v par w dans t (sauf là où v a été re-lié par un autre λ, parce que du coup ce n'est plus le même v justement) ou λ(u:U).t[v←u] : tout ça est pour moi le même terme : les variables liées n'existent même plus en tant que variables, elles ne sont que des pointeurs du lié vers le liant. C'est la convention usuelle des mathématiques, donc je ne m'appesantis pas dessus.

Le t ainsi formé (celui qui désigne la preuve) s'appelle le terme de preuve ou λ-terme de preuve.

Par exemple, la preuve que j'ai donnée plus haut de (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C) s'écrit, dans ces notations (à quelques libertés près avec les parenthèses qui, j'espère, ne déstabiliseront personne) par le λ-terme suivant :

λ(u:A∨B ⇒ C). ⟨λ(x:A).u(ι₁^(A,B)x), λ(y:B).u(ι₂^(A,B)y)⟩

De même, la démonstration que j'ai donnée de (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C) s'écrit par le λ-terme suivant :

λ(u:(A⇒C)∧(B⇒C)). λ(z:A∨B). (match z with ι₁v ↦ (π₁u)v, ι₂v ↦ (π₂u)v)

On devrait pouvoir le vérifier en reprenant point par point les deux démonstrations que j'ai données et en construisant le nom à chaque étape (on devrait retrouver exactement les termes que j'ai donnés, à ceci près que le choix des noms des variables pour les hypothèses — ce que j'ai appelé u,v,x,y,z, est arbitraire et sans importance).

Ce n'est peut-être pas archi lisible, mais c'est quand même plus court à écrire que les deux preuves en 11 points écrites plus haut. Et avec un peu d'habitude ça ne se lit pas si mal : λ(v:P) se lit supposons P et donnons le nom v à cette hypothèse, pour que je puisse au final conclure P⇒(⋯), et fx se lit appliquons le modus ponens à la conclusion de f sur la conclusion de x, et ainsi de suite.

Pour donner un autre exemple, une preuve de (A⇒B)∨(A⇒C) ⇒ (A ⇒ B∨C) est donnée par le λ-terme :

λ(u:(A⇒B)∨(A⇒C)). λ(z:A). (match u with ι₁v ↦ ι₁^(B,C)(vz), ι₂v ↦ ι₂^(B,C)(vz))

Il devrait être raisonnablement clair que non seulement chaque démonstration donne naissance à un λ-terme et que le λ-terme permet de retrouver la démonstration (à des permutations triviales près sur l'ordre dans lequel on écrit des bouts « qui commutent »), mais même que c'est un objet bien plus fondamental et agréable à manier que la démonstration en « points itemisés ». Donc pour tout ce que j'ai envie de raconter, je considérerai désormais que le λ-terme « est » la démonstration.

L'interprétation des λ-termes comme des programmes

L'intérêt d'avoir défini un λ-terme pour chaque preuve, c'est que ce λ-terme admet d'autres interprétations possibles que comme une preuve.

Aparté : Les lecteurs sophistiqués (mais on peut se demander ce qu'ils font à lire ce billet qui ne leur apprendra rien, et les autres devraient sauter la fin de ce paragraphe donc en fait personne ne devrait le lire) pourront dire que les λ-termes sont une notation pour les flèches de la catégorie bicartésienne close (BiCC) libre construite sur le stock de variables, et qu'on a juste défini une notation pour chaque construction de cette catégorie. L'observation fondamentale est alors que les preuves du calcul propositionnel intuitionniste sont des flèches de cette catégorie BiCC libre, et on peut même s'en servir pour décréter que deux preuves sont la même si et seulement si les flèches sont égales dans la catégorie BiCC libre ; ensuite, trouver une interprétation de la preuve dans telle ou telle catégorie C revient simplement à observer que cette dernière est BiCC donc on a un foncteur depuis la catégorie BiCC libre. Je crois que c'est ça qu'on appelle la correspondance de Curry-Howard-Lambek. Néanmoins, je ne suis pas sûr de savoir utiliser ces remarques sophistiquées pour définir le Curry-Howard « programmes », d'une part parce que ce n'est pas clair pour moi quel doit être la catégorie BiCC C de « programmes » à laquelle on applique cette observation (sauf à tomber dans une tautologie consistant à définir pour C le λ-calcul simplement typé enrichi de types produits et sommes, défini… justement comme la catégorie BiCC libre, auquel cas on a juste défini le foncteur identité et on n'a rien dit du tout) ; d'autre part, parce que ma notation distingue un λ-terme et son réduit (elle est plus fine que la β-réduction), or justement dans une catégorie BiCC on ne peut pas faire cette distinction. Bref, je ne sais pas si l'abstract nonsense nous sauve tellement ici.

À ce stade, donc, la correspondance de Curry-Howard revient à reprendre la notation que j'ai introduite ci-dessus pour les preuves et à réinterpréter ces λ-termes comme des programmes. Plus exactement, ce qu'on obtient sont des termes du λ-calcul simplement typé enrichi de types produits et sommes (et unité et vide), et ces termes, que j'ai décrit comme des preuves, peuvent se comprendre comme des programmes selon les explications ci-dessous.

Mon langage de programmation a des types, donc : chaque donnée manipulée relève d'un certain type. Les types en question sont formés à partir de variables de types (qui sont des types opaques, non spécifiés, sur lesquels on ne sait rien, et dont on ne peut donc manipuler les données qu'en les passant à d'autres bouts du programme) avec des constructions que sont les types fonctions, les types produits, les types sommes (et les types trivial et vide) :

• le type fonction (la notation usuelle serait quelque chose comme σ→τ, mais ici ce sera P⇒Q) correspond au type des fonctions qui prennent en argument une valeur de type P et renvoient une valeur de type Q ;
• le type produit (la notation usuelle serait quelque chose comme σ×τ, mais ici ce sera P∧Q) correspond au type des couples formés d'une valeur de type P et d'une valeur de type Q (penser : produit cartésien d'ensembles) ;
• le type somme (la notation usuelle serait quelque chose comme σ+τ, mais ici ce sera P∨Q) correspond au type données formées d'une donnée de type P ou bien d'une donnée de type Q, ainsi que d'un sélecteur qui indique dans quel cas on se trouve (penser : union disjointe d'ensembles) ;
• il y a aussi le type unité (trivial ou singleton[#3] ; la notation usuelle serait quelque chose comme 1, mais ici ce sera ⊤) qui n'a qu'une seule valeur ‘•’, et le type vide (la notation usuelle serait quelque chose comme 0, mais ici ce sera ⊥) qui n'a aucune valeur.

[#3] Signalons que, de façon extrêmement confusante, c'est le type unité (enfin, quelque chose qui y ressemble) qui est noté void en C, pas le type vide. Une fonction qui ne renvoie rien, ou qui ne prend aucun argument, est une fonction qui renvoie ou prend en argument le type unité. Une fonction qui renvoie le type vide, ou qui prend en argument le type vide, c'est une fonction qui ne peut pas renvoyer ou être appelée.

Le type d'un bout du programme (λ-terme) est obtenu en réinterprétant comme type la proposition que ce bout du λ-terme démontre (et donc le type de l'ensemble du programme est donné par la conclusion de la démonstration). Les variables propositionnelles (A,B,C…) s'interprètent comme des types opaques (des données non spécifiées), et les connecteurs logiques par ce qui vient d'être dit. Le programme dépend de variables locales v₁,…,v_r de types P₁,…,P_r (ayant certaines valeurs dans l'environnement en cours) et est défini ainsi (si on me pardonne un langage un petit peu informel) :

(Variable)

Chaque variable locale désigne sa valeur dans l'environnement en cours.

(Introduction du ‘⇒’)

Le programme noté λ(v:P).t désigne la fonction qui prend un argument de type P, évalue le programme t dans l'environnement où v a été lié à cet argument, et renvoie la valeur en question. (Cette notation λv.t pour la fonction qui prend v en argument et renvoie t est la notation usuelle du λ-calcul ; en OCaml par exemple ceci se note fun v -> t. Mais ici on veut indiquer le type de tous les objets introduits, d'où la notation avec :P.)

(Élimination du ‘⇒’)

La notation fx désigne l'application d'une fonction f à l'argument x.

(Introduction du ‘∧’)

La notation ⟨x₁,x₂⟩ désigne le couple formé des coordonnées x₁ et x₂.

(Élimination du ‘∧’)

Les notations π₁x et π₂x désignent la première et deuxième coordonnée respectivement du couple x.

(Introduction du ‘∨’)

Les notations ι₁^(Q₁,Q₂)x et ι₂^(Q₁,Q₂)x désignent l'injection de x dans la première et deuxième composante respectivement du type somme Q₁∨Q₂ (les exposants sont nécessaires pour deviner le type de la composante manquante).

(Élimination du ‘∨’ ou distinction de cas)

La notation match x with ι₁v₁↦t₁, ι₂v₂↦t₂ s'évalue, si x est à valeurs dans la première composante de P₁∨P₂, en la valeur t₁ dans laquelle la variable v₁ est liée à la valeur de x dans cette première composante, et de façon analogue pour la seconde.

(Introduction du ‘⊤’)

La notation ‘•’ désigne la valeur triviale de type unité.

(Élimination du ‘⊥’ ou ex falso quodlibet)

La notation exfalso^(Q) x ne désigne rien du tout car il n'y a pas de valeur de type vide.

En général, pour définir précisément une sémantique de langage de programmation il faudrait entrer dans des questions assez subtiles sur la stratégie d'évaluation (par exemple, dans fx, est-ce qu'on fait du « call-by-value », qui correspond à évaluer d'abord x avant de l'appliquer, ou du « call-by-name », qui correspond à évaluer x seulement aux endroits où f l'utilise). Mais pour les programmes que je définis ici, toutes ces questions disparaissent, d'une part parce que le langage est complètement « pur » (il ne peut pas produire d'effets de bord, qui sont une importante source de complications et de maux de tête dans la définition des langages informatiques réels : ici il n'y a rien de tel, on ne peut pas modifier de valeurs ni faire d'entrées-sorties ni rien qui y ressemble), et aussi en vertu d'un théorème (dû à Turing, Tait et/ou Girard) selon lequel tout programme écrit dans ce langage termine — et a le même résultat — quel que soit la stratégie d'évaluation (le λ-calcul simplement typé enrichi de types produits et sommes est fortement normalisant).

Formellement, le comportement du programme est défini par un processus appelé β-réduction qui consiste essentiellement à remplacer tous les machins de la forme (λ(v:P).t)x (un tel truc s'appelle un redex) par t[v←x] (le réduit correspondant) pour ce qui est de l'évaluation des fonctions, et des règles d'évaluation analogues et plus ou moins devinables pour la projection des couples et le matching des sommes. Les détails de comment on applique ces règles n'a pas d'importance justement parce le λ-calcul simplement typé est fortement normalisant.

Le λ-calcul simplement typé (enrichi gnagnagna) est par définition l'ensemble des termes produits par les règles que j'ai présentées ci-dessus, i.e., des λ-termes des démonstrations, réinterprétés si on veut comme des programmes : du coup, ça rend la correspondance de Curry-Howard trivialement bijective (et finalement assez inintéressante) : par définition, tout programme dans le λ-calcul simplement typé correspond à une démonstration puisqu'on a construit exprès un langage dont le typage n'autorise que ces termes-là. C'est pour ça que je dis que la partie qui me semble la plus intéressante de Curry-Howard, c'est le passage d'une preuve à un programme : le programme en question fait quelque chose, le typage est juste quelque chose qui assure qu'on n'obtient rien de plus que les démonstrations, mais le comportement du programme est quelque chose qui n'était pas du tout évident.

À titre d'exemple, et pour montrer que ce sont de vrais programmes qu'on peut vraiment écrire, en Haskell, les programmes correspondant à ma preuve λ(u:A∨B ⇒ C). ⟨λ(x:A).u(ι₁^(A,B)x), λ(y:B).u(ι₂^(A,B)y)⟩ de (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C) et à ma preuve λ(u:(A⇒C)∧(B⇒C)). λ(z:A∨B). (match z with ι₁v ↦ (π₁u)v, ι₂v ↦ (π₂u)v) de (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C) s'écrivent (après des lignes servant à définir le type somme et les projections des couples dans les notations que j'ai utilisées) :

data Sum a b = Iota1 a | Iota2 b -- Define a sum type of a and b
pi1 (x,y) = x
pi2 (x,y) = y
prog1 = \u -> (\x -> u(Iota1 x), \y -> u(Iota2 y))
-- prog1 :: (Sum a b -> c) -> (a -> c, b -> c)
prog2 = \u -> \z -> (case z of Iota1 v -> (pi1 u) v ; Iota2 v -> (pi2 u) v)
-- prog2 :: (a -> c, b -> c) -> Sum a b -> c

ou, si on préfère le OCaml :

type ('a, 'b) sum = Iota1 of 'a | Iota2 of 'b (* Define a sum type of 'a and 'b *)
let pi1 (x, y) = x
let pi2 (x, y) = y
let prog1 = fun u -> (fun x -> u(Iota1 x), fun y -> u(Iota2 y))
(* val prog1 : (('a, 'b) sum -> 'c) -> 'a -> 'c * ('b -> 'c) = <fun> *)
let prog2 = fun u -> fun z -> (match z with Iota1 v -> (pi1 u) v | Iota2 v -> (pi2 u) v)
(* val prog2 : ('a -> 'c) * ('b -> 'c) -> ('a, 'b) sum -> 'c = <fun> *)
;;

et l'un comme l'autre langage donnent à prog1 et prog2 le type (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C) et (A⇒C)∧(B⇒C) ⇒ (A∨B ⇒ C) respectivement (au nommage près des variables, et avec des notations diverses pour ‘⇒’, ‘∧’ et ‘∨’, ce dernier connecteur étant réalisé par la définition de type de la première ligne).

Remarque (sur l'effacement du typage) : Ce sont là des langages fortement typés et dont le typage (enfin, la partie que j'utilise) reproduit fidèlement ce dont j'ai besoin du λ-calcul simplement typé (enrichi gnagnagna). Mais j'insiste sur le fait, et je n'ai pas souvent vu cette observation certes évidente mais qui me plonge néanmoins dans une certaine perplexité, que ces programmes ont un sens même dans un langage non typé : ce sont vraiment des programmes, qui font des choses, et il reste quelque chose de ces programmes même quand on retire tout le typage de l'histoire. Je peux écrire mes programmes ci-dessus en Scheme, même si le Scheme n'a pas de typage. Je peux retirer toutes les annotations de type et j'obtiens un terme du λ-calcul non typé (bon, il faut décider quelque chose pour les couples et sommes, mais ce n'est pas très difficile soit d'enrichir le λ-calcul non typé de telles constructions, soit de les coder d'une façon ou d'une autre dedans, par exemple en codant ⟨x,y⟩ comme λk.kxy et ι₁z resp. ι₂z comme λkℓ.kz resp. λkℓ.ℓz). Ou encore, on peut utiliser un codage de Gödel des couples d'entiers naturels par les entiers naturels (et représenter ι₁z resp. ι₂z comme ⟨0,z⟩ resp. ⟨1,z⟩) et surtout une numérotation des fonctions générales récursives par les entiers naturels (l'application fx devient une notation pour l'évaluation de la f-ième fonction générale récursive en l'argument x, et λv.t devient une notation pour un entier naturel codant la fonction récursive qui à v associe t : il faut faire des choix arbitraires, mais on peut les faire de façon constructive) : alors Curry-Howard nous donne un entier naturel pour chaque démonstration. La raison de cette remarque est en lien avec la réflexion que je veux esquisser, dans un billet ultérieur, sur la réalisabilité (propositionnelle uniforme) et son rapport avec Curry-Howard « typé » [ajout : j'ai publié le billet en question], mais pour l'instant je me contente de ça : ce n'est pas parce que Curry-Howard produit naturellement un programme typé qu'on n'a pas le droit d'en effacer les types, et ce n'est pas pour autant que c'est inintéressant de le faire (et le programme continuera à terminer sur toute entrée qui est correctement typable). Bien sûr, en contrepartie, rien ne dit qu'on ne perde pas plein d'information comme ça, et on n'obtient certainement pas tous les programmes, ni même les programmes qui terminent, ni même les programmes qui font une manipulation potentiellement sensée au niveau des types (je compte revenir sur ce point dans un billet ultérieur).

Remarque (sur la négation) : J'aurais dû signaler quelque part plus haut, mais je ne sais pas où l'insérer, que ¬A, qui est je le rappelle une abréviation de A⇒⊥, correspond via Curry-Howard au type des fonctions de A vers le type vide… chose qui n'existe que si A est lui-même le type vide, auquel cas il n'y a qu'une seule telle fonction (à savoir la fonction vide). C'est-à-dire qu'une négation n'a jamais de contenu opérationnel, c'est une « pure promesse » (fournie par le système de typage, si on parle de la version typée) du fait qu'une valeur de type A n'existe pas. Quant à ¬¬A, c'est une promesse que le type A est habité (mais sans pour autant en donner une valeur).

Généralités (informelles) sur les quantificateurs

Je comptais initialement arrêter ce billet à ce point, mais je me suis dit qu'au point où j'en suis, il serait dommage de ne pas dire un mot sur les quantificateurs. Le problème avec les quantificateurs c'est que, côté logique ou côté typage, c'est hyper technique, il y a un zillion de systèmes qui diffèrent dans les règles détaillées de ce qu'on a le droit de quantifier et comment et on s'y perd complètement, donc je vais être plus informel et moins précis que ce que j'ai écrit ci-dessus sur le calcul propositionnel. L'idée générale des règles, côté logique, est quelque chose comme ceci (je vais parler plus bas du cas usuel de la logique du premier ordre, pour l'instant je reste délibérément vague sur ce qu'on a le droit de quantifier) :

Je peux introduire des notations pour ça, et je vais présentement le faire (je discuterai plus bas de la logique de leur choix).

Mais là où ça commence à devenir problématique c'est qu'on a besoin de notations pour les démonstrations (comme jusqu'à présent) et aussi pour les termes (notés t dans les quatre points ci-dessus) qui servent à appliquer une quantification universelle ou à exhiber une quantification existentielle : les règles ci-dessus expliquent comment on produit une démonstration, mais ne disent absolument rien sur comment on produit un terme (c'est qui ce t et d'où sort-il ?). Or j'ai envie de me concentrer vraiment sur les démonstrations, donc je vais écrire les notations en notant Γ ⊢ t : U pour dire on a produit un t de type U sans dire quoi que ce soit sur ce que ça signifie ; ni quel est le rapport entre le ‘⊢’ concernant les démonstrations (Γ ⊢ s : Q qui signifie s est une preuve de Q) et ce ‘⊢’ concernant les termes (Γ ⊢ t : U qui signifie on a produit un terme t de type U). De même, mon Γ mélange maintenant des variables concernant des objets dont on a envie de parler (notées v:U ci-dessous) et des hypothèses (comme dans toutes mes règles antérieures). À ces problèmes-là près, mes règles sont les suivantes :

Je conviens que mes choix de lettres sont assez pourris. Par exemple, on prendra bien garde au faut que dans la dernière règle, v est une variable pour un objet de type U tandis que w est une variable pour une hypothèse P(v), et dans la règle précédente, t est un terme de type U et z est une démonstration de Q(t) : c'est justement le principe du ‘∃’ de combiner ensemble deux choses qui peuvent paraître complètement hétérogènes.

Rappelons que les règles usuelles sur les variables liées ont cours : ∃(v:U).P(v) est, pour moi, exactement la même chose que ∃(w:U).P(w) ou ∃(u:U).P(u) : c'est le même terme, les variables liées n'existent même plus en tant que variables, elles ne sont que des pointeurs du lié vers le liant.

Je vais donner plus bas des exemples de démonstrations écrites sous forme de λ-termes avec ces notations. Mais en attendant, signalons qu'elles sont raisonnables si on pense intuitivement que :

• ∀(v:U).Q(v) est une sorte de « conjonction en famille » ⋀_v:U Q(v) qui doit donc correspondre par Curry-Howard à un type « produit en famille » ∏_v:U τ(v) par Curry-Howard, c'est-à-dire que τ(v) est un type qui dépend de v (un type dépendant) et ∏_v:U τ(v) est le type correspondant à se donner une valeur de type τ(v) pour chaque v (donc une fonction, mais dont le type de la cible dépend de la source). Et en même temps, il ressemble à U⇒Q si Q se trouve ne pas dépendre de v, de la même manière que ∏_v:U τ, lorsque τ ne dépend pas de v, donne quelque chose comme τ^U (enfin, U→τ avec la notation ‘→’ pour les types fonctions).
• ∃(v:U).Q(v) est une sorte de « disjonction en famille » ⋁_v:U Q(v) qui doit donc correspondre par Curry-Howard à un type « somme en famille » ∑_v:U τ(v) par Curry-Howard, c'est-à-dire que τ(v) est un type qui dépend de v (un type dépendant) et ∑_v:U τ(v) est le type correspondant à se donner un v de type U et une valeur de type τ(v) pour ce v (donc une sorte de couple, mais dont le type de la seconde composante dépend de la première composante). En même temps, il ressemble à U∧Q si Q se trouve ne pas dépendre de v, de la même manière que ∑_v:U τ, lorsque τ ne dépend pas de v, donne quelque chose comme U×τ.

Notamment, le fait d'utiliser la même notation λ(v:…).… pour l'introduction du ‘⇒’ (où v est alors une hypothèse) et pour l'introduction du ‘∀’ (où v est alors une variable qu'on veut généraliser) est sensé, et en même temps ne causera pas de confusion. De même pour l'utilisation de la même notation ⟨t,…⟩ pour l'introduction du ‘∧’ (où t est alors une preuve de la première partie de la conjonction) et pour l'introduction du ‘∃’ (où t est alors un témoin de l'existence).

Le problème avec mes règles c'est surtout qu'elles sont excessivement obscures sur ce qui est U et comment on produit des choses comme t:U (j'utilise le ‘⊢’ pour dire démontre ou type un terme) : est-ce qu'il y a tout un système de types là-dessous ? Si oui, quelles sont les opérations à son sujet ? Lié à ça, il y a le problème que je ne suis pas du tout super clair si j'autorise à écrire quelque chose comme (match z with ⟨v,w⟩↦v) lorsque Γ ⊢ z : ∃(v:U).P(v), qui serait une façon d'extraire la valeur dont le ‘∃’ prétend affirmer l'existence.

La logique du premier ordre

Le cas le plus simple, même s'il n'est pas très satisfaisant du point de vue de la théorie des types, c'est celui de la logique du premier ordre, qui, si on en croit le Dogme Orthodoxe, est la logique usuelle des mathématiques (la théorie des ensembles ZFC se place dans le cadre de la logique du premier ordre). La logique du premier ordre est fondée sur l'idée qu'il y a un seul type sur lequel on peut quantifier : les habitants de ce type s'appellent les individus, son type s'appelle l'univers ou le domaine des individus, et on ne peut faire aucune construction sur ce type des individus. Quand on va appliquer Curry-Howard, les propositions vont devenir des types (comme ci-dessus dans le cas propositionnel où il n'y avait pas d'individus du tout, uniquement des propositions), mais ces types sont d'une sorte complètement séparée du type des individus.

En un peu plus précis, pour la logique du premier ordre :

• Il y a un seul type U sur lequel on puisse quantifier, il est complètement spécial, c'est l'univers des individus, et on ne peut appliquer aucune opération de type sur lui (on ne peut même pas fabriquer U×U ni U+U, quelle que soit la notation) ni rien de la sorte. Du coup, on peut se dispenser d'écrire ∀(v:U) ou ∃(v:U) dans les quantificateurs et simplement mettre ∀v ou ∃v. Les variables de type U sont appelées les variables d'individus, elles sont complètement séparées des variables propositionnelles/relationnelles mentionnées au point suivant.

• Les propositions (qui vont devenir des types propositionnels via Curry-Howard) sont obtenues par application des connecteurs logiques et quantificateurs à partir de propositions de la forme A^(r)(x₁,…,x_r) (qu'il serait sans doute plus logique de noter A^(r)x₁⋯x_r en fait, mais bon, c'est assez peu lisible), où A^(r) est une variable relationnelle d'arité r (il y en a un stock infini pour chaque r≥0, et en pratique on peut se dispenser d'écrire le r) : ici, les x_i sont des (termes d')individus.

  Le cas r=0 (relations nullaires) correspond aux variables propositionnelles du calcul propositionnel qu'on a déjà rencontrées, i.e., des propositions non spécifiées, et le cas r>0 correspond à des relations non spécifiées entre les individus. En tout cas, on ne peut pas quantifier sur ces variables relationnelles, juste les appliquer à un nombre d'individus exactement égal à leur arité. (C'est-à-dire qu'en pratique elles ont type U^r→Prop ou quelque chose comme ça, mais on n'a même pas le droit d'écrire ce type.)

• Dans la version la plus simple, les seuls termes d'individus sont les variables d'individus elles-mêmes. Mais on peut aussi éventuellement autoriser des variables fonctionnelles entre les individus (fonctions de différentes arités, et sur lesquelles on ne peut pas quantifier non plus), qui ont en pratique le type U^r→U (qu'on n'a pas le droit d'écrire), et les termes d'individus sont alors ceux obtenus en composant de la façon évidente ces fonctions d'arités diverses sur des variables d'individus.

  (Notons que tout ça n'est pas forcément anodin : la seule présence d'une fonction c d'arité zéro (= une constante d'individu) permet de démontrer ∃(v:U).⊤ (le domaine des individus est habité, avec pour preuve ⟨c,•⟩), ce qui n'était pas évident ni forcément souhaitable.)

• En tout cas, pour être bien clair, on n'autorise pas des écritures comme (match z with ⟨v,w⟩↦v) sur un z de type ∃(v:U).P(v) : les termes d'individus ne doivent être fabriqués qu'à partir des variables d'individus et éventuellement des fonctions signalées au point précédent, mais pas avec les constructions que j'ai introduites pour les démonstrations.

Je ne suis absolument pas certain de ne pas avoir merdé mes règles et oublié des petits caractères quelque part disant que la variable machin doit être libre, ou pas libre, ou apparaître, ou pas apparaître, ou qu'on n'a pas le droit de faire ceci ou cela, mais globalement ce sont censé être les règles usuelles de la logique du premier ordre utilisée dans l'essentiel des maths usuelles, sauf qu'elle est intuitionniste (et présentée avec une petite saveur théorie des types, et en évitant de supposer que U est habité, chose sur quoi les logiciens du premier ordre ne sont pas toujours d'accord).

À titre d'exemple de théorèmes et de preuves en (pure) logique du premier ordre (et en omettant les :U qui ne sont pas très utiles vu qu'il n'y a qu'un domaine d'individus dans mon histoire) :

• Une démonstration de ∀v.∃w.⊤ est donnée par le λ-terme suivant : λv.⟨v,•⟩ (rappelons que λv est mis ici pour λ(v:U) de meme que ∀v est mis ici pour ∀(v:U)). Noter que ∃w.⊤ ne devrait pas être démontrable en contexte vide (si je ne me suis pas planté dans mes règles ; par contre, dès que Γ a un u:U dedans, alors ⟨u,•⟩ démontre ∃u.⊤).
• Une démonstration de (∃v.⊤) ⇒ (∀v.A(v)) ⇒ (∃v.A(v)) est donnée par le λ-terme suivant : λ(h:∃v.⊤). λ(f:∀v.A(v)). (match h with ⟨v,w⟩ ↦ ⟨v, fv⟩). On peut préférer affirmer (∃v.⊤) ∧ (∀v.A(v)) ⇒ (∃v.A(v)) (mais alors la preuve est λ(p : ∃v.⊤ ∧ ∀v.A(v)). (match π₁p with ⟨v,w⟩ ↦ ⟨v, π₂pv⟩), ce qui est quand même moins lisible). En revanche, (∀v.A(v)) ⇒ (∃v.A(v)) ne devrait pas être démontrable (toujours parce que je ne suppose pas que mon domaine d'individus est habité).
• Une démonstration de (∀v.(A(v)⇒C)) ⇒ (∃v.A(v)) ⇒ C est donnée par le λ-terme suivant : λ(f:∀v.(A(v)⇒C)). λ(p:∃v.A(v)). (match p with ⟨v,w⟩ ↦ fvw).
• Réciproquement, une démonstration de ((∃v.A(v)) ⇒ C) ⇒ (∀v.(A(v)⇒C)) est donnée par le λ-terme suivant : λ(g:(∃v.A(v))⇒C). λv. λ(q:A(v)). g⟨v,q⟩.
• Une démonstration de (∃v.(A(v)⇒C)) ⇒ (∀v.A(v)) ⇒ C est donnée par le λ-terme suivant : λ(p:∃v.(A(v)⇒C)). λ(f:∀v.A(v)). (match p with ⟨v,w⟩ ↦ w(fv)).
• Une démonstration de (∃v.∀w.B(v,w)) ⇒ (∀w.∃v.B(v,w)) est donnée par le λ-terme suivant : λ(p : ∃v.∀w.B(v,w)). λw. (match p with ⟨v,z⟩ ↦ ⟨v,zw⟩).

De nouveau, on va pouvoir voir ça comme des programmes, et c'est ça la correspondance de Curry-Howard.

Au niveau typage, la nouveauté c'est qu'on a affaire à des types dépendants. Plus exactement, à la sortie de la moulinette Curry-Howard, on obtient deux sortes différentes d'objets : les individus, de type U, qui sont complètement à part, et les valeurs des types propositionnels (i.e., les types que Curry-Howard a introduits pour correspondre aux propositions logiques). Les types propositionnels peuvent dépendre d'individus : ce sont des types dépendants ; par exemple, une relation unaire A(x) (= prédicat sur les individus) devient par Curry-Howard un type distinct pour chaque valeur de x (et qui est opaque de toute manière) ; les quantificateurs sont des façons d'opérer « en famille » sur ces types dépendants, et se comprennent, ainsi que je l'ai expliqué plus haut, comme des produits et des sommes « en famille » (mais toujours indicés par le même domaine U des individus puisque, en logique du premier ordre, on n'a que ça).

En revanche, au niveau du comportement du programme, je n'ai pas à changer mes explications : il n'y a que le typage qui est plus compliqué par le fait qu'il y a des types dépendants, mais le comportement du programme est la généralisation évidente de ce qui précède.

Par exemple, mon dernier exemple, vu en tant que programme, prend un p dont le type est ∑_v∏_wB(v,w) (pour B un type dépendant à deux paramètres), c'est-à-dire la donnée d'un v et d'une fonction prenant un w et renvoyant une valeur de type B(v,w), et il fabrique la fonction de w qui extrait les deux deux données de p comme v et z (le z étant la fonction, désolé si mes notations sont épouvantables) et renvoie ⟨v,zw⟩ dans ∑_vB(v,w), donc finalement une valeur dans ∏_w∑_vB(v,w) qui est simplement obtenue en « constanciant » v sur le p de départ. Le typage est éventuellement un peu subtil, mais la fonction elle-même n'a rien de compliqué, d'ailleurs si demande à OCaml (c'est-à-dire à l'algorithme de Hindley-Milner) de typer λp. λw. (match p with ⟨v,z⟩ ↦ ⟨v,zw⟩), il me renvoie (je change juste les notations) U×(U′→B) → U′→(U→B) : OCaml n'a pas de types dépendants[#4] donc il ne peut pas faire mieux que ça au niveau typage, mais le programme lui-même est parfaitement représentable en OCaml (ou, comme je le disais plus haut, en Scheme qui n'a pas du tout de types statiques).

[#4] Enfin, méfions-nous : le bout que je connais de OCaml n'a pas de types dépendants. Le système de typage de OCaml a l'air d'être l'accumulation de N thèses de N doctorants à l'INRIA qui ont chacun ajouté son lot de complications, et à chaque fois que je dis que OCaml n'a pas quelque chose, quelqu'un m'envoie un mail pour me dire que si, et il vaut donc mieux que j'évite ce genre d'affirmations. En tout état de cause, il y a (avait ?) un langage appelé Dependent ML qui avait ça.

Quelques mots sur l'arithmétique du premier ordre

Bon, dans la section précédente il s'agissait de logique du premier ordre pure, c'est-à-dire qu'il n'y a aucun axiome, juste des variables relationnelles de différentes arités, et à moins d'être adepte du logicisme le plus strict, ce n'est pas très rigolo de ne regarder que des affirmations comme ((∃v.A(v)) ⇒ C) ⇒ (∀v.(A(v)⇒C)) qui portent sur des propriétés non spécifiées d'un domaine non spécifié d'individus non spécifiées.

Peut-être qu'il est plus satisfaisant de transformer en programme une démonstration dans une théorie comme, disons, l'arithmétique de Heyting (qui est essentiellement la version intuitionniste de l'arithmétique de Peano : mêmes axiomes mais en logique intuitionniste). Essayons donc de dire un mot sur l'interprétation de Curry-Howard pour les démonstrations dans l'arithmétique de Heyting du premier ordre.

La difficulté, d'abord, est qu'il faut donner un sens aux relations, fonctions et constantes du langage, et aux axiomes de la théorie. S'agissant de l'arithmétique, on va évidemment comprendre le domaine des individus (ce que j'avais noté U) comme les entiers naturels, et les fonctions et constantes du langage, c'est-à-dire, 0, le successeur, l'addition et la multiplication, se comprennent sans difficulté comme elles-mêmes. Mais on rencontre un petit problème pour savoir comment comprendre l'égalité : comme m=n est, côté logique, une proposition de deux variables libres, côté programme c'est un type dépendant de deux variables, qu'il faut imaginer comme le type des témoignages d'égalité de m et de n : le type en question doit donc être vide si m≠n, et il n'y a pas spécialement de raison (au moins pour quelque chose d'aussi simple que les entiers naturels) de vouloir qu'il ait plus qu'une seule valeur[#5] ; donc on peut y penser comme un truc spécial qui atteste que m=n mais, si on est plus pragmatique, simplement comme la valeur commune à ces deux entiers.

[#5] Comprendre « ce que c'est » que l'égalité, et ce qu'elle doit vérifier, est une des questions les plus épineuses de la théorie des types (remarquez par exemple que j'ai très soigneusement évité de dire quoi que ce soit sur la question de si ou quand deux preuves sont égales). Si vous voulez être certain de ne plus rien comprendre à l'égalité, je conseille de lire le livre Homotopy Type Theory. Si vous voulez espérer y comprendre quand même quelque chose, il peut être intéressant de regarder par exemple les chapitres introductifs de deux thèses soutenues récemment : Extending type theory with syntactic models de Simon Boulier et Computing with Extensionality Principles in Type Theory de Loïc Pujet. Mais à part cette brève excursion dans le domaine de l'arithmétique, je vais m'abstenir de parler d'égalité parce que je n'y comprends rien (surtout depuis que j'ai eu le malheur de jeter un œil à la théorie homotopique des types).

Ensuite, il faut donner un sens aux axiomes de l'arithmétique. Entendons-nous bien : chaque axiome est une proposition, donc Curry-Howard doit le transformer en un type ; mais il y aussi un démonstration de cette proposition dans l'arithmétique, qui consiste justement à dire c'est un axiome : si on veut transformer les démonstrations en programmes, il va falloir transformer les axiomes en fonctions de base. À la limite, ces fonctions peuvent faire n'importe quoi (quand on a une démonstration dans une théorie les types correspondant aux axiomes de la théorie définissent ce qu'en langage informatique on appelle une API, et les programmes sont construits sur cette API en appelant les fonctions en question, peu importe ce qu'elles font) ; mais en l'occurrence, s'agissant de l'arithmétique c'est très clair ce qu'elles doivent faire.

Je reprends l'énumération des axiomes que j'avais faite dans cette section de ce billet, en commençant par ceux de l'égalité :

• ∀m.(m=m) : ceci est implémenté par une fonction prenant m et renvoyant un témoignage que m=m (si on identifie un tel témoignage à m lui-même, c'est juste la fonction identité, mais dont la cible a une type plus particulier).
• ∀m.∀n.((m=n)⇒(n=m)) : on prend deux entiers m,n en entrée et un témoignage de leur égalité m=n, et on renvoie le témoignage symétrique de n=m.
• ∀m.∀n.((m=n)⇒(P(m)⇒P(n))) (où ici P est un type dépendant d'arité 1 quelconque : on n'a pas le droit de quantifier dessus puisqu'on parle de logique du premier ordre, donc en principe il y a une infinité d'axiomes, un pour chaque type possible ; mais peu importe pour ce que je veux dire) : ici on prend deux entiers m et n et un témoignage de leur égalité, et une valeur de type P(m), et on renvoie la même valeur mais maintenant vue dans le type P(n) (le fait que ce soit possible est justement une façon de constater que m et n sont bien égaux ; d'ailleurs, si on ne s'était pas limité au premier ordre on pourrait prendre ça comme définition de l'égalité, ou égalité de Leibniz).
• ∀n.¬(Sn=0) : cette fonction ne fait rien, elle prend n en entrée et un témoignage du fait que le successeur Sn de n est égal à 0 et… ne fait rien, parce qu'un tel témoignage n'existe pas (cette fonction est donc une pure promesse).
• ∀p.∀q.((Sp=Sq)⇒(p=q)) : cette fonction prend en entrée deux entiers p,q et un témoignage de l'égalité de leurs successeurs Sp,Sq, et renvoie un témoignage de l'égalité de p,q eux-mêmes (au niveau opérationnel, ce n'est toujours pas bien passionnant : on n'est même pas en train de soustraire 1 aux entiers, puisque les valeurs p,q ont déjà été fournies en entrée).
• (P(0) ∧ ∀n.(P(n)⇒P(Sn))) ⇒ ∀n.P(n) : voilà enfin une fonction qui fait quelque chose d'intéressant ! Il s'agit de la fonction itérateur qui prend en entrée le couple formé d'une valeur initiale c et une fonction f, et renvoie la suite définie par récurrence, c'est-à-dire la fonction qui à 0 associe c, à 1 associe f 0 c, à 2 associe f 1 (f 0 c), etc. En OCaml on pourrait la coder comme let iter = fun (c, f) -> let rec u = fun n -> if n==0 then c else f (n-1) (u (n-1)) in u sauf que ceci a pour type A∧(ℕ⇒A⇒A)⇒ℕ⇒A (en notation OCaml 'a * (int -> 'a -> 'a) -> int -> 'a) alors qu'on a affaire à une version plus précisément typée dans laquelle chaque valeur de la suite a un type P(n) potentiellement différent au lieu d'un seul et même A tout du long.
• ∀m.(m+0=m), ∀m.∀n.(m+Sn=S(m+n)), ∀m.(m×0=0), ∀m.∀n.(m×Sn=(m×n)+m), ∀m.(m↑0=1), ∀m.∀n.(m↑Sn=(m↑n)×m) : aucune de ces fonctions ne fait rien d'intéressant, elles se contentent de manipuler des témoignages d'égalité.

Tout ceci étant fait, que font les programmes que Curry-Howard associe à une démonstration arithmétique (en arithmétique de Heyting) ? À vrai dire, ce n'est pas très surprenant : en gros ce sont des programmes qui calculent ce dont le théorème affirme l'existence. C'est peut-être décevant si on s'attendait à découvrir que la preuve du théorème de Fermat allait correspondre à un jeu de Tetris… non, c'est un programme qui ne fait rien parce que le théorème est dans le fragment négatif de l'arithmétique, donc le programme attend un contre-exemple au théorème de Fermat et renvoie quelque chose d'impossible, ou fait exploser l'Univers.

Mais c'était, en fait, un peu tout le but de faire des maths « constructives » au sens de ne pas utiliser le tiers exclu : qu'elles soient effectivement « constructives » au sens de construire les objets dont elles affirment l'existence. Par exemple, la preuve d'Euclide de l'existence d'une infinité de nombres premiers (convenablement réécrite dans l'arithmétique de Heyting après vérification du fait qu'elle est bien constructive) devrait calculer quelque chose comme la suite d'Euclide-Mullin. De façon plus précise/technique, ce que fait la conversion de Curry-Howard, pour l'arithmétique de Heyting du premier ordre, c'est transformer une preuve d'un énoncé arithmétique φ en un réalisateur de φ au sens que j'avais défini ici.

Addendum 1 : quelques mots sur ‘∃’ et les types sommes

Je continue donc ce billet en parlant un peu du problème du ‘∃’ en logique et pourquoi il n'est pas tout à fait le même que le type somme (sauf si Martin-Löf vous surveille) ; et d'ailleurs même pour le ‘∨’. Comme je crois que ce problème ne se pose pas pour la logique du premier ordre[#7], mon explication ne sera pas pour le premier ordre, mais de toute façon je vais être si approximatif dans ce que je vais dire pour que ce ne soit pas très important. Encore une fois, je vais être vague, mais je trouve que tout ceci est incroyablement mal expliqué partout et j'ai mis un temps dingue à comprendre les quelques miettes que j'ai comprises, donc ça vaut la peine que je les écrive explicitement.

[#7] Enfin, je croyais, mais à la lecture de la (non-)réponse qu'Andrej Bauer m'a fait à cette question, je ne sais plus quoi croire (son contre-exemple est du premier ordre… sauf qu'il utilise l'égalité, mais je ne sais pas si c'est pertinent vu que comme je l'ai dit plus haut je ne comprends rien à l'égalité en théorie des types).

Avec les mains, le problème est le suivant : une démonstration d'existence, disons de ∃(v:U).Q(v) affirme juste qu'un objet v existe, elle en produit même bien un si on est dans un système constructif, mais elle n'en choisit pas un (l'objet construit peut dépendre de choses sans importance comme la manière dont les données ont été présentées) ; ou plutôt, la démonstration renferme un v mais on ne doit pas pouvoir extraire ce v pour faire autre chose qu'une démonstration. Un type somme ∑_v:U τ(v), en revanche, il enregistre indiscutablement la valeur de v, pas juste un témoignage de son existence, et on peut librement utiliser ce v. De même, une démonstration de Q₁∨Q₂ doit démontrer soit Q₁ soit Q₂, mais le choix, la distinction de Q₁ ou de Q₂, ne doit pas pouvoir être extrait dans autre chose qu'une démonstration : à partir d'une hypothèse Q₁∨Q₂ on peut produire une démonstration en distinguant les deux cas, mais on ne peut pas produire une valeur en distinguant les deux cas, tout simplement parce que ces cas peuvent se recouper ! Tandis que dans un type somme τ₁+τ₂, on sait à tout moment de quel côté de la somme on est.

Bref, l'idée est qu'on a deux « mondes » : un monde logique (celui des preuves) et un monde informatif (ou « informatique », si on veut : celui des valeurs), et que le monde logique a le droit (mais pas l'obligation !) de perdre les témoins d'existence avec lesquels on a construit les preuves, donc ces témoins peuvent seulement servir à fabriquer des démonstrations mais pas passer dans le monde informatif. L'information peut passer du côté informatif vers le côté logique mais pas dans le sens inverse.

Pour donner l'exemple le plus simple possible, d'une valeur v de type U (monde informatif) on peut tirer une démonstration de ∃(v:U).⊤ (le type U est habité), mais cette démonstration a le droit de perdre l'information de v donc on ne peut pas aller dans l'autre sens et extraire d'une preuve de ∃(v:U).⊤ une valeur v de type U.

Sur les règles du jeu, concrètement, ça va vouloir dire qu'on a le droit d'appliquer les opérations de déconstruction des disjonctions (ce que j'ai noté match), lorsqu'on déconstruit une disjonction, uniquement pour construire une démonstration, et pas pour construire un objet.

Maintenant, Curry-Howard fonctionne précisément en disant qu'on va tout mettre dans le même monde (prendre tout ce qui était purement logique et le rendre informatif) : les propositions logiques deviennent des types. Du coup, une démonstration logique va bien donner un programme valable (puisque tout devient un seul monde, les contraintes sur le non passage d'information du monde logique vers le monde informatif deviennent caduques et toute démonstration correspond à un programme valable), mais dans l'autre sens ça ne marche plus forcément : il y a des programmes correctement typés qui ne respectent pas cette règle de séparation des mondes.

Voici un exemple très simple : considérons la proposition (écrite avec deux types U et V et en notant U⇒V le type des fonctions de l'un vers l'autre ; donc je ne suis pas en premier ordre, mais je n'en suis pas très loin non plus) :

(∀(u:U). ∃(v:V). P(u,v)) ⇒ (∃(f:U⇒V). ∀(u:U). P(u,f(u)))

Cet énoncé s'appelle l'axiome du choix (c'est l'analogue en théorie des types de l'axiome du choix de Zermelo en théorie des ensembles), et on ne veut probablement pas l'admettre en logique. Mais si on comprend ‘∀’ et ‘∃’ comme des types produits et sommes en famille comme le demande Curry-Howard, et que je change les notations pour le refléter, on est juste en train de chercher une fonction de type

(∏_u:U ∑_v:V P(u,v)) → (∑_f:U→V ∏_u:U P(u,f(u)))

et là c'est non seulement possible, mais c'est même « canonique » : avec mes notations, on peut écrire

λ(h:⋯). ⟨λ(u:U).(match hu with ⟨v,z⟩ ↦ v), λ(u:U).(match hu with ⟨v,z⟩ ↦ z)⟩

(où les ‘⋯’ omettent le type de la partie de gauche, soit ∀(u:U). ∃(v:V). P(u,v) en notation logique ou bien ∏_u:U ∑_v:V P(u,v) en notation typage). En tant que programme, ceci est parfaitement sensé, et conforme au type de la ligne précédente (d'ailleurs je peux l'écrire en OCaml : fun h -> ((fun u -> match h u with (v,z) -> v), (fun u -> match h u with (v,z) -> z)) même si OCaml n'a pas les types dépendants donc le type devient juste (U⇒V∧W)⇒(U⇒V)∧(U⇒W)). Mais ceci n'est pas une preuve légitime de l'axiome du choix.

Le problème est qu'on a essayé d'extraire des informations du monde logique (où vit P) vers le monde informatif (où vivent U,V) en écrivant match hu with ⟨v,z⟩ ↦ v : plus précisément, la règle serait que le match (que ce soit pour déconstruire un ‘∃’ ou un ‘∨’) appliqué à une démonstration (quelque chose qui vit côté logique) ne doit finalement produire qu'une démonstration. Si P était côté informatif, comme je viens de le dire, mon terme est légitime et il a le type que Curry-Howard attribue à l'axiome du choix[#8]. Mais avec P côté logique et U,V côté informatif, mon terme qui prétend démontrer l'axiome du choix, est tabou.

[#8] Et inversement, si tout était côté logique, i.e., si U et V étaient des propositions, mon terme serait légitime aussi, même si je ne comprends pas bien ce que ça voudrait dire que faire dépendre une proposition d'une démonstration, donc je ne sais pas comprendre ça autrement que comme une preuve de (U⇒V∧W)⇒(U⇒V)∧(U⇒W).

Cette histoire de séparation du monde logique et du monde informatif est ce que pratique Coq : dans le monde logique, les « types » sont des propositions, et leur domaine est appelé Prop, tandis que dans le monde informatif, les types sont des types, et leur domaine est appelé Type (ou éventuellement Set) sauf qu'en fait pour éviter un paradoxe (« paradoxe de Girard ») c'est une tour infinie de types que Coq cache derrière un seul nom, je vais en dire un mot dans l'addendum suivant. Coq traite les deux mondes de façon extrêmement parallèle, mais ils sont distincts, et l'interdiction de passer de l'information du monde logique vers le monde informatif est présentée sous la forme Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set because proofs can be eliminated only to build proofs (avec une sous-exception dans le cas d'un singleton où c'est quand même autorisé[#9]).

[#9] Je ne comprends d'ailleurs pas pourquoi cette sous-exception autorisant l'élimination des singletons ne permet pas de démontrer l'axiome du choix unique dans Coq. Purée, que tout ceci est embrouillé et mal expliqué partout !

Une solution que je crois analogue (ou en tout cas, dont je ne comprends pas les différences s'il y en a) apparaît sous forme de troncature propositionnelle en théorie homotopique des types : laissant de côté le côté « homotopique » que je ne comprends pas du tout, l'opération de troncature propositionnelle doit revenir, si je comprends, à transformer un type U en la proposition [U] := ∃(u:U).⊤ qui dit que U est habité, sauf que le choix est plutôt de définir, dans l'autre sens, ∃(u:U).P(u) comme [∑_u:U P(u)] ou quelque chose du genre. Aussi, à la différence de Coq qui est agnostique sur la question de la proof irrelevance (est-ce que toutes les preuves d'une même proposition sont égales ?), la troncature doit servir justement à imposer ça.

Les théories des types à la Martin-Löf, en revanche (et sur lesquelles sont basées Agda), n'ont pas de vrai ‘∃’, juste un ‘Σ’ des types sommes : pour cette raison, elles ne permettent jamais de tronquer ni de perdre l'information, et elles croient à Curry-Howard jusqu'au bout, et notamment, elles démontrent l'axiome du choix (avec la démonstration que je viens de donner). Mais évidemment cela a des inconvénients : en gros ça empêche d'utiliser les constructions usuelles des mathématiques que sont les ensembles quotients ou les images de fonctions (ce que ces théories appellent types sont des objets pour lesquels l'axiome du choix vaut (et que dans un autre contexte on appellerait objets projectifs). On doit donc « simuler » les choses comme les quotients avec des constructions appelées « setoïdes » (un setoïde est un type et une relation d'équivalence sur ce type, et puisqu'on ne peut pas quotienter par ladite relation, on doit se la trimbaler partout). Voir par exemple cette réponse d'Andrej Bauer sur l'importance d'avoir à la fois un ‘∃’ et un ‘Σ’.

Addendum 2 : quelques mots sur l'imprédicativité

Je termine ce billet en continuant mes remarques d'ordre « les trucs super mal expliqués partout et ça m'énerve donc je braindumpe un peu le peu que j'ai compris » avec une autre question indépendante (je crois ?) de la précédente : l'imprédicativité.

L'imprédicativité, en gros, c'est de faire une définition en considérant tout un tas d'objets y compris celui qu'on est en train de définir. Donc on peut considérer ça comme une sorte de définition circulaire.

En l'occurrence, c'est la forme suivante d'imprédicativité : quantifier sur l'ensemble des valeurs du type dont fait partie la formule quantifiée. I.e., fabriquer ∀(A:*).(⋯), où ‘*’ est un certain type, ce machin étant lui-même de type ‘*’.

Si on pense à la logique, c'est-à-dire que ‘*’ est le type des propositions logiques, ce n'est pas spécialement problématique ni surprenant de faire des propositions qui ont le droit de quantifier sur les propositions : c'est l'idée de la logique du second ordre[#10], qui est intéressante déjà au niveau propositionnel c'est-à-dire si on autorise juste de quantifier sur des propositions. Évidemment, en calcul propositionnel « basique » on peut considérer qu'on a déjà une quantification universelle implicite sur toutes les variables propositionnelles (puisque ce sont, justement, des variables sur lesquelles on n'a pas d'hypothèse) : quand on écrit A∧B⇒B∧A en fait on peut considérer que ça veut dire ∀(A:*).∀(B:*).A∧B⇒B∧A (où ‘*’ est le type des propositions), juste on ne peut pas l'écrire comme ça parce que le simple calcul propositionnel n'a pas de quantificateurs du tout. Le calcul propositionnel du second ordre autorise cette quantification explicite, et bien sûr elle n'a pas besoin de se trouver en tête de formule, on peut parfaitement considérer une formule comme, disons, ¬∀(A:*).(¬¬A⇒A). Tout ceci est imprédicatif, parce qu'on quantifie sur les propositions pour fabriquer une proposition. Mais ce n'est pas spécialement mystérieux pour autant : si on pense que les propositions sont des pures valeurs de vérité, alors ‘∀’ est juste un inf sur ces valeurs de vérité et ‘∃’ est un sup, et on a parfaitement le droit de prendre l'inf ou le sup d'une fonction d'un ensemble ordonné (suffisamment complet) vers lui-même, c'est imprédicatif parce que la borne inf ou sup qu'on considère est dans l'ensemble sur lequel on prend l'inf ou le sup, mais ce n'est pas logiquement problématique.

[#10] La terminologie second ordre et premier ordre est assez merdique, parce que le calcul propositionnel du second ordre ne généralise pas la logique [i.e., le calcul des prédicats] du premier ordre : dans le calcul propositionnel du second ordre, on peut quantifier sur des propositions, dans la logique du premier ordre on peut quantifier sur des individus, et ces choses sont en fait essentiellement orthogonales. C'est juste que traditionnellement on ne s'est intéressé à la quantification sur les propriétés que quand ces propriétés portaient déjà sur un domaine d'individus, donc on avait déjà l'autre sorte de quantification.

Il n'est pas difficile d'adapter les règles et notations que j'ai proposées plus haut pour le calcul propositionnel du second ordre : au lieu de quantifier sur les individus on quantifie sur les propositions, on a un type des propositions (je vais le noter ‘*’) qui est tout aussi « intangible » que le type des individus dans la logique du premier ordre, et les termes qu'on peut fabriquer dans ce type ‘*’ sont justement ceux qu'on peut fabriquer avec les connecteurs logiques, quantificateurs compris ; mais sinon, rien de particulier à dire : les règles d'introduction et d'élimination de ‘∀’ et ‘∃’ (et donc les notations que j'ai introduites pour elles) ne renferment pas de surprise particulière. (Enfin, je crois.)

À titre d'exemple (et toujours en notant ‘*’ le type des propositions), on peut affirmer que ∀(A:*). A ⇔ (∀(C:*).(C⇒A)), que je précise qu'il faut parenthéser comme ∀(A:*). (A ⇔ (∀(C:*).(C⇒A))). La preuve de ∀(A:*). A ⇒ (∀(C:*).(C⇒A)) est donnée par le λ-terme λ(A:*). λ(x:A). λ(C:*). λ(z:C). x : ça se lit vraiment comme on l'imagine : soit A une proposition quelconque, supposons que A soit vraie et appelons x cette hypothèse, soit C une proposition quelconque, supposons que C soit raie et appelons z cette hypothèse, alors A est vraie en vertu de l'hypothèse z. Quant à la la preuve de la réciproque ∀(A:*). (∀(C:*).(C⇒A)) ⇒ A (de nouveau, je souligne que c'est à parenthéser comme ∀(A:*). ((∀(C:*).(C⇒A)) ⇒ A)), elle est donnée par le λ-terme λ(A:*). λ(h:∀(C:*).(C ⇒ A)). h⊤• (je prends mon hypothèse h qui affirme ∀(C:*).(C⇒A), et je l'applique avec pour C la proposition trivialement vraie ⊤ et la preuve • de cette proposition).

Pour donner un exemple un peu moins trivial, montrons que ∀(A:*). A ⇔ (∀(C:*).((A⇒C)⇒C)). La preuve dans le sens ∀(A:*). A ⇒ (∀(C:*).((A⇒C)⇒C)) est facile :

λ(A:*). λ(x:A). λ(C:*). λ(k:A⇒C). kx

et dans l'autre sens, une preuve de ∀(A:*). (∀(C:*).((A⇒C)⇒C)) ⇒ A est donnée par :

λ(A:*). λ(h:∀(C:*).((A⇒C)⇒C)). hA(λ(x:A).x)

qu'il faut lire quelque chose comme soit A une proposition quelconque et soit h l'hypothèse qui affirme ∀(C:*).((A⇒C)⇒C) : appliquons h avec pour C la proposition A, ce qui nous donne (A⇒A)⇒A ; mais on a une preuve évidente de A⇒A (donnée par le terme λ(x:A).x), donc par modus ponens on en tire A comme annoncé.

Ça peut ressembler à un gadget, mais cette imprédicativité est utile. Par exemple, je peux facilement adapter les termes ci-dessus pour montrer que

∀(A:*). ∀(B:*). A∧B ⇔ (∀(C:*).((A⇒B⇒C)⇒C))

par les preuves (dans un sens et dans l'autre) :

λ(A:*). λ(B:*). λ(z:A∧B). λ(C:*). λ(k:A⇒B⇒C). k(π₁z)(π₂z)

λ(A:*). λ(B:*). λ(h:∀(C:*).((A⇒B⇒C)⇒C)). h(A∧B)(λ(x:A).λ(y:B).⟨x,y⟩)

et que

∀(A:*). ∀(B:*). A∨B ⇔ (∀(C:*).((A⇒C)⇒(B⇒C)⇒C))

par les preuves (dans un sens et dans l'autre) :

λ(A:*). λ(B:*). λ(z:A∨B). λ(C:*). λ(k:A⇒C). λ(ℓ:B⇒C). (match z with ι₁x↦kx, ι₂y↦ℓy)

λ(A:*). λ(B:*). λ(h:∀(C:*).((A⇒C)⇒(B⇒C)⇒C)). h(A∨B)(λ(x:A).ι₁^(A,B)x)(λ(y:B).ι₂^(A,B)y)

— et l'intérêt de ces exemples est que ça peut servir à définir les connecteurs ‘∧’ et ‘∨’ par la partie droite de ces équivalences : dès lors que j'ai le droit de quantifier sur les propositions, je peux définir A∧B comme raccourci de langage pour ∀(C:*).((A⇒B⇒C)⇒C) et A∨B comme raccourci de langage pour ∀(C:*).((A⇒C)⇒(B⇒C)⇒C). (Bon, il faut vérifier que ces définitions obéissent bien aux mêmes règles que ‘∧’ et ‘∨’, ce que mes preuves ne font pas vraiment, après tout, elles dépendent du fait que ‘∧’ et ‘∨’ existent déjà, mais en fait c'est bien le cas.)

Je peux même définir, de même, ∃(D:*).ψ(D) comme abréviation de ∀(C:*).(∀(D:*).ψ(D)⇒C)⇒C) pour toute formule logique ψ faisant intervenir une variable D sur laquelle on veut quantifier (avec les quantifications limitées que j'ai permises, je n'ai pas le droit d'écrire le type de ce ψ, donc ce n'est pas un citoyen du langage et je ne peux certainement pas quantifier sur ψ, mais peu importe, je peux convenir de ce raccourci pour tout ψ, et l'équivalence est facile à montrer sur chaque instance selon le même schéma de démonstration). Donc en fait on peut ne garder comme seules constructions que le ‘∀’ et l'implication (on peut se passer du ‘⊥’ en le voyant comme un raccourci de ∀(C:*).C et du ‘⊤’ en le voyant comme un raccourci de ∀(C:*).(C⇒C)).

(Il ne faut pas s'imaginer d'après ces simples exemples que toute formule du calcul propositionnel du second ordre se ramène à une formule du calcul propositionnel basique. Par exemple, en réponse à cette question on m'a expliqué que la formule ∀(C:*).(C∨(C⇒A)) — qu'on peut elle-même réécrire comme on vient de l'expliquer si on veut faire disparaître le ‘∨’ — n'est pas démontrablement équivalente à une formule propositionnelle sans quantificateurs dans la variable A.)

Ce que j'ai plus-ou-moins décrit là est un système appelé système F par Girard et λ2 par Barendregt. Du moins, c'est la vision « système logique » de ce machin. (Aussi, ce que j'ai noté λ(X:*), celui qui sert à montrer des ‘∀’, est généralement noté ΛX quand on s'intéresse spécifiquement au système F, par exemple dans l'article Wikipédia à son sujet.)

Mais justement, que dit Curry-Howard de tout ça ? (Parce que c'est quand même censé être le sujet de ce billet.) J'ai parlé ci-dessus du côté logique, mais quel est le côté programmes ?

Si on réinterprète les propositions A,B,C… comme des types (et ‘*’ comme le « domaine des types ») en suivant le principe général de Curry-Howard, on obtient un langage avec polymorphisme explicite, c'est-à-dire que par exemple une fonction comme l'« identité polymorphe », à savoir

λ(A:*). λ(x:A). x

est de type ∀(A:*). (A⇒A), c'est-à-dire qu'elle peut explicitement se décliner en une fonction de type A⇒A pour n'importe quel type A : elle prend comme premier argument un type A, et renvoie l'identité λ(x:A).x de ce type (qui est elle-même de type A⇒A), d'où le type final ∀(A:*). (A⇒A).

Si on y pense comme des programmes, ces arguments-types (ceux introduits par λ(X:*), ou par ΛX si on préfère cette notation-là) peuvent être purement et simplement ignorés lors de l'exécution (à moins qu'on veuille garder une trace des types à l'exécution), ils servent juste à ce que le système de types soit heureux, mais si on pratique l'effacement des types on obtient un programme dont le comportement ne voit pas du tout de types.

Les termes que j'ai donnés plus haut de type ∀(A:*). ∀(B:*). A∧B ⇒ (∀(C:*).((A⇒B⇒C)⇒C)) et ∀(A:*). ∀(B:*). (∀(C:*).((A⇒B⇒C)⇒C)) ⇒ A∧B sont des programmes tout à fait raisonnables et même utiles : ce sont ceux qui convertissent un couple (de type A∧B) en une représentation du couple dans une clôture comme je l'avais évoqué dans ce billet (où ces fonctions étaient en gros appelées fromnative et tonative j'expliquais justement que la seconde ne marchait pas bien à cause de limitations du système de typage dans un langage qui ne sait pas représenter des fonctions prenant en argument un type universellement quantifié). Les termes que j'ai donnés pour ∀(A:*). ∀(B:*). A∨B ⇒ (∀(C:*).((A⇒C)⇒(B⇒C)⇒C)) et ∀(A:*). ∀(B:*). (∀(C:*).((A⇒C)⇒(B⇒C)⇒C)) ⇒ A∨B sont de même des façons de convertir un type somme vers et depuis une représentation sous forme de clôtures. Bref, Curry-Howard produit des programmes tout à fait raisonnables avec ces preuves.

On peut quand même se sentir un peu gêné aux entournures par cette histoire d'imprédicativité : autant si on pense aux trucs de type ‘*’ comme des propositions qui n'ont qu'une valeur de vérité, ce n'est pas particulièrement perturbant de prendre des inf et des sup librement dessus, autant si on imagine que ‘∀’ représente un type produit (ce qui était l'interprétation que je proposais aux quantificateurs), ça commence à avoir l'air suspicieusement paradoxal que, par exemple, l'identité polymorphe vive dans un produit qui est lui-même une composante de ce sur quoi on a pris le produit !

En fait, Girard a montré que l'imprédicativité du système F ne cause pas de paradoxe (le système de typage est sain et garantit la terminaison de tous les programmes). L'imprédicativité peut facilement conduire à des paradoxes (le paradoxe de Girard auquel je faisais allusion plus haut), mais apparemment pas si elle concerne une unique sorte à la base du système de types… ou quelque chose comme ça. En tout cas, le système F échappe au paradoxe. Mais la preuve de Girard est essentiellement syntaxique. Il est sans doute intéressant de regarder à quoi ressemblent les modèles du système F (on me souffle qu'un mot-clé ici est celui d'hyperdoctrine) pour comprendre comment on s'arrange pour avoir quelque chose qui ressemble à un produit qui soit lui-même une composante de ce sur quoi on a pris le produit. J'essaierai de jeter un œil à ça un jour.

Dans Coq, si je comprends bien, Prop est imprédicatif, c'est-à-dire qu'on peut définir des propositions en quantifiant universellement sur les propositions ; Type est prédicatif, c'est-à-dire qu'on ne peut pas définir un type par quantification universelle sur les types (mais Coq va faire semblant en créant des tours d'univers dont il ne montre pas les indices et ne se plaindre que si on a une incohérence : i.e., si on quantifie universellement sur les types, ça crée en fait un truc dans Type_i+1 qui quantifie universellement sur Type_i pour tout i) ; et Set (qui est une sorte de Type₋₁) est prédicatif par défaut mais il y a une option pour le rendre lui aussi imprédicatif (même si du coup ça ne correspond franchement pas à l'intuition d'un ensemble) : cette option n'est pas activée par défaut parce qu'elle contredit une forme du tiers exclu. Dans les théories des types de Martin-Löf, en revanche, à part une version imprédicative initiale qui s'est avérée incohérente, tout est prédicatif (et du coup on ne peut pas définir ‘∃’, qui d'ailleurs n'est pas un ‘∃’ mais un ‘Σ’ comme expliqué dans l'addendum 1, au moyen de ‘∀’=‘Π’).

Remarque : j'ai présenté les deux questions discutées par mes deux addenda (la question du monde logique vs. le monde informatif, aka ‘∃’ vs. ‘Σ’, et la question de l'imprédicativité), comme indépendantes, mais ce n'est notamment pas du tout clair pour moi si elles sont vraiment indépendantes. Est-ce que le fait que Coq et les trucs à la Martin-Löf aient fait des choix différents sur les deux questions est un hasard, ou est-ce qu'il y avait une raison plus profonde ?