Chapitre 3  Normalisation forte du λ_{σ w}-calcul

Nous avons introduit au chapitre précédent une extension du λ-calcul aux substitutions explicites: le λ_x-calcul [BR95]. Cette extension, bien qu'elle possède les propriétés de confluence et de normalisation forte, n'est pas satisfaisante en tant que modèle des langages de programmation fonctionnels. En effet, les substitutions du λ_x-calcul sont beaucoup trop simples pour être utilisées dans une implantation raisonnable du λ-calcul puisque pour chaque couple (x/t), il est nécessaire de parcourir une fois en entier l'arbre du terme dans lequel nous désirons effectuer la substitution. Ainsi, la séquence suivante de réductions est "minimale" en λ_x-calcul:

Nous présentons dans ce chapitre, la première extension du λ-calcul aux substitutions explicites: le λ_σ-calcul [ACCL90]. Ce système permet l'utilisation de substitutions correspondant à des listes de couples de la forme (x/t).

Ainsi la même substitution pourra s'effectuer comme suit en λ_σ-calcul:

Cependant, le λ_σ-calcul ne possède pas, y compris dans sa version typée que nous proposerons, la propriété de normalisation forte [Mel95].

Nous présenterons une version affaiblie de ce calcul: le λ_{σ w}-calcul [CHL96] nommé. Nous montrerons alors que ce calcul est fortement normalisant sur l'ensemble de ses expressions bien typées. Notre technique de démonstration est une adaptation d'une preuve due à Ritter [Rit94] pour le calcul avec indice de de Bruijn. L'originalité de la technique étant de remplacer le calcul λ_{σ w} par un autre calcul λ_{σ w/≡} dans lequel nous identifierons certains termes grâce à une relation de congruence. Nous montrerons tout d'abord la terminaison des expressions bien typées du λ_{σ w/≡}-calcul grâce à une extension de la technique classique de réductibilité au cas de la gestion explicite de la substitution. Informellement, nous définirons dans un premier temps les expressions dites réductibles. Nous montrerons ensuite que les expressions réductibles terminent. Puis, nous montrerons comment, à partir d'une expression bien typée e, il est possible d'obtenir une expression réductible e' contenant e. Il nous suffira de remarquer que, puisque e ' termine, il en est de même pour e. Nous pourrons enfin conclure que toute expression bien typée du λ_{σ w/≡}-calcul termine. Nous en déduirons la terminaison du λ_{σ w}-calcul par un lemme technique.

Le but pricipal de la présentation de cette preuve est de permettre au lecteur de ce document de mieux comprendre la preuve de terminaison du λ P_w-calcul proposée au chapitre 4.

3.1  Définition du formalisme λ_σ

Le λ_σ-calcul a été introduit par Abadi, Cardeli, Curien et Lévy [ACCL90] en 1990. Sa grammaire divise en deux parties mutuellement inductives l'ensemble de ses expressions: les termes et les substitutions.

Nous utiliserons dans ce chapitre les types simples induits par la grammaire de la définition 50. Ces types seront généralement notés A,B, ….

Informellement, dans l'expression ( x y) [ ( x/z ).((( z'/z ).id) ∘ id) ] , les variables libres sont y et z alors que les variables x et z' sont liées. La structure des substitutions pouvant être arbitrairement complexe, nous avons besoin de définir l'ensemble des variables liées par une substitution (dans l'exemple précédent {x,z'}) afin de pouvoir définir l'ensemble des variables libres d'une expression de la forme M [ s ] .

Comme toujours, nous travaillerons modulo α-conversion. Les deux termes suivants sont α-équivalents:

Nous sommes désormais en mesure de présenter les règles de réduction du λ_σ-calcul.

Le λ_σ-calcul est confluent:

Nous présentons à présent un système de types pour le calcul λ_σ. La principale nouveauté de ce système de types par rapport à ceux du λ-calcul et du λ_x-calcul est le fait que les substitutions doivent elles aussi être "typées". Ce typage ne se fera pas en renvoyant un type. Le type d'une substitution s dans un environnement Γ sera un environnement Γ' ce que nous noterons Γ⊢ s ▷ Γ'. Informellement, l'environnement Γ' sera l'union de l'environnement Γ et du domaine de s (enrichi de types). Il est donc nécessaire de pouvoir modifier les environnements à l'aide des substitutions.

 Preuve. La preuve de ce théorème est obtenue par induction mutuelle sur les structures de M et de s. Nous admettrons provisoirement ce théorème. En effet, cette démonstration bien que techniquement assez simple est très longue et le chapitre 4 est consacré à l'étude d'une extension du λ_σ-calcul pour lequel nous démontrons cette propriété (théorème 56). D'autre part une preuve de ce théorème peut être trouvée, pour la version originale du λ_σ-calcul, dans Explicit Substitutions [ACCL90].

---

Malheureusement, le λ_σ-calcul ne possède pas la propriété de normalisation forte. Plus précisément, il existe des λ-termes bien typés (donc, par le théorème 56, fortement normalisables pour le système →_λ ) qui ne sont pas fortement normalisables pour le système →_λσ .

 Preuve. Ce théorème est dû à Paul-André Melliès [Mel95, BG99].

---

3.2  Le calcul λ_{σ w}

Le contre-exemple de Melliès nous démontre qu'il est nécessaire de modifier les règles du λ_σ-calcul afin de pouvoir recouvrer la terminaison. L'une des solutions est de supprimer la règle (abs) ce qui conduit au λ_{σ w}-calcul. Cette solution est celle que nous adopterons dans la suite de ce chapitre. Elle présente trois avantages majeurs à nos yeux. Tout d'abord, le λ_{σ w}-calcul fournit une description plus proche des implantations des langages de programmation fonctionnels actuels qui implantent tous des stratégies faibles. Son second avantage est, tout en gardant des noms de variables, de ne plus recourir à l'α-conversion dans le système de réduction. Enfin, cette restriction présente l'avantage de permettre de recouvrer la terminaison des expressions bien typées.

Ce système est confluent [CHL96] et préserve de plus les types par réduction [ACCL90]. Nous allons maintenant prouver la normalisation forte pour ce calcul.

Le principe général de cette preuve est dû à Ritter [Rit94]. Les grandes étapes de cette preuve sont:

• Dans un premier temps, nous allons définir un nouveau calcul, le λ_{σ w/≡}-calcul, dérivé du λ_{σ w}-calcul par la transformation en égalité de trois de ces règles de calcul.
• Nous définirons alors les notions de terme et de substitution réductible dans le λ_{σ w/≡}-calcul.
• Nous montrerons alors que toute expression réductible est fortement normalisable par la relation →_{λσ w/≡} .
• Puis nous démontrerons que si s est une substitution réductible alors pour tout terme t bien typé, t [ s ] est réductible et pour toute substitution s' bien typée, s' ∘ s est réductible.
• Nous remarquerons alors que la substitution id est réductible ce dont nous déduirons que toute expression bien typée du λ_{σ w/≡}-calcul est réductible.
• Enfin, nous déduirons que toute expression bien typée du λ_{σ w}-calcul est bien typée du point précédent et d'un lemme technique.

3.3  Preuve de normalisation forte

Nous aurons besoin au cours de cette preuve de manipuler des substitutions inopérantes.

Informellement les substitutions inopérantes sont de la forme (id ∘ id) ∘ id… et ce sont les substitutions qui ne modifient pas leur environnement de typage.

 Preuve. La preuve de ce lemme est immédiate par induction sur la hauteur de la preuve du jugement Γ⊢ s ▷ Γ'.

---

Nous allons maintenant définir le calcul λ_{σ w/≡}. Ce calcul est dérivé du λ_{σ w}-calcul par la transformation de trois de ses règles de calcul en égalité.

 Preuve. Nous raisonnons par induction sur la structure de la substitution s. Par définition de la relation ≡, seuls deux cas sont possibles:

• s=id: Le résultat est alors immédiat.
• s=id ∘ s': Dans ce cas s' est, elle aussi, inopérante donc, par hypothèse d'induction, s' est fortement normalisable. Le résultat est alors immédiat par récurrence sur la longueur de la plus longue dérivation de s'.

---

Nous allons maintenant donner la définition, cruciale pour la suite de cette démonstration, d'expressions neutres. Informellement, les expressions neutres sont les expressions qui, une fois appliquées, ne créent pas de radical.

Une autre notion vitale pour notre preuve est la notion d'expression réductible.

Dans la suite de ce chapitre, nous dirons qu'une expression est réductible pour exprimer le fait que cette expression est réductible dans un environnement donné.

Nous allons maintenant démontrer que les termes réductibles sont fortement normalisables et stables par réduction. De plus, les termes neutres dont tous les réduits sont réductibles sont eux-mêmes réductibles.

 Preuve. Nous démontrons ces quatre points par induction sur le type A des expressions considérées.

• A=ι
  1. Le résultat est immédiat par définition de [[ ι]]_Γ.
  2. Soit M=(x M₁… M_n) un terme tel que Γ⊢ M : ι et tel que les M_i soient fortement normalisables. Il est évident que M est lui-même fortement normalisable et nous avons donc le résultat par définition de [[ ι]]_Γ.
  3. Soit M∈[[ ι]]_Γ et tel que M→  M'. Par le théorème 9, Γ⊢ M' : ι. De plus, il est évident que M' est fortement normalisable puisque M l'est par définition de [[ ι]]_Γ. Donc, par définition de [[ ι]]_Γ, M'∈[[ ι]]_Γ.
  4. Soit M un terme neutre tel que tous ses réduits en un pas sont dans [[ ι]]_Γ. En particulier M est fortement normalisable puisque, par définition de [[ ι]]_Γ, tous ses réduits en un pas le sont. Le résultat est alors immédiat par définition de [[ ι]]_Γ.
• A=A₁→A₂
  1. Soit M un terme appartenant à [[ A]]_Γ. Soit x une variable fraîche. Remarquons que, par hypothèse d'induction (point 2), x∈[[ A₁]]_{x : A1,Γ}. Donc, par définition de [[ A]]_Γ, nous avons ( M x)∈[[ A₂]]_{x : A1,Γ}. Ainsi, par hypothèse d'induction (point 1), le terme M x est fortement normalisable. Le résultat est alors immédiat.
  2. Soit M=(x M₁… M_n) un terme tel que Γ⊢ M : A et tel que les M_i soient fortement normalisables et soit N∈[[ A₁]]_ΔΓ. Nous savons alors que ΔΓ⊢ (x M₁… M_n N) : A₁. Par hypothèse d'induction (point 1), le terme N est fortement normalisable. Donc, par hypothèse d'induction (point 2), nous savons que (x M₁… M_n N)∈[[ A₂]]_ΔΓ ce qui est la définition de l'appartenance de M à [[ A]]_Γ.
  3. Soit M∈[[ A]]_Γ tel que M→  M' et soit N∈[[ A₁]]_ΔΓ. Par définition, nous avons M N∈[[ A₂]]_ΔΓ et donc, par hypothèse d'induction (point 3), M' N∈[[ A₂]]_ΔΓ. Le résultat est alors immédiat par définition.
  4. Soit M un terme neutre tel que Γ⊢ M : A et tel que tous ses réduits en un pas appartiennent à [[ A]]_Γ. Soit N un terme appartenant à [[ A₁]]_ΔΓ. Puisque M N est un terme neutre et puisque ΓΔ⊢ ( M N) : A₂ , il nous suffit par hypothèse d'induction (point 4) de montrer que tous les réduits en un pas de ce terme sont dans [[ A₂]]_ΓΔ pour pouvoir conclure que ( M N)∈[[ A₂]]_ΓΔ. Par hypothèse d'induction (point 1), nous savons que N est fortement normalisable. Nous allons donc raisonner par récurrence sur ν(N). Les réduits possibles en un pas de M N sont:
     • M N' où N→  N'. Dans ce cas nous avons ν(N')<ν(N) et donc le résultat est vrai par hypothèse d'induction.
     • M' N où M→  M'. Dans ce cas nous savons que M'∈[[ A]]_Γ et donc, par définition, que M' N∈[[ A₂]]_ΔΓ.
     • Il n'y a pas d'autre cas puisque M est neutre.
     Donc M N appartient à [[ A₂]]_ΔΓ, ce qui nous permet de conclure par définition de [[ A]]_Γ.

---

Bien évidement, les substitutions réductibles vérifient les mêmes propriétés.

 Preuve. Nous démontrons ces propriétés par cas sur l'environnement Δ tel que Γ⊢ s ▷ Δ.

• Δ=∅.
  1. Par le lemme 13, nous savons que Γ=∅ et que s est inopérante. Nous concluons alors par le lemme 16.
  2. Soit s∈[[ ∅]]_Γ alors, par lemme 13, nous savons que s est inopérante et que Γ=∅. Il est évidement que pour toute substitution s' telle que s→  s', s' est elle-même inopérante. Nous concluons alors grâce à la remarque 19 et au théorème 9.
  3. Ce point est évident par définition des substitutions inopérantes et par la remarque 19.
• Δ≠∅.
  1. Soit s une substitution appartenant à [[ Δ]]_Γ et (x : A)∈Δ. Par définition, nous savons que x [ s ] ∈[[ A]]_Γ. Donc par le point 1 du lemme 21, nous savons que x [ s ] est fortement normalisable. Le résultat est alors évident.
  2. Soient s une substitution appartenant à [[ Δ]]_Γ et s' telle que s→  s'. Soit (x : A)∈Δ. Par définition, nous savons que x [ s ] ∈[[ A]]_Γ. Par le point 3 du lemme 21, nous savons que x [ s' ] appartient à [[ A]]_Γ. Nous concluons alors par définition de [[ Δ]]_Γ.
  3. Soit s un substitution neutre telle que Γ⊢ s ▷ Δ et que tous ses réduits en un pas appartiennent à [[ Δ]]_Γ. Soit alors (x : A)∈Δ. Puisque s est neutre, les seuls réduits possibles en un pas de x [ s ] sont x [ s' ] (où s→  s') et x (si s=id). Dans le premier cas, nous concluons par définition de la réductibilité des substitutions (puisque s' est réductible). Le second cas est évident par le point 2 du lemme 21. Nous en déduisons que x [ s ] ∈[[ A]]_Γ. Le résultat est alors évident.

---

Grâce à ces deux lemmes fondamentaux nous allons pouvoir donner des critères syntaxiques de réductibilité.

 Preuve. Avant toute chose nous remarquons que nous avons Γ⊢ t ▷ x : A,Δ. Afin de prouver que t appartient à [[ x : A,Δ]]_Γ, il nous faut démontrer que pour tout (y : A) appartenant à x : A,Δ, nous avons y [ t ] ∈[[ B]]_Γ.

Soit (y : B)∈ x : A,Δ. Nous remarquons que y [ t ] est neutre. Donc par le point 4 du lemme 21, il nous suffit de montrer que tous ses réduits en un pas appartiennent à [[ B]]_Γ pour montrer que ce terme appartient à [[ B]]_Γ. Mais puisque M et s sont réductibles, par les lemmes 21 et 22, ces deux expressions sont fortement normalisables. Nous allons raisonner par récurrence sur ν(M)+ν(s). Les réduits en un pas possibles de y [ t ] sont:

• y [ ( x/M' ).s ] où M→  M'. Dans ce cas, nous concluons par hypothèse d'induction.
• y [ ( x/M ).s' ] où s→  s'. Dans ce cas, nous concluons par hypothèse d'induction.
• M, si x=y. Dans ce cas, nous concluons par hypothèse.
• x [ s ] , si x≠ y. Dans ce cas, nous concluons par hypothèse.

Donc y [ t ] est réductible et donc, par définition, t est réductible.

---

 Preuve. Nous remarquons tout d'abord que u est bien typée dans Δ. Pour démontrer que u est réductible, il nous suffit de montrer que pour tout (y : B) dans x : A,Δ nous avons y [ u ] ∈[[ B]]_Γ. Soit donc (y : B) appartenant à x : A,Δ. Puisque les expressions M [ t ] et s ∘ t sont réductibles, nous savons que M [ t ] et s ∘ t sont fortement normalisables par les lemmes 21 et 22. Nous allons démontrer par récurrence sur ν( M [ t ] )+ν(s ∘ t) que y [ u ] ∈[[ B]]_Γ. Puisque y [ u ] est un terme neutre, il nous suffit de démontrer que tous ses réduits en un pas sont réductibles. Les réduits possibles en un pas de ce terme sont:

• y [ (( x/M' ).s) ∘ t ] où M→  M'. Dans ce cas, nous concluons par hypothèse d'induction.
• y [ (( x/M ).s') ∘ t ] où s→  s'. Dans ce cas, nous concluons par hypothèse d'induction.
• y [ (( x/M ).s) ∘ t' ] où t→  t'. Dans ce cas, nous concluons par hypothèse d'induction
• y [ ( x/ M [ t ] ).(s ∘ t) ] . Dans ce cas, nous savons par hypothèse que M [ t ] et s ∘ t sont réductibles et donc, par le lemme 23, que ( x/ M [ t ] ).(s ∘ t) est réductibles. Nous en déduisons la réductibilité de y [ ( x/ M [ t ] ).(s ∘ t) ]

Donc y [ u ] est réductible et donc, par définition, u est réductible.

---

 Preuve. Par définition, il nous suffit de démontrer que pour tout N dans [[ A]]_ΓΔ', on a ( R N)∈[[ B]]_ΓΔ'. Soit donc un terme N∈[[ A]]_ΓΔ'. Puisque le terme R N est neutre il nous suffit, par le point 4 du lemme 21, de démontrer que tous ses réduits en un pas sont dans [[ B]]_ΓΔ'. Puisque M [ ( x/N ).s ] est réductible, ce terme est fortement normalisable. Nous allons donc raisonner par récurrence sur ν(M)+ν(N)+ν(s). Les réduits possibles en un pas de R N sont:

• (λ x : A. M') [ s ] N où M→  M'. Dans ce cas, nous concluons par hypothèse d'induction.
• (λ x : A. M) [ s' ] N où s→  s'. Dans ce cas, nous concluons par hypothèse d'induction.
• (λ x : A. M) [ s ] N' où N→  N'. Dans ce cas, nous concluons par hypothèse d'induction.
• M [ ( x/N ).s ] . Dans ce cas, nous concluons par hypothèse.

---

Nous somme désormais en mesure de démontrer que la réductibilité est "stable" par substitution et par concaténation.

 Preuve. La preuve de ce théorème est obtenue par induction sur les structures de t et M.

• Si t=id alors id ∘ s est neutre. Il nous suffit donc, pour conclure, de démontrer, par récurrence sur ν(s), que tous ses réduits en un pas sont réductibles. Ces réduits en un pas sont:
  1. [•] id ∘ s' où s→  s'. Dans ce cas, nous concluons par hypothèse de récurrence.
  2. s. Dans ce cas, nous concluons par hypothèse.
• Si M=x alors Δ n'est pas vide puisque (x : A)∈Δ. Nous concluons alors par définition de la réductibilité des substitutions.
• Si t=( x/M ).s alors, par hypothèse d'induction, nous savons que M [ t ] et s ∘ t appartiennent respectivement à [[ A]]_Γ et [[ Γ']]_Γ. Nous concluons alors grâce au lemme 24.
• Si t=v ∘ u alors nous avons deux environnements Δ' et Δ'' tels que Δ⊢ u ▷ Δ' et Δ'⊢ v ▷ Δ''. Donc, par hypothèse d'induction, nous savons que u ∘ s appartient à [[ Δ']]_Γ et donc, par hypothèse d'induction de nouveau, v ∘ (u ∘ s) appartient à [[ Δ'']]_Γ. Nous concluons alors en nous souvenant que (v ∘ u) ∘ s≡v ∘ (u ∘ s).
• Si M= N₁ N₂ alors, par hypothèse d'induction, nous savons que N₁ [ s ] et N₂ [ s ] appartiennent respectivement à [[ A₁→ A₂]]_Γ et [[ A₁]]_Γ et donc, par définition de la réductibilité, N₁ [ s ] N₂ [ s ] appartient à [[ A₂]]_Γ. Nous concluons alors en nous souvenant que N₁ [ s ] N₂ [ s ] ≡ ( N₁ N₂) [ s ] .
• Si M=λ x : A. N alors par le lemme 23 nous savons que pour tout terme N₁ appartenant à [[ A]]_ΓΔ', nous avons ( x/N ).s∈[[ x : A,Δ'Δ]]_ΓΔ'. Par hypothèse d'induction, nous avons alors M [ ( x/N ).s ] ∈[[ B]]_ΓΔ'. Nous concluons alors grâce au lemme 25.
• Si M= M [ t ] , nous savons alors, par hypothèse d'induction, que t ∘ s est réductible. Nous obtenons alors, par hypothèse d'induction de nouveau, la réductibilité de M [ s ∘ t ] . Nous concluons grâce à la définition de ≡.

---

Nous somme désormais en mesure de démontrer la normalisation forte du λ_{σ w/≡}-calcul.

 Preuve. Nous commençons par remarquer que pour tout environnement Γ la substitution id appartient à [[ Γ]]_Γ puisque Γ⊢ id ▷ Γ et id est une substitution neutre sans réduits.

Pour conclure, il nous suffit de montrer que pour tout terme M (resp. toute substitution s) bien typé, M est fortement normalisable.

Or, si M (resp. s) est bien typé alors, par le théorème 26, M [ id ] (resp. s ∘ id) est réductible et donc par le point 1 du lemme 21 (resp. le point 1 du lemme 22) le terme M [ id ] (resp. la substitution s ∘ id) est fortement normalisable. Nous en déduisons aisément le résultat.

---

Nous allons maintenant conclure ce chapitre par le résultat suivant:

 Preuve. Avant toute chose, nous remarquons que nous pouvons considérer la relation →_{λσ w}  comme étant R₁∪ R₂ où R₁ est la relation induite par les règles définissant le λ_{σ w} calcul privées de (app), (ass_env) et (clos) et où R₂ est induite par ces trois règles. Nous considérons alors O l'ensemble de λ_{σ w}-expressions, O' celui des λ_{σ w/≡}-expressions, T la congruence ≡ et R' la relation →_{λσ w/≡} . Nous concluons alors par le lemme 8 et par le théorème 27 après avoir remarqué que R₂ est fortement normalisante.

---