Les subtilités de Coq, épisode 3 : systèmes de typage purs

28 novembre 2024 ⋅ Retour à l'accueil du blog

Dans ce troisième épisode de ma série sur la théorie des types (épisode précédent), je définis la notion de système de typage pur — en abrégé PTS, pour pure type system —, qui permet de présenter de manière unifiée un grand nombre de théories des types. Le but est de pouvoir ensuite parler du paradoxe de Girard dans le cadre des PTS.

Définition

À ce stade, j'invite fortement le lecteur non-averti, avant de prendre connaissance de la définition, à prendre une feuille de papier et à essayer d'écrire les règles d'un système de déduction plausible pour un λ-calcul typé avec des types dépendants.

Donnons quelques indications pour retomber sur quelque chose de proche des PTS. On va se donner un jeu de sortes $S$ (à penser comme Prop, Set et les univers Type en Coq). Chaque sorte pourra avoir un nombre quelconque de types possibles (donc possiblement aucun, et possiblement plusieurs), qui seront d'autres sortes, et comme on cherche à donner une définition assez générale, on va prendre en paramètre du PTS un ensemble d'axiomes de sorte $A ⊆ S × S$, dont les paires $(s_1, s_2)$ se comprennent comme « $s_1$ est de type $s_2$ ».

Il faudra aussi pouvoir former des produits dépendants. À nouveau, on ne va pas chercher à fixer les choses pour rester général, donc on va prendre un ensemble de règles $R ⊆ S × S × S$, où la règle $(s_1, s_2, s_3)$ signifie que le type produit dépendant $Π (x : T) ⋅ U$ (ou, en notation Coq, forall x : T, U) sera typé par la sorte $s_3$ lorsque $T$ et $U$ sont respectivement typés par les sortes $s_1$ et $s_2$.

Avec ceci, vous devriez avoir tous les éléments. Vraiment, faites-le ! Il n'y a rien de plus instructif que de se forcer à se poser cette question pour se rendre compte des subtilités en jeu.

Une fois que vous avez fait cet exercice, vous pouvez comparer avec cette définition :

Définition. On fixe un ensemble de variables $V$ (infini dénombrable). On se donne :

• Un ensemble de sortes $S$,
• Un ensemble d'axiomes $A ⊆ S × S$,
• Un ensemble de règles $R ⊆ S × S × S$.

On définit inductivement les termes du λΠ-calcul par la grammaire de termes :

$$\def\or{\ |\ } Λ ::= V \or S \or Λ Λ \or λ (V : Λ) ⋅ Λ \or Π (V : Λ) ⋅ Λ$$

Les jugements de typage seront de la forme $Γ ⊢ u : U$, où $u$ et $U$ sont des termes, et le contexte de typage $Γ$ est une liste (ordonnée) d'hypothèses également de la forme $u : U$.

La substitution de $x$ par $v$ dans $u$ est définie de la manière usuelle ($λ$ et $Π$ lient une variable) et notée $u[x:=v]$. La β-équivalence est aussi définie comme usuellement (les Π ne créent pas de nouveaux rédexs) et notée $=_β$.

Le système de typage pur associé à $S, A, R$ est défini sur les termes par les règles de déduction suivantes, où implicitement $x$ désigne une variable, $s, s_1, s_2, s_3$ une sorte, et $u, v, U, V$ un terme. (Ces règles ignorent volontairement et allègrement tous les problèmes de variables libres et liées, qui sont très peu intéressants.)

$$\def\next{\\[2em]} \boxed{ \begin{align*} \text{Axiome :}& \quad \frac{}{⊢ s_1 : s_2} \quad \footnotesize{(s_1, s_2) ∈ A} \next \text{Variable :}& \quad \frac{Γ ⊢ V : s}{Γ, x : V ⊢ x : V} \next \text{Affaiblissement :}& \quad \frac{Γ ⊢ u : U \qquad Γ ⊢ V : s}{Γ, x : V ⊢ u : U} \next \text{Application :}& \quad \frac{Γ ⊢ u : Π (x : V) ⋅ U \qquad Γ ⊢ v : V}{Γ ⊢ u v : U[x:=V]} \next \text{λ-abstraction :}& \quad \frac{Γ ⊢ Π (x : V) ⋅ U : s \qquad Γ, x : V ⊢ u : U}{Γ ⊢ λ (x : V) ⋅ u : Π (x : V) ⋅ U} \next \text{Produit dépendant :}& \quad \frac{Γ ⊢ V : s_1 \qquad Γ, x : V ⊢ U : s_2}{Γ ⊢ Π (x : V) ⋅ U : s_3} \quad \footnotesize{(s_1, s_2, s_3) ∈ R} \next \text{Conversion :}& \quad \frac{Γ ⊢ x : U}{Γ ⊢ x : V} \quad \footnotesize{U =_β V} \end{align*} }$$

Remarque diverses

Cette définition mérite quelques commentaires.

La règle d'application et la règle de produit dépendant ne devraient pas contenir de surprise majeure. La règle de λ-abstraction non plus, mais il faut tout de même faire attention à ne pas écrire

$$\frac{Γ ⊢ V : s_1 \qquad Γ, x : V ⊢ u : U}{Γ ⊢ λ (x : V) ⋅ u : Π (x : V) ⋅ U}$$

Cette règle n'est pas bonne parce que même si $V$ type dans la sorte $s_1$, et $U$ type dans la sorte $s_2$ sous l'hypothèse supplémentaire $x : V$, rien ne garantit que le produit dépendant $Π (x : V) ⋅ U$ soit bien typé, car il n'y a possiblement aucune règle dans $R$ de la forme $(s_1, s_2, s_3)$ pour une troisième sorte $s_3$ : on ne peut pas former de produits dépendants arbitraires, les règles peuvent imposer des restrictions sur la quantification.

Bien que cette présentation soit standard, l'algorithme de typage qu'on en extrait immédiatement est terriblement inefficace, à cause de la formulation des règles d'axiome, de variable et d'affaiblissement. Telles que je les ai écrites, tous les types dans le contexte n'arrêtent pas d'être revérifiés en permanence. Par exemple, prenons un terme tout simple :

$$λ (x : Y → Z → X) (y : Y) (z : Z) ⋅ x y z$$

où comme d'habitude $X → Y$ dénote $λ (x : X) ⋅ Y$ lorsque $x$ n'apparaît pas dans $Y$, et en supposant que les axiomes et règles permettent de typer ce terme (peu importe à ce stade). Donnons-nous un contexte de départ $Γ_0 := X : s, Y : s, Z : s$ où $s$ est une sorte quelconque. Voici la manière dont il va être typé en $(Y → Z → X) → Y → Z → X$ (je n'ai même pas le courage de dessiner l'arbre de dérivation) :

• La règle de λ-abstraction va vérifier que $Y → Z → X$ est bien typé dans $Γ_0$ (pas de problème), puis va vérifier que $λ (y : Y) (z : Z) ⋅ x y z$ est bien typé dans le contexte $x : Y → Z → X$ (et enfin vérifier que les sortes permettent d'écrire le produit $(Y → Z → X) → Y → Z → X$),

• On applique de nouveau la règle de λ-abstraction, deux fois, pour se retrouver à typer $x y z$ dans le contexte $x : Y → Z → X, y : Y, z : Z$,

• On utilise deux fois la règle d'application pour se retrouver finalement avec trois sous-arbres à construire, pour vérifier $Γ ⊢ x : Y → Z → X$, $Γ ⊢ y : Y$ et $Γ ⊢ z : Z$ où $Γ := Γ_0, x : Y → Z → X, y : Y, z : Z$,

• Et ici, on comprend qu'il y a plus de travail que ce à quoi on s'attendrait. Pour dériver $Γ_0, x : Y → Z → X, y : Y, z : Z ⊢ x : Y → Z → X$, on est obligé d'appliquer deux fois la règle affaiblissement, en vérifiant que $Y$ et $Z$ sont bien typés. On se ramène à dériver $Γ_0, x : Y → Z → X ⊢ x : Y → Z → X$, mais pour cela, il faut vérifier que $Γ_0 ⊢ Y → Z → X$ pour une certaine sorte $s$, et ceci se fait par de nouvelles applications de la règle produit suivies d'affaiblissements, axiomes et variables. Et ce n'est pas fini ! Il reste encore $Γ_0, x : Y → Z → X, y : Y, z : Z ⊢ y : Y$ et $Γ_0, x : Y → Z → X, y : Y, z : Z ⊢ z : Z$, où on doit refaire plus ou moins le même travail…

Bref : à chaque variable ou sorte, on revérifie que tout le contexte entier est bien typé (et ceci récursivement…), et c'est une (très) mauvaise idée du point de vue algorithmique. En plus, telles quelles, les règles ne sont même pas déterministes, parce que l'affaiblissement peut s'appliquer à divers endroits (si je veux typer $u v$ dans un contexte dont la dernière variable $x$ n'apparaît pas dans $u v$, je peux soit typer $u$ et $v$ dans ce contexte, avec des affaiblissements dans chacune des deux dérivations, soit appliquer maintenant l'affaiblissement et ainsi économiser des affaiblissements plus tard).

Bien que la présentation précédente soit standard, il est donc sans doute préférable d'utiliser ce style de présentation :

$$\def\next{\\[2em]} \boxed{ \begin{align*} \text{Axiome :}& \quad \frac{}{Γ ⊢ s_1 : s_2} \quad \footnotesize{(s_1, s_2) ∈ A} \next \text{Variable :}& \quad \frac{}{Γ, x : V, Γ' ⊢ x : V} \next \text{Application :}& \quad \frac{Γ ⊢ u : Π (x : V) ⋅ U \qquad Γ ⊢ v : V}{Γ ⊢ u v : U[x:=V]} \next \text{λ-abstraction :}& \quad \frac{Γ ⊢ Π (x : V) ⋅ U : s \qquad Γ, x : V ⊢ u : U}{Γ ⊢ λ (x : V) ⋅ u : Π (x : V) ⋅ U} \next \text{Produit dépendant :}& \quad \frac{Γ ⊢ V : s_1 \qquad Γ, x : V ⊢ U : s_2}{Γ ⊢ Π (x : V) ⋅ U : s_3} \quad \footnotesize{(s_1, s_2, s_3) ∈ R} \next \text{Conversion :}& \quad \frac{Γ ⊢ u : U}{Γ ⊢ u : U'} \quad \footnotesize{U =_β U'} \end{align*} }$$

Ici, il n'y a plus d'affaiblissement, la règle axiome accepte un contexte arbitraire à gauche, et la règle variable ne demande plus forcément que la variable soit la dernière dans le contexte mais accepte des hypothèses supplémentaires qui la suivent.

Il est facile de se convaincre que le jugement $⊢ u : U$ est dérivable dans ce nouveau système de règles si et seulement s'il était dérivable dans le précédent. Ceci est le cas parce que les règles qui introduisent de nouvelles variables dans le contexte, à savoir la λ-abstraction et le produit dépendant, ne le font qu'après avoir vérifié que leur type était lui-même bien typé. Néanmoins, il n'y a pas équivalence entre les deux, ceci parce que le nouveau système autorise, par exemple, les jugements $x : s, y : \text{portnawak} ⊢ x : s$, où $\text{portnawak}$ est un terme quelconque possiblement intypable. Le précédent obligerait à typer $\text{portnawak}$ dans l'application de la règle affaiblissement qui dérive ce jugement de $x : s ⊢ x : s$. De même, $y : \text{portnawak}, x : s ⊢ x : s$ serait rejeté, d'une manière légèrement différente : la règle variable demanderait de dériver $y : \text{portnawak} ⊢ s : s'$ (pour une sorte $s'$ quelconque), et ceci ne pourrait se faire qu'à partir de la règle axiome, mais celle-ci ne dérive que $⊢ s : s'$, donc pour passer à $y : \text{portnawak} ⊢ s : s'$, il faut appliquer l'affaiblissement, qui à nouveau rejette $\text{portnawak}$.

Bref : le but de ces restrictions sur les règles axiome et variable et de la règle affaiblissement est d'empêcher de dériver des jugements dans des contextes mal typés, mais ceci se fait au prix d'une revérification constante des contextes partout, donc il vaut sans doute mieux s'en passer, ou alors introduire les règles selon ma deuxième présentation, puis séparément introduire une notion de bien-formation d'un contexte.

Au passage, cette nouvelle présentation a le bon goût d'être beaucoup plus déterministe. La règle à appliquer sur un terme est entièrement déterminée par sa forme… sauf pour la règle de conversion, dont il faut justement que je discute.

Digression sur la conversion

Une discussion récente m'a fait prendre conscience du fait que le concept d'égalité définitionnelle, qui est absolument fondamental en théorie des types, n'est sans doute pas souvent expliqué dans les cours d'assistants de preuve ni de λ-calcul, donc il vaut sans doute la peine que j'en dise quelques mots.

Pour illustrer à quel point ce concept est essentiel, on va typiquement définir exists x : X, P x comme un type inductif qui en Coq se note @ex X P, donc par exemple exists x : nat, x = 0 est une notation pour @ex nat (fun x => x = 0), et si on veut prouver cette proposition, il faut donner un témoin et une preuve que le témoin satisfait la proposition, soit un x et une preuve de P x : en l'occurrence, un x : nat et une preuve de (fun x => x = 0) x, et on peut évidemment choisir 0 : nat, mais encore faut-il prouver, non pas 0 = 0, mais bien (fun x => x = 0) 0. Encore faut-il pouvoir simplifier ce type (fun x => x = 0) 0 en 0 = 0 pour pouvoir en exhiber un habitant.

Fondamentalement, l'égalité « normale », celle qui est visible, celle dont on parle quand on écrit 0 = 0, et qui s'appelle l'égalité propositionnelle, va être définie par un constructeur de type $∀ X, ∀ (x : X), x = x$ (en Coq, @eq_refl : forall (X : Type) (x : X), x = x). Si on imagine une version de Coq qui ressemble à la définition des PTS ci-dessus mais sans la règle de conversion, le terme @eq_refl nat 0 va être de type 0 = 0 par deux utilisations de la règle application, mais d'aucun autre type.

On peut tout à fait imaginer un système de typage où ces égalités doivent être prouvées à la main (par exemple, on aurait une règle qui déduit $⊢ (λ x ⋅ u) v = u[x:=v]$ sans hypothèse). D'ailleurs, c'est à peu près ce qui se passe, disons, en logique du premier ordre : on a des axiomes comme $∀ x, 0 + x = x$ dans une théorie comme l'arithmétique de Peano, et à chaque fois qu'on veut prouver une égalité, il faut la déduire d'un axiome. Mais dans un vrai assistant de preuve, ce serait incroyablement fastidieux (encore plus que l'égalité ne l'est déjà en Coq…).

Il est donc très tentant, et on le fait toujours, d'ajouter une règle de conversion de la forme

$$\frac{Γ ⊢ u : U}{Γ ⊢ u : U'} \qquad \footnotesize{Γ ⊢ U ≡ U'}$$

où la notation $Γ ⊢ U ≡ U'$ signifie que $U$ et $U'$ sont « définitionnellement égaux » dans le contexte $Γ$.

On peut mettre plus ou moins de choses dans l'égalité définitionnelle. Dans les PTS, c'est simplement la β-équivalence, mais en général, elle peut dépendre du contexte $Γ$.

En regardant cette règle avec les lunettes de Curry-Howard, on obtient « deux propositions définitionnellement égales sont équivalentes », ce qui n'est pas habituel dans les systèmes logiques les plus usuels pour les mathématiciens, essentiellement la logique du premier ordre et la logique d'ordre supérieur.⁰ Ce type de règle porte un nom, c'est la déduction modulo, et vu que je viens d'expliquer qu'il s'agit de rendre le système utilisable en pratique, il n'est sans doute pas si surprenant que la déduction modulo ait d'abord été étudiée dans le cadre de la démonstration automatique. C'est d'ailleurs l'origine du nom des solveurs SMT, acronyme de « satisfiabilité modulo théorie ». On peut faire de la déduction modulo en logique du premier ordre ou d'autres systèmes, par exemple en modifiant l'arithmétique de Peano pour changer les axiomes comme $∀ x, 0 + x = x$ en règles d'égalité définitionnelle comme $0 + x ≡ x$. Pour une introduction générale très lisible, cf. Deduction modulo theory de Gilles Dowek.

Pour qu'il soit décidable de vérifier si un terme est bien typé, il est essentiel que l'égalité définitionnelle soit décidable. Typiquement, on travaille avec un λ-calcul qui est fortement normalisant et confluent, donc tout terme a une unique forme normale, et deux termes sont β-équivalents si et seulement si leurs formes normales sont identiques. Si l'égalité définitionnelle est simplement la β-équivalence, il suffit donc de β-réduire jusqu'au bout les deux termes et de comparer les formes normales.

On peut ajouter des choses en plus dans cette égalité définitionnelle. Je peux mentionner trois extensions (dont j'espère reparler dans des billets futurs) :

• Les let x := v in u, qui peuvent différer de $(λ x ⋅ u) v$ en ce que l'égalité définitionnelle entre $x$ et $v$ va être disponible pendant la vérification du typage de $u$.

• En Lean, la sorte Prop possède l'indiscernabilité des preuves définitionnelle, c'est-à-dire que plutôt que d'ajouter un axiome comme on peut le faire en Coq (Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.), deux termes du même type sont considérés comme définitionnellement égaux dès que leur type est une proposition. Malheureusement, comme expliqué dans la thèse de master de Mario Carneiro, la manière dont ceci est fait casse la normalisation forte et la décidabilité. En Coq, il existe depuis quelques années une sorte expérimentale SProp parallèle à Prop qui fait plus ou moins la même chose, mais avec des restrictions pour préserver normalisation et décidabilité.

• Dans l'équipe Deducteam du LMF sont développés des outils comme Dedukti dont l'idée est de mettre énormément de choses dans l'égalité définitionnelle, y compris des règles de réécriture définies par l'utilisateur. (Par exemple, l'article Embedding Pure Type Systems in the lambda-Pi calculus modulo de Cousineau et Dowek précise comment traduire les PTS que j'ai présentés ici dans ce type de système.)

On peut aussi spécifier l'égalité définitionnelle par un système de déduction qui s'entremêle au typage plutôt que d'en être indépendant, ce qui peut permettre certaines extensions. C'est la « conversion typée », par opposition à la « conversion non-typée ». Cette réponse d'András Kovács sur StackExchange donne plus de détails.

Il faut avoir conscience que cette règle de conversion est essentiellement la seule source de complexité au sens calculatoire dans la vérification du typage. Si on retire la conversion de la définition des PTS ci-dessus, on constate qu'il n'y a qu'une règle qui peut s'appliquer à un terme, choisie en fonction de sa forme (sorte, variable, application, λ-abstraction ou produit dépendant). Le typage est alors décidable efficacement (en temps polynomial). Mais avec la règle de conversion, les choses sont toutes autres. Un exemple suffira :

Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => (S n')*(fact n') end.
Check eq_refl : fact 101 = 101 * fact 100.

D'après les règles de typage de Coq, il devrait théoriquement accepter ce code, mais comme il est amené à calculer $101!$ (en unaire !) pour décider l'égalité définitionnelle, il est probablement parti pour y mettre plus longtemps que l'âge de l'Univers.

En fait, on voit facilement que la complexité de la vérification du typage de Coq est minorée par n'importe quelle fonction définissable en Coq. En sachant que la force de Coq est comparable à celle de ZFC (probablement avec $ω$ univers de Grothendieck, mais ne pinaillons pas entre le méga-giga-hyper-grand et le super-méga-giga-hyper-grand)… l'algorithme qui vérifie si un terme de Coq est à peu près imbattable dans la catégorie des algorithmes de complexité théorique inimaginable. Correction (4 décembre 2024) : En fait, la force de Coq est sans doute plus proche de la théorie des ensembles de Zermelo, mais c'est une question subtile, cf. les commentaires.

(Bien sûr, on peut aussi s'amuser à prouver $101! = 101 ⋅ 100!$ en logique du premier ordre en calculant entièrement les deux côtés, simplement, cette fois, la longueur de la preuve devient proportionnelle à la longueur du calcul, donc on n'a pas cette explosion de complexité. En Coq, on peut aussi guider la réduction, en l'occurrence faire Definition fact_101_eq_fact_101 : fact 101 = 101 * fact 100. Proof. unfold fact. reflexivity. Defined.)

Le λ-cube

Bref. Je digresse, mais je n'ai toujours pas donné un seul exemple concret de système de typage pur. L'exemple le plus connu de cette définition est une famille de huit systèmes qui forment le λ-cube de Barendregt. En partant du λ-calcul simplement typé, on peut rajouter trois extensions orthogonales, généralement résumées par : « termes dépendant de types », « types dépendant de termes », et « types dépendant de types ». Le nom « λ-cube » provient de la représentation graphique de ces extensions sous forme d'un cube dont chacun des huit λ-calculs est un sommet (figure ci-dessous prise sur Wikipédia).

Pour définir ces systèmes, on va poser $S = \{*, □\}$, $A = \{(*, □)\}$, et $R = \{(*, *, *)\} ∪ R'$ en considérant les huit possibilités pour

$$R' ⊆ \{(□, *, *), (*, *, □), (□, □, □)\}$$

Intuitivement, $*$ va être la sorte des types de base (comme « entier » ou « booléen »), et $□$ va être la sorte des types eux-mêmes.

Commençons par le cas $R' = ∅$. Les seules λ-abstractions qu'on a le droit de former sont $λ (x : U) ⋅ v$ où $U : *$ et $v : V : *$. Autrement dit, les fonctions ne peuvent que traiter des éléments des types de bases, par des types eux-mêmes.

On vérifie par des récurrences immédiates que si $u : U : *$ alors $u$ ne contient pas de produit dépendant ($Π$) tandis que $U$ ne contient pas de λ-abstraction ni d'application, et que si le produit dépendant $Π (x : U) ⋅ V$ type, alors $x$ ne figure nulle part dans $V$. Bref : les termes dans la sorte $*$ sont des λ-termes usuels, les termes dans le type $*$ (donc la sorte $□$) sont des types simples, avec seulement des types primitifs (on met $U : *$ dans le contexte) ou des types fonction non dépendants ($V → U := Π (x : V) ⋅ U$), et on reconnaît le λ-calcul simplement typé et ses trois règles

$$\frac{}{Γ, x : V ⊢ x : V}$$

$$\frac{Γ ⊢ u : V → U \qquad Γ ⊢ v : V}{Γ ⊢ u v : U}$$

$$\frac{Γ, x : V ⊢ u : U}{Γ ⊢ λ x ⋅ u : V → U}$$

Rajoutons maintenant les extensions annoncées. Je commence par les types dépendant de termes, qui correspondent bien à ce que l'on appelle « types dépendants ». On prend ici $R' = \{(*, □, □)\}$. On peut maintenant écrire $Π (x : V) ⋅ U : □$ où $V : *$ et (sous $x : V$) $U : □$, et en particulier $V → U$ où $V : *$ et $U : □$. Du point de vue logique, ceci correspond au passage de la logique propositionnelle à la logique du premier ordre. Par exemple, on peut se donner le contexte :

$$\begin{align*} &N : * \\ &Z : N \\ &S : N → N \\ &E : N → N → * \\ &+ : N → N → N \\ &P : Π (a : N) (b : N) ⋅ E (+ (S a) b) (S (+ a b)) \end{align*}$$

pour représenter les débuts de l'arithmétique de Peano, $ℕ, 0, S, =, +$ et l'axiome $S(a) + b = S(a + b)$. Noter que l'on ne peut pas exprimer le schéma de récurrence, qui serait

$$Π (P : N → *) ⋅ P Z → (Π (n : N) ⋅ P n → P (S n)) ⋅ Π (n : N) ⋅ P n$$

car $N → * := Π (n : N) ⋅ *$ vit dans $□$, donc on n'a pas le droit de quantifier dessus. Ce n'est pas une surprise au vu du fait qu'on ne peut pas non plus exprimer le schéma de récurrence par une unique formule du premier ordre, pour essentiellement la même raison.

Dans une autre direction, on peut rajouter les termes qui dépendent de types avec $R' = \{(□, *, *)\}$. On peut donc écrire $Π (X : *) ⋅ U$ où (sous $x : *$) $U : *$. Par exemple, $Π (X : *) ⋅ (Π (x : X) ⋅ X)$ devient valide et habité par $λ (X : *) ⋅ λ (x : X) ⋅ x$. Du point de vue logique, la quantification sur $*$ correspond à la logique du second ordre propositionnelle (l'exemple précédent est une preuve de $∀ X, X → X$), et on retrouve le système F de Girard et Reynolds. (À nouveau, pour vérifier l'équivalence avec la présentation usuelle, il faut faire des tas de petites récurrences.)

La dernière extension, types dépendant de types, $R' = \{(□, □, □)\}$, n'est pas si intéressante pour elle-même. Elle permet de mettre dans le contexte des choses comme $C : * → *$ qui se comprennent comme des constructeurs de types paramétrés (comme list). Elle devient un peu plus intéressante en combinaison avec les termes qui dépendent de types du système F (c'est le système Fω).

Enfin, en combinant tout, avec $R' = \{(*, □, □), (□, *, *), (□, □, □)\}$, on obtient le système appelé calcul des constructions — du moins l'une de ses variantes, parce qu'évidemment, ce ne serait pas drôle si tous étaient d'accord sur le sens de l'expression « calcul des constructions ».

Propriétés

Quelques propriétés qui sont ou ne sont pas vérifiées dans les PTS :

L'autoréduction est vérifiée : Si $u → v$ et $Γ ⊢ u : U$ alors $Γ ⊢ v : U$. C'est une récurrence directe.

L'inverse n'est pas vrai : si $Γ ⊢ v : U$ et $u → v$, alors on n'a pas forcément $u : U$. Ceci est déjà faux pour le λ-calcul simplement typé, par exemple en prenant $u := (λ x y ⋅ y) v (λ x ⋅ x x)$, mais la nouveauté par rapport au λ-calcul simplement typé est que même si $u$ est typable, ce n'est toujours pas vrai. Par exemple, prenons $u := (λ (x : X) ⋅ s_2) t$, où $t$ et $X$ sont des termes quelconques tels que $t : X : s_1$, et $v := s_2$. À condition de disposer d'un axiome $s_2 : s_3$, on a $v : s_3$. Mais pour avoir $u : s_3$, il faut typer $λ (x : X) ⋅ s_2$ dans $Π (x : X) ⋅ s_3$, ce qui nécessite d'avoir une règle $(s_1, s_3, s_3)$. Il est possible que cette règle soit absente, mais que l'on ait par contre une autre sorte $s_4$ avec un autre axiome $s_2 : s_4$ et une règle $(s_X, s_4, s_4)$, ce qui fait typer $u : s_4$ et $v : s_3$ ainsi que $v : s_4$ mais pas $u : s_3$.

L'unicité des types n'est pas forcément vérifiée : il se peut que $u : U$ et $u : U'$ avec $U, U'$ non définitionnellement égaux. Par exemple, si $A$ contient les axiomes $(s_1, s_2)$ et $(s_1, s_3)$ avec $s_2 ≠ s_3$, alors $s_1$ est à la fois de type $s_2$ et de type $s_3$. Néanmoins, l'unicité des types est vérifiée pour les PTS qui sont fonctionnels, au sens où pour tout $s_1$, il existe au plus un $s_2$ tel que $(s_1, s_2) ∈ A$, et pour tous $s_1, s_2$, il existe au plus un $s_3$ tel que $(s_1, s_2, s_3) ∈ A$.

La normalisation forte est vraie pour les systèmes du λ-cube, mais en général, elle n'est pas toujours vérifiée… j'y reviendrai.

Conclusion

J'espère que cette courte introduction sera suffisante pour comprendre le futur billet sur le paradoxe de Girard.

Pour plus de renseignements, je peux renvoyer vers le livre de Barendregt Lambda Calculi with Types (1992, collection Handbook of Logic in Computer Science), qui commence par une introduction générale classique au λ-calcul (syntaxe, réduction, développements finis, confluence, réduction de tête, standardisation, arbres de Böhm, entiers de Church, …), et se termine par un chapitre détaillé sur les systèmes de typage pur. (Attention à ne pas le confondre avec Lambda Calculus with Types, ouvrage collectif dirigé entre autres par le même auteur, et qui n'a pas du tout le même contenu.)

Je termine sur une conjecture qui est, semble-t-il, le graal du domaine, et qu'il paraît difficile de ne pas mentionner :

Conjecture de Barendregt-Geuvers-Klop : Si un système de typage pur est faiblement normalisant, alors il est fortement normalisant.

Commentaires

Inductive V : Type :=
| sup : forall (X : Type), (X -> V) -> V.

(*
NB : Les univers sont comme ceci :

Inductive V@{u} : Type@{u+1} :=
    sup : forall X : Type@{u}, (X -> V@{u}) -> V@{u}.
*)

Fixpoint Veq (A B : V) {struct A} : Prop :=
  let (X, f) := A in
  let (Y, g) := B in
  (forall x : X, exists y : Y, Veq (f x) (g y))
  /\ (forall y : Y, exists x : X, Veq (f x) (g y)).

Definition Vin (a A : V) : Prop :=
  let (X, f) := A in exists x : X, Veq (f x) a.


Require Import Classes.RelationClasses.

Instance Veq_refl : Reflexive Veq.
Proof.
  intros A. induction A as [X f IH]. split.
  - intros x. exists x. apply IH.
  - intros x. exists x. apply IH.
Qed.

Instance Veq_symm : Symmetric Veq.
Proof.
  refine (fix IH A B := _).
  destruct A as [X f], B as [Y g]. intros [H1 H2]. split.
  - intros y. destruct (H2 y) as [x Hx]. exists x. apply IH. apply Hx.
  - intros x. destruct (H1 x) as [y Hy]. exists y. apply IH. apply Hy.
Qed.

Instance Veq_trans : Transitive Veq.
Proof.
  refine (fix IH A B C := _).
  destruct A as [X f], B as [Y g], C as [Z h].
  intros [H_AB H_BA] [H_BC H_CB]. split.
  - intros x. destruct (H_AB x) as [y Hy]. destruct (H_BC y) as [z Hz].
    exists z. apply (IH (f x) (g y) (h z)). apply Hy. apply Hz.
  - intros z. destruct (H_CB z) as [y Hy]. destruct (H_BA y) as [x Hx].
    exists x. apply (IH (f x) (g y) (h z)). apply Hx. apply Hy.
Qed.

Instance Veq_equiv : Equivalence Veq.
Proof.
  split; [apply Veq_refl | apply Veq_symm | apply Veq_trans].
Qed.

Lemma Vin_respects_Veq_right : forall A B : V, Veq A B -> forall c : V, Vin c A -> Vin c B.
Proof.
  intros [X f] [Y g] [H_XY H_YX] c [x Hx].
  destruct (H_XY x) as [y Hy].
  exists y. symmetry. transitivity (f x). symmetry. apply Hx. apply Hy.
Qed.

Lemma Vin_respects_Veq_left : forall a b : V, Veq a b -> forall C : V, Vin a C -> Vin b C.
Proof.
  intros a b E [Z h] [z Hz].
  exists z. transitivity a. apply Hz. apply E.
Qed.

Theorem extensionality : forall A B : V, Veq A B <-> (forall c : V, Vin c A <-> Vin c B).
Proof.
  intros [X f] [Y g]. simpl. split.
  - intros [H_XY H_YX] c. split.
    + intros [x Hx]. destruct (H_XY x) as [y Hy].
      exists y. transitivity (f x). symmetry. apply Hy. apply Hx.
    + intros [y Hy]. destruct (H_YX y) as [x Hx].
      exists x. transitivity (g y). apply Hx. apply Hy.
  - intros H. split.
    + intros x.
      enough (exists y, Veq (g y) (f x)) as [y Hy]. { exists y. symmetry. apply Hy. }
      apply H. exists x. reflexivity.
    + intros y. apply H. exists y. reflexivity.
Qed.

Theorem replacement
  (A : V) (phi : V -> V)
  (phi_respectful : forall x x', Veq x x' -> Veq (phi x) (phi x')) :
  exists B, forall y, Vin y B <-> exists x, Vin x A /\ Veq (phi x) y.
Proof.
  Fail exists (sup V phi).
  destruct A as [X f].
  exists (sup X (fun x => phi (f x))).
  simpl. intros y. split.
  - intros [x Hx]. exists (f x). split.
    + exists x. reflexivity.
    + apply Hx.
  - intros [s [[x Hx] Hs]]. exists x.
    transitivity (phi s).
    + apply phi_respectful. apply Hx.
    + apply Hs.
Qed.

Theorem replacement
  (A : V) (phi : V -> V)
  (phi_respectful : forall x x', Veq x x' -> Veq (phi x) (phi x')) :
  exists B, forall y, Vin y B <-> exists x, Vin x A /\ Veq (phi x) y.