Méta : Le présent billet, quoique indépendant, est une sorte de suite de celui-ci où j'exposais quelques points d'informatique théorique que j'ai appris, ou mieux/enfin compris, en enseignant un cours que je crée cette année à Télécom. En fait, j'étais parti pour écrire quelque chose sur un sujet plus spéculatif, mais je me suis dit que pour commencer il fallait que j'explique proprement la correspondance de Curry-Howard, et comme c'est justement une des choses que j'enseigne et que je trouve généralement très mal expliqué, autant en faire aussi une entrée de blog ; puis comme j'étais trop débordé par l'écriture des transparents du cours lui-même, j'ai laissé ça de côté. J'ai de nouveau un petit peu de temps avec les vacances, donc je publie et complète séparément ce bout sur Curry-Howard comme un texte autonome, dans l'espoir de faire ensuite un autre billet sur les questions qui, au-delà de mon enseignement du moment, m'avaient initialement motivé à en parler. Mais comme je tombe dans un trou de lapin dès que je me mets à écrire sur un sujet, j'ai quand même élargi le sujet à des questions connexes.
Table des matières
Introduction
Bref, mon but est d'exposer (avec des prérequis aussi limités que possible) la correspondance de Curry-Howard entre preuves et programmes.
De quoi s'agit-il ? On résume parfois la correspondance de Curry-Howard en disant que, comme un bon acteur capable de prendre des rôles très différents, les preuves mathématiques et les programmes informatiques sont, en fait, fondamentalement la même chose (et d'ailleurs je suis très content de l'illustration ci-contre).
À vrai dire, ce raccourci, qui a le mérite d'être mémorable, est un
peu… raccourci. Ce ne sont pas n'importe quelles preuves et surtout,
ce ne sont pas n'importe quels programmes. Côté preuves, il
s'agit a priori de preuves en logique intuitionniste
(c'est-à-dire sans le tiers exclu ; je vais définir les choses
précisément ci-dessous), et même si on peut étendre Curry-Howard à la
logique classique grâce à la
fonction call/cc
,
la correspondance obtenue n'est peut-être pas aussi satisfaisante.
Côté programmes, il s'agit de programmes écrits dans des langages
fortement typés dans lesquels la terminaison de tout programme est
garanti : donc ce ne sont pas du tout les langages de programmation
habituels, lesquels permettent des boucles infinies et/ou des appels
récursifs illimités[#] ; il n'y
a rien non plus qui corresponde à des effets de bord (modification de
valeurs, entrées-sorties, rien de tel). Parmi les limites de
Curry-Howard, il y a aussi des différences subtiles dans la
signification de la quantification existentielle (‘∃’) en logique par
rapport aux types sommes (‘Σ’) qui vont faire l'objet de
mon « addendum 1 » plus
bas.
Toujours est-il que, malgré ces limitations, Curry-Howard établit
une correspondance entre, côté logique propositions
et preuves de ces propositions, et, côté
informatique, types dans un langage informatique
fortement typé et termes (i.e., programmes) de ces
types. À un certain niveau c'est même une trivialité (observer qu'on
exactement les mêmes règles de formation des deux côtés : c'est juste
deux façons de voir le même acteur, cet acteur étant une sorte de
λ-calcul qui peut servir soit à désigner des preuves soit à coder des
programmes) ; mais quand même, cette correspondance permet
d'interpréter une preuve comme quelque chose qui va
s'exécuter, prendre des données en entrée et renvoyer des résultats à
la sortie, et c'est assez frappant, et c'est l'essence de ce
qui permet d'extraire d'une preuve constructive un programme réalisant
le calcul qu'elle prétend construire (j'agite un peu les mains ici).
À titre d'exemple, le programme qui correspond à la preuve
« évidente » de A∧B ⇒ B∧A
(si A et B sont vrais, alors B
et A sont vrais
) est le programme qui prend en entrée
un couple et échange les deux coordonnées de ce couple (lesquelles
peuvent être de types arbitraires).
[#] Comme je
l'ai déjà signalé ici, autoriser
ces appels récursifs revient très précisément, au niveau preuves, à
autoriser les raisonnements du style suivant : Je veux démontrer
que les poules ont des dents. Je tiens l'affirmation suivante :
Il est peut-être intéressant de s'intéresser à des
logiques paraconsistantes dans lesquelles une telle démonstration
serait permise (et du coup, tout est démontrable, de même que dans un
langage de programmation usuel on peut fabriquer un programme de
n'importe quel type — même le type vide, c'est juste que le programme
ne terminera pas), mais ce n'est pas ce qu'on appelle usuellement une
« démonstration » mathématique.Si
j'ai raison, alors les poules ont des dents.
Clairement, si j'ai
raison (c'est-à-dire, si cette affirmation est vraie), alors les
poules ont des dents. Mais c'était justement mon affirmation : donc
j'ai raison. Donc, par ce qui vient d'être démontré, les poules ont
des dents.
De façon un petit peu plus détaillée, la correspondance de Curry-Howard met en regard (je vais essayer d'expliquer ces différents points dans la suite, donc ceci est un divulgâchis qui a pour but d'aider à se retrouver dans la masse de mes explications si on décide de la lire en diagonale) :
- propositions avec types ;
- preuves avec termes (= programmes) ;
- implication logique (P⇒Q) avec types fonctions (σ→τ, qui correspond aux fonctions prenant une valeur de type σ et renvoyant une valeur de type τ) ;
- modus ponens (application d'une implication : si P⇒Q et P alors Q) avec application d'une fonction (une fonction σ→τ s'applique à un type σ pour donner un type τ) ;
- ouverture d'une hypothèse (pour démontrer une implication) avec λ-abstraction (= définition d'une fonction à partir d'un argument) ;
- hypothèses actuellement ouvertes avec variables libres (en contexte) dans le programme ;
- hypothèses déchargées avec variables liées dans le programme ;
- conjonction (
et
logique : P∧Q) avec types produits (σ×τ, qui correspond aux données d'un couple d'une valeur de type σ et d'une valeur de type τ) ; - disjonction (
ou
logique : P∨Q) avec types produits (σ+τ, qui correspond aux données soit d'une valeur de type σ soit d'une valeur de type τ, avec un sélecteur qui indique dans quel cas on se trouve) ; - le vrai (noté ‘⊤’, affirmation tautologiquement vraie) avec le type unité (ayant une seule valeur, triviale) ;
- le faux (noté ‘⊥’, affirmation tautologiquement fausse) avec le type vide (n'ayant aucune valeur) ;
- quantification universelle ∀(v:U).P(v) (qui est une sorte de « conjonction en famille » ⋀v:U P(v) sur tous les v de type U) avec types produits en famille ∏v:U σ(v) (type des fonctions prenant un v de type U et renvoyant une valeur de type σ(v)) ;
- quantification existentielle ∃(v:U).P(v) (qui est une sorte de « disjonction en famille » ⋁v:U P(v) sur les v de type U) avec types sommes en famille ∑v:U σ(v) (type des données d'un v₀ de type U et d'une valeur de type σ(v₀)).
La correspondance est surtout satisfaisante dans le sens des preuves vers les programmes, i.e., donnée une démonstration, arriver à construire un programme. C'est cette direction que je vais essayer d'exposer ci-après, en laissant globalement de côté la question de si on obtient tous les programmes de cette façon (ce qui demanderait d'expliquer précisément ce que sont « tous les programmes », et j'ai peur qu'on ne puisse avoir qu'une réponse un peu triviale en prenant la définition de programme qui fait rend Curry-Howard bijectif, c'est-à-dire de prendre pile-poil ceux qu'on peut fabriquer de la sorte : c'est en quelque sorte tout l'objet du typage que de limiter les programmes écrivibles à ceux que la correspondance de Curry-Howard atteint).
Bref, mon but dans la suite est d'exposer ça plus précisément, d'abord dans le cas purement propositionnel, c'est-à-dire sans quantificateurs (c'est nettement plus simple et si ça peut sembler ennuyeux je pense qu'il a déjà énormément à nous apprendre), et ensuite dire des choses plus vagues sur les quantificateurs (les quantificateurs posent toutes sortes de difficultés pénibles sur ce qu'on a le droit de quantifier exactement), en regardant d'un peu plus près la logique du premier ordre (qui est la forme de quantification la plus simple) ; je finis par parler de deux points indépendants (et que je ne comprends que de façon très imparfaite, donc je serai encore plus vague et à la limite de l'agitage de mains) : la question du sens du ‘∃’ d'une part, et l'imprédicativité de l'autre.
L'exposition que je vais faire ici suit pour le début la même idée que mon cours, pour laquelle on peut se référer à ce jeu de transparents pour la partie propositionnelle, mais je vais plutôt partir du côté preuves et ne pas entrer dans une description précise de ce qu'est le λ-calcul simplement typé. En revanche, la fin de ce billet va nettement au-delà de ce que je compte exposer dans mon cours (la partie de mon cours sur les quantificateurs est encore à l'état d'ébauche au moment où j'écris ce paragraphe, mais de toute façon je ne vais pas dire grand-chose).
Puisque ce sera le côté « preuves », je commence par des explications sur la logique intuitionniste (propositionnelle pour commencer) et sur ses règles de démonstration : on peut aussi se référer à ce billet passé pour le contexte général (y compris historique) sur les maths constructives, et cet autre billet (assez mal écrit) pour une description un peu différente des règles de la logique (en style « calcul des séquents »).
❦
Le cas du calcul propositionnel
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)
- (2) Faisons l'hypothèse : A
- (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
- (5) Faisons l'hypothèse : A
- (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 P1,…,Pr ⊢ Q
pour dire on a démontré Q sous les
hypothèses P1,…,Pr
.
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 v1:P1,…,vr:Pr ⊢ t:Q
pour dire t désigne une preuve de Q dans
laquelle les variables
libres v1,…,vr
désignent des hypothèses qui
supposent P1,…,Pr
:
le point intéressant c'est que t, dans cette histoire, est
une expression (ou λ-terme
) formée à partir des
variables v1,…,vr,
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
xwith
ι₁v₁↦t₁, ι₂v₂↦t₂) : Q (les variables v₁ et v₂, qui peuvent d'ailleurs être la même, deviennent liées dans la notation(
). 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₂.match
xwith
ι₁v₁↦t₁, ι₂v₂↦t₂) - (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)⟩
Si ce n'est pas clair, revoici la démonstration dans laquelle j'ai écrit les termes construits au fur et à mesure de la démonstration partielle, montrant comment on obtient le λ-terme final :
- (1) Par
hypothèse :
u : A∨B ⇒ C ⊢ u : A∨B ⇒ C - (2) Par
hypothèse :
u : A∨B ⇒ C, x : A ⊢ x : A - (3) De (2), par introduction gauche
du ‘∨’ :
u : A∨B ⇒ C, x : A ⊢ ι₁(A,B)x : A∨B - (4) De (1) et (3), par élimination
du ‘⇒’ :
u : A∨B ⇒ C, x : A ⊢ u(ι₁(A,B)x) : C - (5) De (4), par introduction
du ‘⇒’ :
u : A∨B ⇒ C ⊢ λ(x:A).u(ι₁(A,B)x) : A⇒C - (6) Par
hypothèse :
u : A∨B ⇒ C, y : B ⊢ y : B - (7) De (6), par introduction droite
du ‘∨’ :
u : A∨B ⇒ C, y : y : B ⊢ ι₂(A,B)y : A∨B - (8) De (1) et (7), par élimination
du ‘⇒’ :
u : A∨B ⇒ C, y : B ⊢ u(ι₂(A,B)y) : C - (9) De (8), par introduction
du ‘⇒’ :
u : A∨B ⇒ C ⊢ λ(y:B).u(ι₂(A,B)y) : B⇒C - (10) De (5) et (9), par introduction
du ‘∧’ :
u : A∨B ⇒ C ⊢ ⟨λ(x:A).u(ι₁(A,B)x), λ(y:B).u(ι₂(A,B)y)⟩ : (A⇒C)∧(B⇒C) - (11) De (10), par introduction du ‘⇒’ :
⊢ λ(u:A∨B ⇒ C). ⟨λ(x:A).u(ι₁(A,B)x), λ(y:B).u(ι₂(A,B)y)⟩ : (A∨B ⇒ C) ⇒ (A⇒C)∧(B⇒C)
Comme ceci a été excessivement pénible à écrire, je ne vais pas le refaire pour les autres, mais j'espère que le procédé est clair.
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 v1,…,vr de types P1,…,Pr (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
pourla fonction qui prend v en argument et renvoie t
est la notation usuelle du λ-calcul ; en OCaml par exemple ceci se note
. Mais ici on veut indiquer le type de tous les objets introduits, d'où la notation avecfun
v->
t: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
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.match
xwith
ι₁v₁↦t₁, ι₂v₂↦t₂ - (Introduction du ‘⊤’)
- La notation ‘•’ désigne la valeur triviale de type unité.
- (Élimination du ‘⊥’ ou
ex falso quodlibet
) - La
notation
ne désigne rien du tout car il n'y a pas de valeur de type vide.exfalso
(Q) x
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).
❦
Au-delà du calcul propositionnel : les quantificateurs
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 :
match
z with
⟨v,w⟩↦s) : Q.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 (
lorsque Γ ⊢ z : ∃(v:U).P(v),
qui serait une façon d'extraire la valeur dont le ‘∃’ prétend affirmer
l'existence.match
z with
⟨v,w⟩↦v)
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)(x1,…,xr) (qu'il serait sans doute plus logique de noter A(r)x1⋯xr 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 xi 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 Ur→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 Ur→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
(
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.match
zwith
⟨v,w⟩↦v)
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
hwith
⟨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
π₁pwith
⟨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
pwith
⟨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
pwith
⟨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
pwith
⟨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.
❦
Addenda
De nouveau, je m'étais d'abord dit que j'allais m'arrêter là, mais en fait je finis ce billet par deux sous-billets indépendants l'un de l'autre (et d'ailleurs aussi indépendants de la sous-section ci-dessus sur l'arithmétique du premier ordre) pour essayer d'expliquer un peu, en agitant les mains et en restant assez vague et assez informel, deux choses que j'ai eu un mal fou à comprendre à moitié (et que je n'ai toujours comprises qu'à moitié) concernant la théorie des types. Ce ne sont pas des explications très précises, et je répète qu'il y a beaucoup de choses que je ne comprends toujours pas bien, mais mon esprit est moins confus maintenant qu'il ne l'était, et du coup, s'il y a des gens dans le même état de confusion que je l'étais il y a quelques mois, et tout aussi furieux que moi de ne trouver aucune explication informelle décente[#6] de ces questions, autant que je publie ce que j'ai réussi à démerdouiller.
[#6] Petite attaque : les théoriciens des types aiment vous balancer des longues règles de typage avec plein de Γ⊢⋯ diversement décorés au-dessus et en-dessous de la barre, et plein de symboles abscons comme ‘*’, ‘□’, sans vous donner la moindre intuition sur ces règles ni faire le moindre effort pour souligner ce qui est inhabituel ou remarquable dedans, et c'est apparemment à vous d'être capables de prendre deux pages absconses comme ça, de les comparer et de trouver tout de suite que l'une permet de créer des types dépendant de termes et l'autre pas, ou autre subtilité de ce genre pas du tout apparente dans les règles et que l'auteur n'a pas envie de bouger le plus petit doigt pour vous aider à voir. Les gens qui trouvent que les textes de géométrie algébrique sont arides, formels et dépourvus d'explications intuitives devraient voir du côté de la théorie des types : moi qui ai lu les deux peux dire que l'absence de pédagogie est une valeur largement partagée par plusieurs branches des mathématiques.
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é
), lorsqu'on déconstruit
une disjonction, uniquement pour construire une démonstration, et pas
pour construire un objet.match
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
: plus précisément, la
règle serait que le match
hu with
⟨v,z⟩ ↦ vmatch
(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
(avec une sous-exception dans le cas d'un singleton où
c'est quand même
autorisé[#9]).Prop
is not allowed on a predicate in
sort Set
because proofs can be eliminated only to build
proofs
[#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.
Il peut être intéressant de recopier ici des exemples qu'on m'a donnés de termes qu'on peut écrire dans le système F mais pas dans le λ-calcul simplement typé (disons, si on veut, que les programmes écrits en OCaml ne typent pas), parce que je trouve assez instructif de réfléchir à ce que disent ces termes en tant que preuves de leurs types respectifs et à ce qu'ils font en tant que programmes :
- λ(A:*). λ(x:∀(A:*).A). x ((∀(B:*).B)⇒A) x qui a pour type ∀(A:*). (∀(B:*).B) ⇒ A (c'est une sorte de ex falso quodlibet mais avec une preuve bizarre : on commence par appliquer ∀B.B pour B valant (∀B.B)⇒A et on l'applique à lui-même : on remarque que l'imprédicativité joue à fond ; en tant que programme, il ne fait pas grand-chose parce qu'une valeur de type ∀A.A n'existe pas, mais s'il y en avait une il l'appliquerait à elle-même)
- λ(f:∀(A:*).A⇒A). f (∀(A:*).A⇒A) f qui a pour type (∀(A:*).A⇒A) ⇒ (∀(A:*).A⇒A) (la proposition prouvée est évidente, mais la preuve n'est pas celle qu'on attend : pour prouver (∀A.A⇒A) ⇒ (∀A.A⇒A) on commence par appliquer l'hypothèse avec A valant ∀A.A⇒A et on l'applique à lui-même)
- λ(A:*). λ(B:*). λ(p:∀(C:*).((A⇒B)⇒A⇒C)⇒C). p
(A⇒B)
(λ(f:A⇒B).λ(x:A).f)
(p A
(λ(f:A⇒B).λ(x:A).x))
qui a pour type
∀(A:*). ∀(B:*). (∀(C:*).((A⇒B)⇒A⇒C)⇒C)
⇒ B (celui-ci fait quelque chose de vaguement utile en tant
que programme puisqu'il prend un couple codé dans une clôture comme
expliqué plus haut, et applique sa première composante à la seconde ;
mais si on essaye de l'écrire en OCaml,
fun p -> p (fun f -> fun x -> f) (p (fun f -> fun x -> x))
, ben ça ne type pas)
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
−1) 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 ?