Chapitre 4  Le calcul λ P_w

Ce chapitre est consacré à la définition et à l'étude d'une extension du λ_{σ w}-calcul aux motifs "à la ML" et au filtrage explicite. Le système des filtres du λ P_w-calcul est inspiré des formalismes précédents dans le domaine des filtres "à la ML" [KPT96, CK99a, For02a, For02b]. Le λ P_w-calcul est, tout comme le λ_{σ w}-calcul, un calcul dit "faible". Rappelons que les calculs de substitution explicite faibles sont ceux pour lesquels il n'existe pas de règle de réécriture de la forme (λ x. M) [ s ] → λ x. ( M [ s ] ). Dans le cas du λ P_w-calcul, il ne comportera pas de règle de la forme (λ P. M) [ s ] → λ P. ( M [ s ] ) où P sera un motif "à la ML". Cette particularité nous permettra de dénoter les variables par des noms tout en n'utilisant pas l'α-conversion dans le système de réduction. Un second avantage important de cette absence sera de nous permettre de démontrer la terminaison de ce calcul.

Le but principal de l'étude explicite de la substitution est de permettre de rapprocher les calculs théoriques des implantations pratiques. Le but poursuivi par l'étude explicite du filtrage est le même. En effet, la plupart des langages de programmation  [LM92, Obj, HPJP92, Har02] et des assistants de preuve [Coq00, , Hal, ELA, Isa] modernes utilisent cette fonctionnalité non primitive dans leur base théorique actuelle.

Les principaux prédécesseurs du calcul λ P_w en matière de filtrage "à la ML" dérivent du Calculus of Pattern Matching [KPT96]. Ce calcul possédait des mécanismes de filtrage et de substitution implicites. Serenella Cerrito et Delia Kesner ont raffiné ce formalisme en proposant deux nouveaux calculs [CK99a]. Le calcul TPC possède un mécanisme de filtrage explicite et un mécanisme de substitution implicite. Le calcul TPC_ES est une extension de TPC à un système de substitution partiellement explicite. Le système de substitution de TPC_ES est fondé sur le système, très simple, de substitutions du λ_x-calcul.

L'avancée majeur du λ P_w-calcul est d'être le premier formalisme à proposer des systèmes de substitution et de filtrage complètement explicite. A l'inverse de TPC_ES, le λ P_w-calcul fonde son système de substitutions sur le λ_{σ w}-calcul. L'inconvénient d'une telle extension est la complexité très fortement accrue des concepts et des preuves de propriétés par rapport au calcul TPC_ES.

Le mécanisme de filtrage explicite du λ P_w-calcul sera obtenu par l'ajout, en plus de la β-règle classique, d'un certain nombre de règles de réécriture permettant de déconstruire les motifs jusqu'à l'obtention d'une abstraction de la forme λ x. M. Ainsi, le λ P_w-calcul comprendra une règle de réécriture de la forme:

La suite de ce chapitre sera organisée de la manière suivante. La section 4.1 sera consacrée à la définition des notions de bases du λ P_w-calcul. Nous proposerons dans cette section une grammaire pour les expressions ainsi que la démonstration de certaines propriétés de base telles que la préservation de l'ensemble des variables libres par réduction. La section 4.2 sera alors consacrée à la démonstration de la confluence du λ P_w-calcul sur l'ensemble de ses expressions en utilisant une technique due à Tait et Martin-Löf [Bar84] sur laquelle nous reviendrons dans la présentation de cette section. Nous proposerons ensuite, dans la section 4.3, un système de types avant de démontrer la préservation de types par réduction. Enfin la section 4.4 sera consacrée à la preuve de normalisation forte des expressions bien typées du λ P_w-calcul. Nous utiliserons au cours de cette démonstration une extension de la méthode de preuve dite "par réductibilité" dont nous présenterons les détails dans l'introduction de cette section.

4.1  Définition du calcul

Cette section est consacrée à la définition du calcul λ P_w. Nous présenterons tout d'abord sa grammaire dans la sous-section 4.1.1, puis, dans la sous-section 4.1.2, nous définirons formellement les notions classiques de variables libres et liées dans un terme. Nous proposerons alors des règles de réduction pour λ P_w. Nous constaterons que la notion de variables libres n'est pas assez fine car elle n'est pas préservée par réduction. La sous-section 4.1.4 sera alors consacrée à la définition de deux nouvelles notions: les variables libres localisées d'un terme et les termes acceptables. Les termes acceptables forment un sous-ensemble des termes qui préservent les variables libres d'un terme par réduction. Enfin dans la sous section 4.1.5 nous démontrerons les propriétés de préservation de l'ensemble des variables libres et de la notion de terme acceptable par réduction.

4.1.1  Grammaire

Le calcul λ P_w est une extension du λ-calcul classique. A ce titre, la nécessité d'un système de types ayant de bonnes propriétés est bien connue [Bar84]. Nous allons utiliser pour définir λ P_w un système de types simples (c.f. section 4.3).

Contrairement à la famille des λ-calculs classiques qui ne fournissent qu'un mécanisme d'abstraction sur les variables, λ P_w fournit un mécanisme d'abstraction sur des motifs complexes. Contrairement à la notion de motif du ρ-calcul [CK98], ces motifs sont définis par une grammaire indépendante de la grammaire des termes bien que partageant avec celle-ci l'ensemble des variables.

Les notations _ , x et ⟨ P, Q ⟩ sont des notations classiques. La notation @(P,Q) est une généralisation du constructeur as de OCAML. Le constructeur [ξ ∣ P,Q ] est le constructeur de motif de choix tels que ceux présents dans la construction function | P -> ... |Q -> ... de OCAML.

Les motifs seront, dans la suite de ce chapitre, dénotés par P, Q, R,…

Nous sommes maintenant en mesure de définir la grammaire des termes du calcul. Ces termes vont utiliser les motifs définis précédemment dans leur mécanisme d'abstraction. Le calcul λ P_w possédant un mécanisme explicite de substitution, nous aurons de plus besoin de définir une grammaire pour les substitutions explicites. Nous allons pour cela étendre la grammaire des substitutions de λ_σ (c.f. chapitre 3). Enfin, nous aurons besoin d'un troisième ensemble: l'ensemble de termes de choix. Ce troisième ensemble nous permettra d'évaluer de manière explicite les choix faits dans les motifs de choix.

Afin de préserver les "bonnes" propriétés de réduction pour λ P_w, nous serons, dans la sous-section 4.1.4, conduits à restreindre ces grammaires.

function 
  | P1 -> M1
  | P2 -> M2

Dans un souci de simplification des notations nous omettrons les types présents dans ces grammaires quand leur présence ne sera pas nécessaire à la compréhension.

Nous allons maintenant définir les notions de variables libres et liées d'une pré-expression.

4.1.2  Variables libres et liées

Comme toujours dans les λ-calculs utilisant des variables nommées, nous travaillerons modulo α-conversion. Nous donnons maintenant la définition formelle des variables liantes d'un motif et d'une pré-substitution par induction sur la structure de ces derniers.

A titre d'exemple, la définition précédente nous permet d'obtenir:

Nous sommes maintenant en mesure de définir les variables libres d'une pré-expression. Informellement ce sont les variables présentes dans cette expression qui ne sont pas liées dans celle-ci.

Ainsi nous avons par exemple:

4.1.3  Règles de réduction

Nous somme maintenant en mesure de définir les règles de réduction de λ P_w. Afin de faciliter la lecture de ces règles nous les avons regroupées en différents ensembles. Le premier ensemble Départ nous permet de ne pas dédoubler les règles du second, l'ensemble Filtrage, qui est l'ensemble des règles qui effectuent le filtrage d'un terme par un motif. L'ensemble Choix est l'ensemble des règles permettant d'évaluer un choix dans un terme. Les autres ensembles sont des extensions naturelles des règles du calcul λ_{σ w} (c.f. chapitre 3). Nous avons omis les types de cette présentation.

Les règles (Abs_left) et (Abs_right) justifient la présence d'un motif dans la construction de choix des substitutions. En effet, si cette construction était simplement de la forme ( ξ/K ).s, ces deux règles libéreraient les variables liées par le motif non choisi.

Considérons en effet les termes:

Nous remarquons tout d'abord que t₁—→^* t₂ et que nous avons bien FV(t₂)⊂ FV(t₁). En revanche, si nous "oublions" le motif y dans le terme t₂ et si nous considérons donc le terme t₂'=_def λ x. [ξ ∣ x,y ] [ ( ξ/L ).id ] M, nous avons alors

Nous remarquons alors que suivant ces règles, la réduction suivante est possible:

Cet exemple nous montre un premier problème: la notion de variables libres n'est dans notre cadre pas assez restrictive pour pouvoir être préservée par réduction. En effet si dans le terme λ [ξ ∣ x,y ]. [ξ ∣ y,x ] qui ne contient pas de variables libres, nous effectuons le choix L nous obtiendrons un terme de la forme λ x. y dans lequel la variable y est libre.

Afin de résoudre ce problème nous allons proposer une nouvelle notion de variable libre: les variables libres localisées.

4.1.4  Variables libres localisées et termes acceptables

L'ensemble des variables libres localisées d'une pré-expression e par rapport à une variable de choix ξ et à un choix K peut être compris informellement comme l'ensemble des variables qui resteraient libres dans e après tout remplacement de ξ par la valeur K: FV_ξ^K(e)≡ FV(e{ ξ ← K } ).

Ainsi nous avons:

 Preuve. La preuve est immédiate par induction sur l'expression e.

---

Définissons maintenant formellement la notion de pré-expression acceptable. Le rôle de la notion de pré-expression acceptable est de capturer les pré-expressions pouvant libérer des variables lors de leur réduction. Intuitivement, le pré-terme λ [ξ ∣ x,y ]. [ξ ∣ y,x ] n'est pas acceptable.

Ainsi le pré-terme λ [ξ ∣ x,y ]. [ψ ∣ x,t ] n'est pas acceptable par définition de Acc( ) pour les abstractions . En effet, FV_ξ^R([ψ ∣ x,t ])={x,t,ψ} et Var(x)={x}.

Nous allons maintenant démontrer que les variables libres (localisées) et les termes acceptables sont préservés par réduction.

4.1.5  Correction de λ P_w

Nous allons tout d'abord démontrer que les variables libres localisées sont préservées par réduction mais avant toute chose nous remarquons que:

 Preuve. Tout d'abord nous remarquons que, par α-conversion, nous pouvons supposer que ξ n'apparaît pas liée dans e. La preuve est alors faite par induction sur la structure des expressions et par cas sur la règle de réduction utilisée.

• Si e=x, e=id, e=L, e=R ou e=ξ, le résultat est immédiat puisque e ne possède pas de réduit.
• Si e=( x/M ).s ou e=( ξ^P/K' ).s, e n'étant pas réductible en tête, le résultat est immédiat par hypothèse d'induction.
• Si e=s ∘ t, 5 possibilités s'offrent à nous.
  1. Si la réduction n'a pas lieu en tête, le résultat est immédiat par la remarque 17 et par hypothèse d'induction.
  2. Si s=id et e' =t, le résultat est immédiat.
  3. Si s=( ψ^Q/K' ).u et e'=( ψ^Q/K' ).(u ∘ t), nous avons alors:

     FVξK(e) = (  FVξK(( ψQ/K'  ).u)∖ Var(t)) ⋃    FVξK(t)   = (  FVξK(u)∖ Var(t))  ⋃    FVξK(t)   =   FVξK(u ∘ t)   =   FVξK(( ψQ/K'  ).(u ∘ t))   =   FVξK(e')

  4. Si s=( x/M ).u et e'=( x/ M [ t ] ).(u ∘ t), nous avons alors:

     FVξK(e) = (  FVξK(( x/M  ).u) ∖ Var(t)) ⋃     FVξK(t)   = ((  FVξK(M) ⋃   FVξK(u))∖ Var(t))  ⋃    FVξK(t)   = (  FVξK(M)∖ Var(t)) ⋃  ((  FVξK(u)∖ Var(t))     ⋃   FVξK(t))   = (  FVξK(M)∖ Var(t)) ⋃    FVξK(u ∘ t)   =   FVξK(( x/  M [ t ]   ).(u ∘ t))   =   FVξK(e')

  5. Si s=s₁ ∘ s₂ et e'=s₁ ∘ (s₂ ∘ t), nous avons alors:

     FVξK(e) = (  FVξK(s1 ∘ s2) ∖ Var(t)) ⋃   FVξK(t)   = ⎛ ⎝ ((  FVξK(s1)∖ Var(s2))⋃   FVξK(s2) ) ∖ Var(t) ⎞ ⎠     ⋃   FVξK(t)   = ⎛ ⎝   FVξK(s1)∖ (Var(s2)⋃ Var(t)) ⎞ ⎠ ⋃     ⎛ ⎝ (  FVξK(s2) ∖ Var(t)) ⋃   FVξK(t) ⎞ ⎠   = (  FVξK(s1)∖    Var(s2 ∘ t)) ⋃   FVξK(s2 ∘ t)   =   FVξK(e')

• Si e= ξ' [ s ] , 4 possibilités s'offrent alors à nous:
  1. Si e'= ξ' [ s' ] avec s→  s', le résultat est alors immédiat par la remarque 17 et par hypothèse d'induction.
  2. Si s=id et e'=ξ' ou si s=( ξ'^Q/K' ).t et e'=K' le résultat est immédiat.
  3. Si s=( ψ^Q/K' ).t avec ψ≠ξ' et e'= ξ' [ t ] nous remarquons tout d'abord que, puisque e est acceptable nous avons:

     ∀                                 (ψ'Q'/K)∈ ( ψQ/K'  ).t, ξ' ∉Var(Q')

     Nous en déduisons en particulier que ξ'∉Var(Q) et donc que:

     FVξK(e) = ({ξ'}∖ ({ψ}⋃ Var(Q)⋃ Var(t)))  ⋃   FVξK(t)   = ({ξ'}∖        Var(t))               ⋃   FVξK(t) puisque ξ'∉{ψ}⋃Var(Q)   =   FVξK(e')

  4. Si s=( x/M ).t et e'= ξ' [ t ] nous avons:

     FVξK(e) = (ξ'∖        (Var(t)⋃ {x}))  ⋃   FVξK(( x/M  ).t)   = (ξ'∖ Var(t))   ⋃ (  FVξK(M) ⋃   FVξK(t))   ⊇ (ξ'∖ Var(t))  ⋃   FVξK(t)   =   FVξK(e')

• Si e=( M N), 8 possibilités s'offrent alors à nous:
  1. Si la réduction n'a pas lieu en tête, le résultat est immédiat par hypothèse d'induction.
  2. Si e=λ P. M₁ et e'= (λ P. M₁) [ id ] N, le résultat est immédiat.
  3. Si e= (λ ⟨ P₁, P₂ ⟩. M₁) [ s ] , N=⟨ N₁, N₂ ⟩ et e'=( (λ P₁. λ P₂. M₁) [ s ] N₁) N₂ nous remarquons que par α-conversion nous pouvons supposer que Var(s)∩ (Var(P₁)∪ Var(P₂)) = ∅ et que nous avons donc:

     FVξK(e) =   FVξK(  (λ ⟨ P1, P2 ⟩. M1) [ s ] )⋃  FVξK(⟨ N1, N2 ⟩)   = ( (  FVξK(λ ⟨ P1, P2 ⟩. M1)∖ Var(s))        ⋃         FVξK(s))       ⋃     (  FVξK(N1) ⋃   FVξK(N2))    = ((  FVξK(M1)∖     (Var(P1)⋃ Var(P2))) ∖ Var(s)) ⋃        FVξK(s) ⋃ (  FVξK(N1) ⋃   FVξK(N2))    = ((  FVξK(M1)∖      Var(P2))∖ Var(P1)) ∖ Var(s))⋃        FVξK(s) ⋃ (  FVξK(N1) ⋃   FVξK(N2))    = (((  FVξK(λ P2. M1))∖ Var(P1)) ∖ Var(s)) ⋃        FVξK(s) ⋃ (  FVξK(N1) ⋃   FVξK(N2))    = (((  FVξK(λ P1. λ P2. M1)) ∖ Var(s)) ⋃   FVξK(s)) ⋃      (  FVξK(N1) ⋃   FVξK(N2))    = ((  FVξK(  (λ P1. λ P2. M1) [ s ] ))  ⋃   FVξK(N1)) ⋃   FVξK(N2)    = (  FVξK(  (λ P1. λ P2. M1) [ s ]   N1))⋃   FVξK(N2)   = (  FVξK(  (λ P1. λ P2. M1) [ s ]   N1) N2)   =   FVξK(e')

  4. Si e= (λ @(P₁,P₂). M₁) [ s ] et e'=( (λ P₁. λ P₂. M₁) [ s ] N) N nous raisonnons comme dans le cas précédent.
  5. Si e= (λ [ψ ∣ P₁,P₂ ]. M₁) [ s ] , N=inl (N₁) et e'= (λ P₁. M₁) [ ( ψ^P₂/L ).s ] N₁ alors, une fois encore par α-conversion nous pouvons supposer que Var(s)∩ (Var(P₁)∪ Var(P₂)∪ {ψ}) = ∅, et nous avons donc:

     FVξK(e) =   FVξK(  (λ  ⎡ ⎣ ψ ∣  P1,P2   ⎤ ⎦ . M1) [ s ] )⋃   FVξK(N1)    = ((  FVξK(λ  ⎡ ⎣ ψ ∣  P1,P2   ⎤ ⎦ . M1)∖ Var(s)) ⋃   FVξK(s))     ⋃  FVξK(N1)    = (  FVξK(M1)  ∖  ({ψ}⋃ Var(P1) ⋃ Var(P2))∖ Var(s))     ⋃  FVξK(s) ⋃   FVξK(N1)    = (  FVξK(M1) ∖ Var(P1) ∖ ({ψ}⋃ Var(P2) ⋃ Var(s)))      ⋃  FVξK(s) ⋃   FVξK(N1)    = ((  FVξK(λ P1. M1)∖ ({ψ}⋃ Var(P2) ⋃ Var(s))) ⋃       FVξK(s))  ⋃    FVξK(N1)    =           FVξK(  (λ P1. M1) [ ( ψP2/L  ).s ] ) ⋃   FVξK(N1)    =   FVξK(   (λ P1. M1) [ ( ψP2/L  ).s ]  N1)   =   FVξK(e')

  6. Si e= (λ [ψ ∣ P₁,P₂ ]. M₁) [ s ] , N=inr (N₁) et e'= (λ P₂. M₁) [ ( ψ^P₁/R ).s ] N₁ nous raisonnons comme dans le cas précédent.
  7. Si M= (λ x. M₁) [ s ] et si de plus e'= M₁ [ ( x/N ).s ] , nous avons alors:

     FVξK(e) =   FVξK(  (λ x. M1) [ s ] )  ⋃     FVξK(N)   = ((  FVξK(λ x. M1)∖ Var(s))⋃   FVξK(s) )      ⋃     FVξK(N)   = (((  FVξK(M1)∖          {x})∖ Var(s))⋃   FVξK(s) )      ⋃     FVξK(N)   = (  FVξK(M1)∖ (Var(s)⋃ {x}))⋃   FVξK(s)      ⋃     FVξK(N)   =   FVξK(  M1 [ ( x/N  ).s ] )   =   FVξK(e')

  8. Si e= (λ _ . M₁) [ s ] et e'= M₁ [ s ] nous avons:

     FVξK(e) =   FVξK(  (λ  _ . M1) [ s ] )  ⋃     FVξK(N)   = ((  FVξK(λ  _ . M1)∖ Var(s))⋃   FVξK(s) )  ⋃     FVξK(N)   = (((  FVξK(M1)∖      ∅)∖ Var(s))⋃   FVξK(s) )  ⋃     FVξK(N)   ⊇ (  FVξK(M1)∖ Var(s))⋃   FVξK(s)    =   FVξK(  M1 [ s ] )   =   FVξK(e')

• Si e=⟨ M₁, M₂ ⟩, e=inl (M₁), e=inr (M₁), e=[ψ ∣ M,N ] le résultat est immédiat par hypothèse d'induction puisque e ne possède par de réduit en tête.
• Si e=[Ξ ∣ ^s M₁,M₂ ], 6 possibilités s'offrent a nous:
  1. Si la réduction n'a pas lieu en tête, le résultat est immédiat par la remarque 17 et par hypothèse d'induction.
  2. Si Ξ=L et e'= M₁ [ s ] nous avons alors:

     FVξK(e) = ((  FVξK(M1)⋃  FVξK(M2))∖ Var(s))⋃  FVξK(s)   ⊇ (  FVξK(M1)∖ Var(s))⋃  FVξK(s)   =   FVξK(e')

  3. Si Ξ=R et e'= M₂ [ s ] , nous raisonnons comme dans le cas précédent.
  4. Si K=L, Ξ=ξ et e'=[ξ ∣ M₁ [ s ] , M₂ [ s ] ] nous avons:

     FVξL(e) = (  FVξL(M1)∖Var(s))⋃  FVξL(s)   =   FVξL(  M1 [ s ] )   =   FVξL(e')

  5. Si K=R, Ξ=ξ et e'=[ξ ∣ M₁ [ s ] , M₂ [ s ] ], nous raisonnons comme dans le cas précédent.
  6. Si Ξ=ψ, ψ≠ξ et e'=[ψ ∣ M₁ [ s ] , M₂ [ s ] ] nous avons:

     FVξK(e) =   FVξK( ⎡ ⎣ ψ ∣ s  M1,M2  ⎤ ⎦ )   = ((  FVξK(M1)⋃  FVξK(M2))∖ Var(s))⋃   FVξK(s) ⋃ {ψ}   = ((  FVξK(M1)∖ Var(s))⋃   FVξK(s))⋃     ((  FVξK(M2)∖Var(s))⋃   FVξK(s)) ⋃ {ψ}   =   FVξK(  M1 [ s ] )⋃  FVξK(  M2 [ s ] )⋃{ψ}   =   FVξL(e')

• Si e=λ P. M le résultat est immédiat par hypothèse d'induction puisque e ne possède pas de réduit en tête.
• Si e= M [ s ] , 4 possibilités s'offrent alors à nous:
  1. Si la réduction n'a pas lieu en tête, le résultat est immédiat par la remarque 17 et par hypothèse d'induction.
  2. Si M= M₁ M₂ et e'= M₁ [ s ] M₂ [ s ] nous avons alors:

     FVξK(e) = (  FVξK((M1  M2))∖ Var(s)) ⋃   FVξK(s)   =         ((  FVξK(M1)⋃  FVξK(M2))∖ Var(s)) ⋃   FVξK(s)   = ((  FVξK(M1))∖    Var(s))   ⋃   FVξK(s)) ⋃     ((  FVξK(M2)∖ Var(s)) ⋃   FVξK(s))   =   FVξK(  M1 [ s ] ) ⋃   FVξK(  M1 [ s ] )   =   FVξK(e')

  3. Si M=⟨ M₁, M₂ ⟩ et e'=⟨ M₁ [ s ] , M₂ [ s ] ⟩, M=inl (M₁) et e'=inl ( M₁ [ s ] ) ou M=inr (M₁) et e'=inr ( M₁ [ s ] ), nous raisonnons comme dans le cas précédent.
  4. Si M=x, s=id et e'=x, si M=x, s=( x/N ).t et e'=N, si M=x, s=( y/N ).t, x≠ y et e'= x [ t ] , ou si M=x, s=( ψ^Q/K' ).t et e'= x [ t ] , le résultat est immédiat puisque e est acceptable.

---

De ce lemme et de la remarque 13, nous déduisons la propriété fondamentale:

 Preuve. Il suffit de prendre une variable de choix ξ n'appartenant ni à e₁ ni à e₂.

---

Afin de pouvoir ne travailler que sur des pré-expressions acceptables, il nous faut prouver la stabilité de cet ensemble par réduction.

 Preuve. Nous allons démontrer ce lemme en raisonnant par induction sur la structure de e et par cas sur la règle utilisée pour atteindre e '. Nous ne traiterons dans cette preuve ni les cas où e ne possède pas de réduit, ni les cas où la réduction ne s'effectue pas en tête d'expression. Dans ce dernier cas, nous obtenons le résultat par hypothèse d'induction et par le lemme 18.

• Si la règle utilisée est la règle (Abs_id), alors nous devons avoir e= λ P. M N donc nous savons que λ P. M et N sont acceptables. Nous en déduisons aisément que (λ P. M) [ id ] l'est aussi d'où le résultat.
• Si la règle utilisée est la règle (Abs_pair), alors e= (λ ⟨ P₁, P₂ ⟩. M) [ s ] ⟨ N₁, N₂ ⟩. Par α-conversion nous pouvons supposer que Var(s)∩ (Var(P₁)∪ Var(P₂))=∅ et nous en déduisons que :
  1. [(R1)] M, s, N₁ et N₂ sont acceptables.
  2. (λ ⟨ P₁, P₂ ⟩. M) [ s ] est acceptable d'où

     ∀ ( ξQ/K  )∈ s,           FVξK(λ ⟨ P1, P2 ⟩. M)              ⋂ Var(Q)=∅

     ou de manière équivalente

     ∀ ( ξQ/K  )∈ s,  (  FVξK(M)  ∖  (Var(P1)⋃  Var(P2))) ⋂ Var(Q)=∅   (*)

  3. λ ⟨ P₁, P₂ ⟩. M est acceptable d'où

     ∀

     ⎡ ⎣

     ξ ∣  Q1,Q2

     ⎤ ⎦

     ∈ ⟨ P1, P2 ⟩,

     ⎧ ⎪ ⎨ ⎪ ⎩

     (  FVξR(M) ⋂ Var(Q1))=∅ et           (  FVξL(M)⋂ Var(Q2)) = ∅

  Puisque N₂ est acceptable, il nous suffit de montrer que (λ P₁. λ P₂. M) [ s ] N₁ est acceptable. Puisque N₁ est acceptable, il nous suffit de montrer que (λ P₁. λ P₂. M) [ s ] est acceptable. Pour montrer ce dernier point, nous devons:

  1. Montrer que ∀ ( ξ^Q/K )∈ s,  FV_ξ^K(λ P₁. λ P₂. M) ∩ Var(Q)=∅. Or nous savons que FV_ξ^K(λ P₁. λ P₂. M)= FV_ξ^K(M) ∖ (Var(P₁) ∪ Var(P₂)) et nous obtenons le résultat par (*).
  2. Monter que λ P₁. λ P₂. M est acceptable, i.e. montrer que λ P₂. M est acceptable et que ∀ [ξ ∣ Q₁,Q₂ ]∈ P₁,  FV_ξ^R(λ P₂. M) ∩ Var(Q₁)=∅ et FV_ξ^L(λ P₂. M)∩ Var(Q₂) = ∅. Nous ne donnons ici que la preuve de ces deux dernières égalités, la preuve d'acceptabilité de λ P₂. M étant du même type. Nous remarquons que si [ξ ∣ Q₁,Q₂ ]∈ P₁ alors [ξ ∣ Q₁,Q₂ ]∈⟨ P₁, P₂ ⟩. Nous obtenons alors le résultat recherché par R3 en remarquant de plus que FV_ξ^K(λ P₂. M)⊂ FV_ξ^K(M).
• Si la règle utilisée est la règle (Abs_contr), nous raisonnons comme dans le cas précédent.
• Si la règle utilisée est la règle (Abs_left), alors e= (λ [ψ ∣ P₁,P₂ ]. M) [ s ] inl(N) d'où nous déduisons que:
  1. [(R1)] Par α-conversion, nous pouvons supposer que (Var(P₁) ∪ Var(P₂) ∪ {ψ}))∩ Var(s)=∅.
  2. M, N et s sont acceptables.
  3. (λ [ψ ∣ P₁,P₂ ]. M) [ s ] est acceptable, c'est à dire:

     ∀ ( ξQ/K  )∈ s,    FVξK(λ

     ⎡ ⎣

     ψ ∣  P1,P2

     ⎤ ⎦

     . M)⋂ Var(Q) = ∅

     ou encore

     ∀ ( ξQ/K  )∈ s,  (  FVξK(M)  ∖  (Var(P1)  ⋃  Var(P2) ⋃ {ψ}))⋂ Var(Q) = ∅

     et donc par (R1) nous obtenons:

     ∀ ( ξQ/K  )∈ s             FVξK(M) ⋂      Var(Q) = ∅      (4.1)

  4. λ [ψ ∣ P₁,P₂ ]. M est acceptable, ce que l'on peut reformuler par:

     ∀  ⎡ ⎣ ξ ∣  Q1,Q2   ⎤ ⎦ ∈  ⎡ ⎣ ψ ∣  P1,P2   ⎤ ⎦ ,    FVξR(M)⋂ Var(Q1) = ∅      (4.2)         ∀  ⎡ ⎣ ξ ∣  Q1,Q2   ⎤ ⎦ ∈  ⎡ ⎣ ψ ∣  P1,P2   ⎤ ⎦ ,          FVξL(M)⋂ Var(Q2) = ∅      (4.3)

  Ces quatre remarques étant faites nous allons maintenant pouvoir montrer que le terme e '= (λ P₁. M) [ ( ψ^P₂/L ).s ] N est un terme acceptable.

  Puisque N est acceptable, il nous suffit de montrer que (λ P₁. M) [ ( ψ^P₂/L ).s ] est acceptable, c'est à dire:

  1. ∀ ( ξ^Q/K )∈ ( ψ^P₂/L ).s, FV_ξ^K(λ P₁. M)∩ Var(Q)=∅. Soit ( ξ^Q/K )∈( ψ^P₂/L ).s, deux cas sont possibles:
     1. Si ( ξ^Q/K )∈ s, il nous faut garantir que ( FV_ξ^K(M) ∖ Var(P₁))∩Var(Q)=∅ ce qui est directement déductible de l'équation (4.1).
     2. Si ( ξ^Q/K )= ( ψ^P₂/L ), nous voulons alors montrer que ( FV_ξ^L(M) ∖ Var(P₁))∩Var(P₂)=∅ ce qui est garanti par l'équation (4.3).
  2. λ P₁. M est acceptable, ce qui est évident puisque nous savons:
     1. que M est acceptable par (R2),
     2. et que ∀ [ξ ∣ Q₁,Q₂ ]∈ P₁,  FV_ξ^R(M)∩ Var(Q₁)=∅ et FV_ξ^L(M)∩ Var(Q₂) = ∅ par les équations (4.2) et (4.3).
• Si la règle utilisée est la règle (Abs_right), nous raisonnons comme dans le cas précédent.
• Si la règle utilisée est la règle (Abs_var), nous savons alors que e= (λ x. M) [ s ] N et donc que:
  1. [(R1)] Les expressions M, s et N sont acceptables.
  2. ∀ ( ξ^Q/K )∈ s,  FV_ξ^K(λ x. M)∩ Var(Q) = ∅ et donc ∀ ( ξ^Q/K )∈ s,  ( FV_ξ^K(M)∖ {x})∩ Var(Q)=∅ et donc

     ∀   ( ξQ/K  )∈    s,      FVξK(M)⋂ Var(Q)=∅

     puisque par α-conversion nous pouvons supposer que x∉Var(s).

  Il nous faut maintenant montrer que e '= M [ ( x/N ).s ] est acceptable. A cette fin nous devons montrer que ( x/N ).s est acceptable, ce que nous faisons en nous souvenant que, par (R1), N et s sont acceptables. De même, puisque M est acceptable il nous suffit de montrer que ∀ ( ξ^Q/K )∈ ( x/N ).s FV_ξ^K(M)∩ Var(Q) = ∅ ce qui est exactement (R2).

• Si la règle utilisée est la règle (Abs_wild), le résultat est immédiat.
• Si la règle utilisée est la règle (Freeze), nous avons e= [ψ ∣ M,N ] [ s ] d'où nous déduisons que :
  1. [(R1)] s, M et N sont acceptables.
  2. ∀ ( ξ^Q/K )∈ s, FV_ξ^K([ψ ∣ M,N ])∩ Var(Q)=∅ ⇔

     ∀ ( ξ^Q/K )∈ s si ξ ≠ψ alors
     ( FV_ξ^K(M) ∪ FV_ξ^K(N)∪{ψ})∩ Var(Q) = ∅(1)

     ∀ ( ψ^Q/L )∈ s, FV_ξ^L(M)∩ Var(Q) = ∅(2)

     ∀ ( ψ^Q/R )∈ s, FV_ξ^R(N)∩ Var(Q) = ∅(3)

  Nous devons maintenant montrer que: [ ψ [ s ] ∣ ^s M,N ] est acceptable. Puisque par (R1) M, N et s sont acceptables il nous suffit de montrer que:

  • ψ [ s ] est acceptable, ce qui est vrai par (1) et ce qui implique que:

    ∀ ( ξQ/K  )∈ s, ψ∉Var(Q)

  • Si ψ∉s, nous avons Acc( M [ s ] ) et Acc( N [ s ] ).
  • Si ( ψ^Q/L )∈ s, nous avons Acc( M [ s ] ).
  • Si ( ψ^Q/R )∈ s, nous avons Acc( N [ s ] ).

  Ces trois derniers cas sont démontrés aisément par hypothèse d'induction.

• Le résultat est immédiat grâce à la définition 14 si la règle utilisée est l'une des suivantes:

  (Left)	(Right)	(Xi)	(app)
  (left)	(right)	(pair)	(var1)
  (var2)	(var3)	(var4)	(sum_var1)
  (sum_var2)	(sum_var3)	(sum_var4)	(id).

• Si la règle utilisée est la règle (clos), nous avons alors e= M [ s ] [ t ] d'où nous déduisons que
  1. [(R1)] M, s, M [ s ] et t sont acceptables.
  2. ∀ ( ξ^Q/K )∈ t,  FV_ξ^K( M [ s ] )∩ Var(Q) = ∅.
  3. ∀ ( ξ^Q/K )∈ s,  FV_ξ^K(M)∩ Var(Q) = ∅.
  Nous devons alors montrer que e '= M [ s ∘ t ] est acceptable c'est à dire:
  1. M, s, t sont acceptables ce qui est trivial par (R1).
  2. s ∘ t est acceptable c'est à dire

     ∀ ( ξQ/K  )∈ t,   FVξK(s)⋂ Var(Q) = ∅

  3. ∀ ( ξ^Q/K )∈ s ∘ t, FV_ξ^K(M)∩Var(Q) = ∅
  • Pour démontrer le second point, il nous suffit de remarquer que

    ∀                                                      K,   FVξK(  M [ s ] )=(  FVξK(M) ∖ Var(s))⋃  FVξK(s)

    nous n'avons alors plus qu'à conclure par (R2)
  • Pour démontrer le troisième point, il nous suffit de remarquer que

    ∀     ( ξQ/K  )∈ s ∘ t,   ( ξQ/K  )∈  s    ou ( ξQ/K  )∈ t

    nous pouvons alors conclure par (R1) ou (R2).
• Si la règle utilisée est la règle (ass_env), nous avons alors e=(s ∘ t) ∘ u d'où nous déduisons que:
  1. [(R1)] Par α-conversion, nous pouvons supposer que Var(t)∩Var(u)=∅.
  2. s, t et u sont acceptables.
  3. ∀ ( ξ^Q/K )∈ u,  FV_ξ^K(s ∘ t)∩ Var(Q) = ∅.
  4. ∀ ( ξ^Q/K )∈ t,  FV_ξ^K(s)∩ Var(Q) = ∅.

  Nous devons démontrer que s ∘ (t ∘ u) est acceptable c'est à dire que:

  1. s, t et u sont acceptables ce que nous obtenons par (R2).
  2. t ∘ u est acceptable c'est à dire ∀ ( ξ^Q/K )∈ u,  FV_ξ^K(t)∩ Var(Q) = ∅.
  3. ∀ ( ξ^Q/K )∈ t ∘ u,  FV_ξ^K(s)∩ Var(Q) = ∅.
  • Le second point est démontré par le fait que:

    FVξK(s ∘ t)=(  FVξK(s)∖Var(t))⋃  FVξK(t)

    et par (R3).
  • Le troisième point est démontré par le fait que:

    ∀ ( ξQ/K  )∈                        t ∘ u, ( ξQ/K  )∈       t        ou ( ξQ/K  )∈          u

    et par (R1).
• Si la règle utilisée est la règle (concat₁), nous avons alors dans ce cas e= (( x/M ).s) ∘ t ce dont nous déduisons que:
  1. [(R1)] M, s et t sont acceptables.
  2. ∀ ( ξ^Q/K )∈ t,  FV_ξ^K(( x/M ).s)∩ Var(Q) = ∅ ou de manière équivalente:

     ∀   ( ξQ/K  )∈  t,   (  FVξK(M) ⋃  FVξK(s))⋂ Var(Q) = ∅

  Il nous faut démontrer que e '=( x/ M [ t ] ).(s ∘ t) est acceptable c'est à dire que:

  1. Les expressions M, s et t sont acceptables ce qui découle triviallement de (R1).
  2. Le terme M [ t ] est acceptable ce que nous obtenons triviallement de (R2) et du fait que FV_ξ^K(M) ⊂ FV_ξ^K(( x/M ).s).
  3. s ∘ t pour lequel nous raisonnons comme dans le cas précédent.
• Si la règle utilisée est la règle (concat₂), nous raisonnons comme dans le cas d'une application de la règle concat₁.

---

Ce dernier lemme conclut notre définition de λ P_w. Nous n'utiliserons désormais que des expressions.

Nous allons dans la section suivante montrer que λ P_w est un calcul confluent sur l'ensemble des expressions.

4.2  Confluence de λ P_w

Cette section est consacrée à l'étude de la confluence de λ P_w. Nous allons utiliser pour cela une méthode utilisée pour la confluence de λ_{σ w} [CHL96]. Dans un premier temps, nous allons montrer que la relation →_es  est confluente et fortement normalisante. Nous définirons alors une nouvelle relation →_{λ Pwi}  agissant dans l'ensemble des formes normales de →_es . Puis nous montrerons la confluence de →_{λ Pwi} . Nous conclurons enfin à la confluence de →_{λ Pw}  par un lemme technique.

4.2.1  Confluence et terminaison de →_es 

La preuve de forte normalisation de →_es  est une preuve par interprétation. Cette interprétation nous a été fournie par CiME [CMMU00].

 Preuve. Il suffit de remarquer que si nous considérons la fonction I() définie ci-dessous et que nous considérons l'ordre strict >_es sur les termes défini par t₁>_es t₂ ⇔ I(t₁)>I(t₂) alors cet ordre est strictement décroissant sur les règles de →_es 

I( L)	=	0
I( R)	=	0
I( id)	=	1
I( x)	=	0
I( ξ)	=	0
I( ( x/M ).s)	=	I(M) + I(s) + 1
I( ( ξ/K ).s)	=	I(s) + 1
I( s ∘ t)	=	I(s)* I(t) + I(t) + 3*I(s) + 1
I( ξ [ s ] )	=	I(s)
I( M [ s ] )	=	I(M)*I(s) + I(s) + 3*I(M) + 1
I( inl (M))	=	I(M) + 1
I( inr (M))	=	I(M) + 1
I( ⟨ M1, M2 ⟩)	=	I(M1) + I(M2) + 1
I( M1 M2)	=	I(M1) + I(M2) + 1
I( [ξ ∣ M1,M2 ])	=	I(M1) + I(M2) + 2
I( [Ξ ∣ s M1,M2 ])	=	I(s)*(I(M1)    + I(M2) + 2) + 3*I(M2) + I(Ξ) + 3*I(M1) + 5
I()

---