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.

À 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 SS (à 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 AS×SA ⊆ S × S, dont les paires (s1,s2)(s_1, s_2) se comprennent comme « s1s_1 est de type s2s_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 RS×S×SR ⊆ S × S × S, où la règle (s1,s2,s3)(s_1, s_2, s_3) signifie que le type produit dépendant Π(x:T)UΠ (x : T) ⋅ U (ou, en notation Coq, forall x : T, U) sera typé par la sorte s3s_3 lorsque TT et UU sont respectivement typés par les sortes s1s_1 et s2s_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 VV (infini dénombrable). On se donne :

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

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

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

La substitution de xx par vv dans uu est définie de la manière usuelle (λλ et ΠΠ lient une variable) et notée u[x:=v]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,RS, A, R est défini sur les termes par les règles de déduction suivantes, où implicitement xx désigne une variable, s,s1,s2,s3s, s_1, s_2, s_3 une sorte, et u,v,U,Vu, 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.)

Axiome :s1:s2(s1,s2)AVariable :ΓV:sΓ,x:Vx:VAffaiblissement :Γu:UΓV:sΓ,x:Vu:UApplication :Γu:Π(x:V)UΓv:VΓuv:U[x:=V]λ-abstraction :ΓΠ(x:V)U:sΓ,x:Vu:UΓλ(x:V)u:Π(x:V)UProduit deˊpendant :ΓV:s1Γ,x:VU:s2ΓΠ(x:V)U:s3(s1,s2,s3)RConversion :Γx:UΓx:VU=βV \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*} }

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

ΓV:s1Γ,x:Vu:UΓλ(x:V)u:Π(x:V)U\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 VV type dans la sorte s1s_1, et UU type dans la sorte s2s_2 sous l'hypothèse supplémentaire x:Vx : V, rien ne garantit que le produit dépendant Π(x:V)UΠ (x : V) ⋅ U soit bien typé, car il n'y a possiblement aucune règle dans RR de la forme (s1,s2,s3)(s_1, s_2, s_3) pour une troisième sorte s3s_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:YZX)(y:Y)(z:Z)xyzλ (x : Y → Z → X) (y : Y) (z : Z) ⋅ x y z

où comme d'habitude XYX → Y dénote λ(x:X)Yλ (x : X) ⋅ Y lorsque xx n'apparaît pas dans YY, 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Γ_0 := X : s, Y : s, Z : sss est une sorte quelconque. Voici la manière dont il va être typé en (YZX)YZX(Y → Z → X) → Y → Z → X (je n'ai même pas le courage de dessiner l'arbre de dérivation) :

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 uvu v dans un contexte dont la dernière variable xx n'apparaît pas dans uvu v, je peux soit typer uu et vv 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 :

Axiome :Γs1:s2(s1,s2)AVariable :Γ,x:V,Γx:VApplication :Γu:Π(x:V)UΓv:VΓuv:U[x:=V]λ-abstraction :ΓΠ(x:V)U:sΓ,x:Vu:UΓλ(x:V)u:Π(x:V)UProduit deˊpendant :ΓV:s1Γ,x:VU:s2ΓΠ(x:V)U:s3(s1,s2,s3)RConversion :Γu:UΓu:UU=βU \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⊢ 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:portnawakx:sx : s, y : \text{portnawak} ⊢ x : s, où portnawak\text{portnawak} est un terme quelconque possiblement intypable. Le précédent obligerait à typer portnawak\text{portnawak} dans l'application de la règle affaiblissement qui dérive ce jugement de x:sx:sx : s ⊢ x : s. De même, y:portnawak,x:sx:sy : \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:portnawaks:sy : \text{portnawak} ⊢ s : s' (pour une sorte ss' quelconque), et ceci ne pourrait se faire qu'à partir de la règle axiome, mais celle-ci ne dérive que s:s⊢ s : s', donc pour passer à y:portnawaks:sy : \text{portnawak} ⊢ s : s', il faut appliquer l'affaiblissement, qui à nouveau rejette portnawak\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.

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∀ 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 (λxu)v=u[x:=v]⊢ (λ 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∀ 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

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

où la notation ΓUUΓ ⊢ U ≡ U' signifie que UU et UU' 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.0 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∀ x, 0 + x = x en règles d'égalité définitionnelle comme 0+xx0 + 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) :

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!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!=101100!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.)

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).

Représentation graphique du λ-cube

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

R{(,,),(,,),(,,)}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=R' = ∅. Les seules λ-abstractions qu'on a le droit de former sont λ(x:U)vλ (x : U) ⋅ vU:U : * et v:V: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:u : U : * alors uu ne contient pas de produit dépendant (ΠΠ) tandis que UU ne contient pas de λ-abstraction ni d'application, et que si le produit dépendant Π(x:U)VΠ (x : U) ⋅ V type, alors xx ne figure nulle part dans VV. 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:U : * dans le contexte) ou des types fonction non dépendants (VU:=Π(x:V)UV → U := Π (x : V) ⋅ U), et on reconnaît le λ-calcul simplement typé et ses trois règles

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

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

Γ,x:Vu:UΓλxu:VU\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={(,,)}R' = \{(*, □, □)\}. On peut maintenant écrire Π(x:V)U:Π (x : V) ⋅ U : □V:V : * et (sous x:Vx : V) U:U : □, et en particulier VUV → UV:V : * et U: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 :

N:Z:NS:NNE:NN+:NNNP:Π(a:N)(b:N)E(+(Sa)b)(S(+ab)) \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, N,0,S,=,+ℕ, 0, S, =, + et l'axiome S(a)+b=S(a+b)S(a) + b = S(a + b). Noter que l'on ne peut pas exprimer le schéma de récurrence, qui serait

Π(P:N)PZ(Π(n:N)PnP(Sn))Π(n:N)PnΠ (P : N → *) ⋅ P Z → (Π (n : N) ⋅ P n → P (S n)) ⋅ Π (n : N) ⋅ P n

car N:=Π(n:N)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={(,,)}R' = \{(□, *, *)\}. On peut donc écrire Π(X:)UΠ (X : *) ⋅ U où (sous x:x : *) U:U : *. Par exemple, Π(X:)(Π(x:X)X)Π (X : *) ⋅ (Π (x : X) ⋅ X) devient valide et habité par λ(X:)λ(x:X)xλ (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,XX∀ 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={(,,)}R' = \{(□, □, □)\}, n'est pas si intéressante pour elle-même. Elle permet de mettre dans le contexte des choses comme C: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={(,,),(,,),(,,)}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 ».

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

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

L'inverse n'est pas vrai : si Γv:UΓ ⊢ v : U et uvu → v, alors on n'a pas forcément u:Uu : U. Ceci est déjà faux pour le λ-calcul simplement typé, par exemple en prenant u:=(λxyy)v(λxxx)u := (λ x y ⋅ y) v (λ x ⋅ x x), mais la nouveauté par rapport au λ-calcul simplement typé est que même si uu est typable, ce n'est toujours pas vrai. Par exemple, prenons u:=(λ(x:X)s2)tu := (λ (x : X) ⋅ s_2) t, où tt et XX sont des termes quelconques tels que t:X:s1t : X : s_1, et v:=s2v := s_2. À condition de disposer d'un axiome s2:s3s_2 : s_3, on a v:s3v : s_3. Mais pour avoir u:s3u : s_3, il faut typer λ(x:X)s2λ (x : X) ⋅ s_2 dans Π(x:X)s3Π (x : X) ⋅ s_3, ce qui nécessite d'avoir une règle (s1,s3,s3)(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 s4s_4 avec un autre axiome s2:s4s_2 : s_4 et une règle (sX,s4,s4)(s_X, s_4, s_4), ce qui fait typer u:s4u : s_4 et v:s3v : s_3 ainsi que v:s4v : s_4 mais pas u:s3u : s_3.

L'unicité des types n'est pas forcément vérifiée : il se peut que u:Uu : U et u:Uu : U' avec U,UU, U' non définitionnellement égaux. Par exemple, si AA contient les axiomes (s1,s2)(s_1, s_2) et (s1,s3)(s_1, s_3) avec s2s3s_2 ≠ s_3, alors s1s_1 est à la fois de type s2s_2 et de type s3s_3. Néanmoins, l'unicité des types est vérifiée pour les PTS qui sont fonctionnels, au sens où pour tout s1s_1, il existe au plus un s2s_2 tel que (s1,s2)A(s_1, s_2) ∈ A, et pour tous s1,s2s_1, s_2, il existe au plus un s3s_3 tel que (s1,s2,s3)A(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.

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.


0.

Parce que, c'est bien connu, il n'y a que les informaticiens qui savent comment sont vraiment faites les preuves mathématiques, les mathématiciens en sont complètement ignorants. Je plaisante à peine : voyez le nombre de cours de logique pour matheux qui s'en tiennent à la déduction en style de Hilbert alors qu'on connaît infiniment mieux depuis que Gentzen a inventé la déduction naturelle il y a presque 100 ans. Fin du sarcasme. Pour être plus sérieux, il est vrai que pour étudier la théorie des modèles ou la théorie des ensembles, le système de déduction n'a aucune espèce d'importance.


Commentaires

Commentaire de Gro-Tsen (3 décembre 2024 à 19:22)

« La force de Coq est comparable à celle de ZFC » → Alors, non, je ne crois vraiment pas. J'avais essayé de résumer les choses dans un vieux billet de mon blog, auquel je viens d'ailleurs d'ajouter un lien vers une réponse de Loïc Pujet sur le StackExchange des assistants de preuves qui répond à des questions analogues, et j'ajoute le disclaimer que tout ça est complètement confus et je m'y perds beaucoup (dans les résultats avec ou sans tiers exclu ou autre gimmick du même genre, sachant que le tiers exclu augmente beaucoup la force de certains systèmes de preuves mais pas de certains autres) et qu'en plus j'ai oublié des choses que j'avais comprises il y a 10 ans, mais de ce que je comprends, la force logique de Coq sans tiers exclu est plutôt comparable à diverses variations de la théorie des ensembles de Zermelo, et pas du tout de ZFC. Dans “Sets in Types, Types in Sets”, Werner obtient bien des choses comparables à ZFC, mais c'est en ajoutant des axiomes qui sont une version à peine déguisée de l'axiome de Remplacement.

Il faut bien se dire que l'axiome de Remplacement, c'est une sorte d'axiome de grand cardinal (qui, je ne sais pas pourquoi, est devenue standard) : en gros elle dit « la classe des ordinaux est un cardinal inaccessible », et c'est vraiment fort, en fait.

Je ne crois pas qu'on sache faire quoi que ce soit qui ressemble à ZFC en force logique (sans parler des différentes saveurs de grands cardinaux qu'on sait y ajouter) et qui ne soit pas essentiellement une transposition de ZFC dans des termes à peine déguisés. C'est un peu mystérieux : il n'y a que sur des fondements ensemblistes qu'on arrive à justifier des résultats arithmétiquement très forts (et qu'on pense vrais, évidemment). En tout cas, Coq est loin du compte (sauf s'il y a eu des développements que j'ignore).

Commentaire de Jean Abou Samra (4 décembre 2024 à 01:51)

Tu as raison, je vais corriger ça.

Dans “Sets in Types, Types in Sets”, Werner obtient bien des choses comparables à ZFC, mais c'est en ajoutant des axiomes qui sont une version à peine déguisée de l'axiome de Remplacement.

Je suis beaucoup moins fort que je le voudrais en théorie des ensembles, et je n'ai que très rapidement survolé le papier, donc je dis possiblement des bêtises, mais où est-ce que tu vois des axiomes qui ressemblent au remplacement ? Je ne vois que TTDAi\text{TTDA}_i et TTCAi\text{TTCA}_i page 10, qui sont des variantes de l'axiome du choix, non ? (Il sont trivialement impliqués par l'axiome du choix global tel que défini au billet précédent.)

À noter que si la force logique de Coq avec tiers exclu ou carrément avec un avatar du choix est une question intéressante en soi, en l'occurrence ça ne va rien changer parce que je parlais uniquement de complexité de la normalisation, donc on se fiche des axiomes qui peuvent être ajoutés vu qu'ils ne viennent pas avec des règles de réduction (ils cassent la canonicité).

Et au passage, j'avoue que je partage ta perplexité sur l'axiome du remplacement. Pour être honnête, autant je crois fermement à l'axiome du choix, dans une vision platonicienne assumée de la hiérarchie cumulative (même si les maths sans l'axiome du choix m'intéressent, pour des raisons analogues à celles qui rendent les maths constructives intéressantes à mes yeux bien que je croie au tiers exclu), autant je ne suis pas parfaitement sûr à 100% de croire platoniquement à l'axiome du remplacement. Quant à la logique qu'implémente Coq, je n'ai pas les idées très claires là-dessus.

Commentaire de Gro-Tsen (4 décembre 2024 à 15:43)

Ce n'est pas non plus clair pour moi pourquoi l'axiome TTDA implique Remplacement/Collection, mais Werner dit que c'est le cas (“the encoding of the following collection scheme can be proved in CIC, assuming TTDA” : comme CIC en soi n'est pas spécialement fort, c'est vraisemblablement que TTDA cache une forme de Remplacement de façon insidieuse sous le typage). Comme la preuve est renvoyée à un fichier Coq sans aucune explication supplémentaire, je n'ai pas vraiment envie de comprendre plus. Je suppose que c'est un peu comme Ensembles de Bourbaki, dont il y a une sorte de légende urbaine selon laquelle il omet l'axiome de Remplacement et est donc équivalent à la théorie des ensembles de Zermelo, alors qu'en fait le Replacement est insidieusement caché dans un des autres axiomes (Union, probablement).

Pour la force du Remplacement, notons quand même qu'IZF interprète ZF(C), donc il a la même force : si on veut bien considérer qu'IZF est constructif, la limitation n'est ainsi pas vraiment liée au problème d'être constructif ou pas mais plutôt d'être « ensembliste » ou pas. Mais c'est peut-être quand même aussi lié à la question de savoir si on peut définir correctement des ordinaux constructivement, et à ce que l'itération des ordinaux permet de faire (cf. cet article intéressant à ce sujet). Je n'ai pas les idées claires.

Commentaire de Jean Abou Samra (4 décembre 2024 à 20:36)

Page 12 du papier, je vois :

Inductive Set:Typei+1sup:A:Typei.(ASet)Set. \begin{align*} &\text{Inductive} \ \textsf{Set} : \textsf{Type}_{i+1} \coloneqq \\ &\textsf{sup} : \prod A : \textsf{Type}_i. (A → \textsf{Set}) → \textsf{Set}. \end{align*}

où il explique que sup A f\textsf{sup} \ A \ f est censé se comprendre comme l'ensemble {f(a),a:A}\{f(a), a : A\}. Ensuite, il interprète les quantificateurs de ZFC par des forall X : Set et exists X : Set. (C'est très « confusant » parce que Set est normalement autre chose en Coq, mais ce ne l'était peut-être pas à l'époque, je ne sais pas.)

On retrouve son code sur https://github.com/rocq-archive/zfc. C'est du Coq très vieux, mais ça m'a aidé à comprendre ce qu'il fait. Je me suis amusé à en refaire une partie de manière un peu différente :

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.

Je définis le type des ensembles V comme lui, l'égalité Veq entre ensembles est l'égalité extensionnelle, Vin modélise l'appartenance, et je prouve que l'égalité est une relation d'équivalence et que l'appartenance lui est compatible (toutes ces preuves sont triviales).

La forme du schéma de remplacement que je prouve est :

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.

Évidemment, comme c'est un schéma d'axiome, on ne peut pas l'encoder parfaitement en un seul théorème Coq, alors j'ai pris en hypothèse une fonction phi : V -> V : ça ne correspond à rien dans ZFC parce que l'univers VV est une classe propre, mais je pense que moralement, c'est bien ce qu'on cherche à modéliser. Si φφ est une formule ensembliste telle que x,!y,φ(x,y)∀ x, ∃! y, φ(x, y) soit prouvable dans IZF (ou CZF ? je n'ai pas le temps de regarder les différences tout de suite), alors forall x : V, exists! y : V, phi_rel x y va être prouvable en Coq pour une traduction raisonnable phi_rel : V -> V -> Prop de φφ (parce que la traduction de chaque axiome est prouvable, je l'ai fait pour l'extensionnalité, je n'ai pas le courage de faire le reste), et il faut alors une variante du choix pour passer à phi : V -> V. De plus, pour phi obtenue de cette manière, l'hypothèse phi_respectful va être prouvable grâce aux compatibilités que j'ai montrées. Tu noteras que le choix n'est nécessaire que pour passer de phi_rel à phi, et d'ailleurs il semblerait qu'on puisse en fait se contenter d'une variante du choix unique.

Maintenant, dans la preuve de replacement, j'ai laissé au début Fail exists (sup V phi). pour montrer, comme on peut s'y attendre, définir « B{φ(x),xV}B \coloneqq \{φ(x), x ∈ V\} » ne marche pas pour cause d'univers (car V vit un univers au-dessus que l'argument de son constructeur). Sauf que comme l'ensemble A est représenté par un type « support » X et une fonction f : X -> V, on peut réutiliser ce support X en composant juste f par phi, et le reste est trivial.

Ma conclusion, c'est que je ne trouve pas que TTDA cache insidieusement une forme de remplacement, et j'ai plutôt l'impression que c'est la possibilité de définir ce type inductif V qui est puissante. Loïc Pujet dit que CCω se trouve strictement entre Z et ZF, mais ici on parle de CICω, et j'en déduis que CICω doit être nettement plus fort que CCω, whatever that means.

Commentaire de Jean Abou Samra (5 décembre 2024 à 02:25)

En fait, le HoTT Book fait précisément ce que j'ai fait ci-dessus, cf. théorème 10.5.8 (dans sa version courante à ce jour, first-edition-15-ge428abf).

Laisser un commentaire