Cours 10: Traduction de Girard et Substitution explicite
Traduction de Girard
- $λ$-calcul simplement typé:
- \[X^G ≝ X\]
- \[(A ⇒ B)^G ≝ \; !A^G \multimap B^G\]
- \[(A ∧ B)^G ≝ \; A^G \& B^G\]
- \[(A ∨ B)^G ≝ \; !A^G \oplus !B^G\]
- \[⊥^G ≝ \; 0\]
- \[(Γ ⊢ A)^G ≝ \; !Γ^G ⊢ A^G\]
On va se concentrer sur le fragment du $λ$-calcul simplement typé.
$λ$-calcul avec duplication explicite
On met sous un bang les termes duplicables.
Grammaire
\[A, B ≝ \; X \mid A \multimap B \mid !A\\ T, U ≝ \; \overbrace{a}^{\text{var. linéaires}} \mid λa. \overbrace{T}^{a \text{ y apparaît exactement une fois}} \mid TU\\ \underbrace{x}_{\text{var. non-lin/exponentielles}} \mid !\underbrace{T}_{\text{pas de var. libre linéaire}} \mid \underbrace{T[!x := U]}_{x \text{ liée dans } T \text{ aussi noté } \texttt{let } !x= U \texttt{ in } T}\]NB: les types de la première ligne correspondent aux termes (linéaires) de la deuxième.
- Contextes de substitution:
- \[S ≝ \; \underbrace{\lbrace \bullet \rbrace}_{\text{"trou"}} \mid S[!x := U]\]
On dénote par $S \lbrace T \rbrace$ le terme obtenu en substituant $T$ à $\lbrace \bullet \rbrace$ dans $S$.
On dénote par $C$ un contexte quelconque.
NB: Attention, cette notion de substitution n’est pas sans capture !
Ex:
- $S ≝ \lbrace \bullet \rbrace[!x := U]$
-
$S \lbrace x \rbrace = x[!x := U]$
- on y a lié des variables
Réécriture
\[S \lbrace λa. T \rbrace ⟶ S \lbrace T \lbrace U/a \rbrace \rbrace \\ T[!x := S \lbrace !U \rbrace] ⟶ S \lbrace T \lbrace U/x \rbrace \rbrace\]NB: La première règle est la $β$-réduction du $λ$-calcul modulo un contexte arbitraire
Avec la notation plus intuitive :
\[\underbrace{T[\_]}_{\text{écriture plus explicite}} ≝ [\_] \lbrace T \rbrace\]Cela donne :
\[(λa. T)[\_]U ⟶ T \lbrace U/a \rbrace [\_]\\ T[!x := (!U)[\_]] ⟶ T \lbrace U / x \rbrace [\_]\]Traduction de Girard du $λ$-calcul avec duplication explicite
\[x^G ≝ \; x \\ (λx. M)^G ≝ \; λa. M^G[!x := a]\\ (MN)^G ≝ \; M^G !N^G\]Lemme:
\[(M \lbrace N / x \rbrace)^G ⟶ M^G \lbrace N^G / x \rbrace\]
Il vient que
Proprété:
\[(λx. M)N ⟶ M \lbrace N / x \rbrace\]
En effet:
\[(λx. M)N ⟶ (λa. M^G[!x := a]) !N^G ⟶ M^G [!x := !N^G] \\ ⟶ M^G \lbrace N^G /x \rbrace ⟶ (M \lbrace N/x \rbrace)^G\]NB: La logique raffine l’exécution du $λ$-calcul, par l’unique étape $(λx. M)N ⟶ M \lbrace N / x \rbrace$ a été décomposée en 2 étapes.
Séquents
On va travailler sur des séquents de la forme
\[Γ; Δ ⊢ A ≝ \; !Γ, Δ ⊢ A\]C’est-à-dire qu’on va supposer que $Γ$ est non linéaire avant le point virgule, même si ce n’est pas explicitement précisé.
Variables linéaires: Axiome
\[\cfrac{}{; a: A ⊢ a: A}ax\]Implication à droite (introduction de la flèche linéaire)
\[\cfrac{Γ; Δ, a: A ⊢ T: B}{Γ ; Δ ⊢ λa. T: A → B} \multimap I\]Elimination de la flèche linéaire
\[\cfrac{Γ; Δ ⊢ M: A → B \qquad Γ'; Δ' ⊢ N:A}{Γ, Γ' ; Δ, Δ' ⊢ MN : B} \multimap E\]Déréliction
\[\cfrac{Γ; Δ, a:A ⊢ T: C}{Γ, x:A ; Δ ⊢ T \lbrace x/a \rbrace : C} \text{ déréliction}\]Rappel:
\[\cfrac{!Γ ⊢ A}{!Γ ⊢ !A} \text{ promotion}\] \[\cfrac{Γ, A ⊢ C}{Γ, !A ⊢ C} \text{ déréliction}\]Structure:
\[\cfrac{Γ, !A, !A ⊢ C}{Γ, !A ⊢ C}\] \[\cfrac{Γ ⊢ C}{Γ, !A ⊢ C}\]Promotion
\[\cfrac{Γ; ⊢ T:A}{Γ; ⊢ !T: !A} \text{ promotion}\]Coupure
\[\cfrac{Γ; Δ ⊢ U: !A \qquad Γ', x:A; Δ' ⊢ T:C}{Γ, Γ'; Δ, Δ' ⊢ T [!x := U] : C} \; !E\]Structure
Contraction
\[\cfrac{Γ, x:A, y:A ; Δ ⊢ T: C}{Γ, x:A ; Δ ⊢ T \lbrace x/y \rbrace : C}\]Affaiblissement
\[\cfrac{Γ ; Δ ⊢ T: C}{Γ, x:A ; Δ ⊢ T : C}\]NB: On peut se passer des règles structurelles:
\[\cfrac{}{Γ ; a: A ⊢ a: A}ax\] \[\cfrac{Γ; ⋯ ⊢ ⋯ \qquad Γ; ⋯ ⊢ ⋯}{Γ ; ⋯ ⊢ ⋯} \; \multimap E / ! E\] \[\cfrac{}{Γ, x:A ; ⊢ x:A} \; \text{ déréliction}\]On dit que c’est “syntax-directed” ⟶ il y a autant de règles que de termes (chaque terme a sa règle: les variables ont la leur, etc…) ⟶ la dernière règle appliquée est toujours donnée par la structure du terme.
La traduction de Girard est bien typée
On va donner une traduction des preuves de la logique intuitionniste respectant la traduction de Girard:
\[(Γ ⊢ M: A)^G = Γ^G; ⊢ M^G: A^G\]Il y a trois règles.
Variable
\[\cfrac{}{Γ; x: A ⊢ x: A} ⟼ \cfrac{}{Γ^G, x: A^G; ⊢ x: A^G}\]$λ$ / Introduction de $⇒$
\[\cfrac{ \cfrac{Γ, x:A ⊢ M: B}{Γ ⊢ λx.M: A ⇒ B} ⟼ \cfrac{ \cfrac{}{Γ; a: !A^G ⊢ a: !A^G} \qquad Γ^G, x: A^G; ⊢ M^G: B^G }{Γ^G; a: !A^G ⊢ M^G[!x := a]: B^G}\quad !E }{ Γ^G; ⊢ λa. M^G[!x := a]: !A^G \multimap B}\]Elimination de $⇒$
\[\cfrac{Γ⊢ M: A ⇒ B \qquad Γ ⊢ N:A}{Γ ⊢ MN: B} ⟼ \cfrac{ Γ^G; ⊢ M^G: !A^G \multimap B^G \qquad \cfrac{Γ^G; ⊢ N^G: A^G}{Γ^G; ⊢ !N^G: !A^G} \; !I }{Γ^G; ⊢ M^G!N^G: B^G}\quad \; \multimap E\]Traduction de toute la logique intuitionniste
Ajout à la grammaire, pour toute la logique linéaire intuitionniste
\[\mid ⟨T, U⟩ \mid π_i T \\ \mid ι_i T \mid \texttt{ case } M \texttt{ of } ⋯ \\ \mid T \otimes U \mid T[a \otimes b := U]\\ \mid \star \mid T[\star := U]\]Substitution explicite
\[(λx. M)N ⟶ M \lbrace N/x \rbrace\]devient, en logique linéaire:
\[(λa. M[!x := a])!N ⟶ M [!x := !N] ⟶ M \lbrace N / x \rbrace\]Substitution explicite
Pour ne pas sortir de l’image de la traduction, et incoporer l’alien $M [!x := !N]$ dans la grammaire:
\[M, N ≝ \; x \mid λx. M \mid MN \mid \underbrace{M [x ← N]}_{\text{substitution explicite}}\\ a \mid λa. M[!x := a] \mid M!N \mid M[!x := !N]\]Avec les règle de réduction
\[(λx. M) [\_] N ⟶ M [x ← N] [\_]\\ M [x ← N[\_]] ⟶ M \lbrace N/x \rbrace [\_]\]Règles de réécriture de la substitution explicite
\[(λy. M)[x ← N] ⟶ λy. M[x ← N] \\ (MN)[x ← P] ⟶ M[x ← P](N [x ← P])\\ x [x ← N] ⟶ N \\ y [x ← N] ⟶ y \text{ si } y≠x\]Mais comment substituer dans une substitution explicite ?
Si on fait, naïvement:
\[M[y ← N][x ← P] ⟶ M [x ← P] [y ← N[x ← P]]\]Calcul de Beniamino Accattoli (2010)
On ne préserve plus la normalisation forte (la normalisation faible est préservée, mais pas la forte) ⟶ contre-exemple trouvé par Melliès.
Lemme de correction (préservation de la normalisation faible):
Si $M ⟶ N$ dans le $λ$-calcul, alors $M ⟶^\ast N$ avec substitution explicite.
Comment régler ce problème ? (loin d’être trivial !). La logique linéaire donne une solution élégante :
\[(λx. M) [\_] N ⟶ M [x ← N] [\_]\\ C \lbrace x \rbrace [x ← N[\_]] ⟶ C \lbrace N \rbrace [x ← N] [\_] \\ M[x ← N [\_]] ⟶ M [\_] \text{ si } x ∉ fv(M)\]où on a “atomisé” la règle
\[(λx. M)N ⟶ M \lbrace N /x \rbrace\]NB: $C \lbrace x \rbrace$ indique qu’il y a une occurrence de $x$ dans $C$ ⟹ calcul non déterministe, puisqu’on peut choisir n’importe laquelle
On garde le lemme de correction : par exemple si $M = C \lbrace x, ⋯, x \rbrace$
\[(λx. M)N ⟶ M[x ← N] ⟶ C \lbrace N, ⋯, x \rbrace [x ← N] \\ ⟶ ⋯ ⟶ M \lbrace N/x \rbrace [x ← N] ⟶ M \lbrace N/x \rbrace\]La clé est qu’on ne duplique pas la substitution explicite !
Machine de Krivine (modifiée) / Milner
L’état de la machine est donné par un triplet
\[\underbrace{M}_{λ-\text{terme}} \mid \underbrace{E}_{\text{environnement: liste de } x ← N} \mid \underbrace{S}_{\text{pile de } λ\text{-termes}}\]Réduction de tête
\[MN \mid E \mid S \overset{\text{push}}{⟶} M \mid E \mid N \cdot S \\ λx.M \mid E \mid N \cdot S \overset{\text{pop}}{⟶} M \mid E [x ← N] \mid S\\ x \mid E \mid S \overset{\text{grab}}{⟶} N^α \mid E \mid S \text{ où } [x ← N] ∈ E\]et où $N^α$ est un $α$-renommage de $N$: toutes les variables liées sont renommées par en des variables n’appartenant pas à l’environnement $E$.
NB: $E$ est un espace mémoire où on stocke la valeur des variables.
Cette machine
- fait de l’appel par noms (faible)
- ne réduit pas sous les $λ$
NB: Quand on veut exécuter un $λ$-terme, on initialise $E$ et $S$ à vide:
\[M \mid ε \mid ε\]Ex: avec $I = λy.y$
\[(λx.xx)I \mid ε \mid ε ⟶ λx.xx \mid ε \mid I\\ ⟶ xx \mid [x ← I] \mid ε \\ ⟶ x \mid [x ← I] \mid x\\ ⟶ I ≝ λy.y \mid [x ← I] \mid x \\ ⟶ y \mid [x ← I][y ← x] \mid ε \\ ⟶ x \mid [x ← I][y ← x] \mid ε \\ ⟶ λz.z \mid [x ← I][y ← x] \mid ε\]Grâce à la logique linéaire, on a trouvé une correspondant bijective entre les stratégies d’exécution et les machine abstraites comme celle-ci.
Le fait d’avoir pu décomposer la $β$-réduction en plusieurs étapes nous a donné un point de vue intéressant
- sur la manière dont s’exécute le $λ$-calcul
-
la complexité de l’exécution du $λ$-calcul
-
si on duplique les termes naïvement pendant les substitutions, la complexité explose.
-
Exemple de cas pathologique ($2^n$ termes après $n$ étapes)
- ⟹ cela donne l’impression que le $λ$-calcul n’est pas un modèle de calcul qui se comporte “raisonnablemet” (comme les machines de Turing)
-
Ex:
\[M \underbrace{\underline{w}}_{\text{mot binaire de Church}} \underbrace{⟶^\ast_h}_{\text{réduction de tête}} \underline{b} = \begin{cases} λx, y. x &&\text{ si } w \text{ appartient au langage} \\ λx, y. y &&\text{ sinon} \end{cases}\]Question: est-ce que si on a un nombre polynomial d’étapes dans la réduction de tête, le langage est dans $P$?
\[λTIME(f) ≝ \lbrace \text{ langages décidés par un } λ\text{-terme en un nombre } f(n) \text{ d'étapes de réduction de tête} \rbrace\]⟶ Pas évident, a priori, comme la réduction duplique n’importe comment !
Mais
Accattoli/Dal Lago (2012):
Il y a un slowdown polynomial !
\[\underbrace{TIME(f)}_{\text{la classe classique avec les TM}} ⊆ λ TIME(O(f))\]et, le point étonnant:
\[λ TIME(f) ⊆ TIME(poly(f))\]
Donc si on a un nombre polynomial d’étapes dans la réduction de tête, le langage est bien dans $P$ !!!
En d’autres termes:
\[λP ≝ \bigcup_{k ∈ ℕ} λ TIME(n^k)\\ ⟹ λP = P\]
c’est vrai aussi pour toutes les classes au-dessus de $P$: $λEXP = EXP$, etc…
Le $λ$-calcul a exécution explicite est plus malin, il ne duplique pas bêtement les occurrences au cours de la substitution.
NB: en 2014, on a montré que c’était aussi le cas pour les réduction gauche ! (qui calcule toutes les formes normales)
Leave a comment