Chapitre 5  Systèmes de réduction d'expressions avec motifs

Ce chapitre est consacré à la présentation et à l'étude d'un formalisme de réécriture d'ordre supérieur incorporant un système de filtrage sur des motifs "à la ML". Ce formalisme, que nous appellerons en français Systèmes de Réduction d'Expressions avec Motifs ou en anglais Expressions Reduction Systems with Patterns (ERSP), reprend globalement le principe du système de filtres utilisé pour le λ P_w-calcul (c.f. chapitre 4). Le formalisme des ERSP est une extension au filtrage du formalisme bien connu des ERSs [Kha90] et plus précisément des SERSs [BKR00].

Les ERSP peuvent aussi être considérés comme une extension à la réécriture d'ordre supérieur du λ P_w-calcul (bien que les mécanismes de substitution et de filtrage soient implicites dans ce cadre) tout comme les formalismes de réécriture d'ordre supérieur classiques [Klo80, Nip91, Kha90] peuvent être considérés comme des extensions du λ-calcul.

En tant qu'extension des ERSs, les ERSP permettent de combiner la réécriture du premier ordre et un mécanisme d'abstraction. En tant qu'extension du λ P_w-calcul, ils permettent en fait de combiner la réécriture du premier ordre et une version "implicite" du λ P_w-calcul.

De même, tout comme les ERSs permettent de redéfinir le λ-calcul, les ERSP permettent de redéfinir le λ P_w-calcul. Cette redéfinition étant par essence même au moins aussi longue que la définition présentée au chapitre 4, nous ne la proposerons pas dans cette courte introduction. En revanche, la version "implicite" du λ P_w-calcul, qui consiste en fait en une généralisation de la règle β au filtrage, est très aisément présentable. En effet, cette règle, qui d'une certaine manière peut être considérée comme un "modèle" du mécanisme de réduction à l'œuvre dans les langages de programmation fonctionnelle modernes est la suivante:

où X est une méta-variable de motif, une variable pouvant être remplacée par n'importe quel motif, et M et N sont des méta-variables de termes, des variables pouvant être remplacées par n'importe quel terme. Informellement, la β_PM-règle peut être traduite par: "Pour connaître la valeur de l'application d'une fonction (éventuellement définie par cas) λ X. M à un argument N, il suffit de connaître la valeur du terme M dans lequel le terme N a été filtré par le motif X".

Ainsi, si nous nous donnons la définition suivante pour la fonction plus sur les entiers:

nous obtiendrons la séquence de réduction suivante (dans laquelle nous identifierons les notation 3 et s(s(s(0))) pour plus de clarté).

La suite de ce chapitre sera organisée comme suit. Tout d'abord nous présenterons, dans la section 5.1, la grammaire formelle des ERSP ainsi que certaines notions de base telles que l'ensemble des variables libres d'un terme ou encore la notion de variables libres localisées d'un terme. La section 5.2 sera alors consacrée à la définition de la notion de règle de réécriture et de réduction induite par un système de réécriture et à la présentation de quelques résultats préliminaires tels que la préservation de l'ensemble des variables libres d'un terme par réduction.

La section 5.4 sera alors consacrée à la définition d'un sous ensemble des ERSP correspondant aux systèmes orthogonaux des formalismes de réécriture d'ordre supérieur classiques: les systèmes l-constructeurs orthogonaux. Ces systèmes seront à la fois orthogonaux et ne permettront le filtrage que sur des fonctions dites constructeurs qui ne peuvent être réduites. La section 5.5 est consacrée à la démonstration de la confluence, par la méthode classique de Tait et Martin-Löf [Bar84], des sytèmes l-constructeurs orthogonaux.

5.1  Définition des ERSP

Cette section est consacrée à la définition des Systèmes de Réduction d'Expressions avec Motifs (ERSP).

Nous allons tout d'abord présenter la syntaxe des ERSP. Nous définirons alors les notions de variable libre et liée dans un ERSP. Les ERSP utilisant une extension du système de filtre du λ P_w-calcul, nous aurons à nouveau besoin d'une notion de variable libre localisée qui généralise la notion classique de variable libre et de la notion de terme acceptable. Nous donnerons alors une relation réalisant le filtrage d'un terme par un motif puis nous définirons la notion de règle de réécriture dans les ERSP avant de présenter la notion de relation de réduction admissible dans notre formalisme. Informellement, la relation de réduction admissible induite par système de réécriture R sera la restriction de la notion de réécriture induite par R aux termes acceptables.

Pour présenter la grammaire des ERSP, nous avons besoin de plusieurs ensembles de variables. Tous ces ensembles sont supposés infinis dénombrables et deux à deux disjoints. Nous utiliserons dans le cadre des ERSP:

• Un ensemble UV de variables (usuelles) qui seront par la suite notées x, y, z, …
• Un ensemble CV de variables de choix qui seront par la suite notées ξ, ψ, …
• Un ensemble B de lieurs qui seront par la suite notés λ, µ, …
• Un ensemble F de symboles de fonction équipé d'une fonction ar() d'arité. Ces symboles de fonction serons notés f, g, …
• Un ensemble TV de méta-variables de termes qui serons notées M, N, …
• Enfin un ensemble PV de méta-variables de motifs qui seront notées X, Y, …

Nous utiliserons dans la suite les notations x, y,…pour dénoter indifféremment une variable usuelle, une variable de choix, une méta-variable de terme ou une méta-variable de motif.

Grâce à ces six ensembles nous pouvons présenter la grammaire des ERSP.

La fonction fibonnaci spécifiée par les équations:

fib(0)=0
fib(1)=1
fib(n+2)=fib(n)+fib(n+1)

peut ainsi être définie comme suit:

• Nous nous donnons une représentation des entiers naturel par 0 et s, deux symboles de fonction + et fib d'arité 2 (le symbole + sera noté en position infixe),
• une variable de choix ξ d'arité 3,
• un lieur λ et un symbole de fonction app d'arité 2,
• et les règles:

  app(λ X. M,N)    M{X by N}   fib(M)    app( λ  ⎡ ⎣ ξ ∣  0,s(0),s(s(x))   ⎤ ⎦ .  ⎡ ⎣ ξ ∣  0,s(0),fib(x)+fib(s(x))   ⎤ ⎦ , M)

Intuitivement, cette dernière règle défini le résultat de l'application de la fonction fib à un argument M, comme étant le résultat de l'application de M à la fonction retournant 0 si M=0, 1 si M=1 et fib(n+1)+fib(n) si M=n+2.

Comme dans le cadre du λ P_w-calcul, il nous faut définir l'ensemble des variables liées par un méta-motif.

Ainsi, nous avons:

Le méta-motif f(X,x) sera ainsi linéaire tandis que les méta-motifs f(X,X) et f(x,x) ne le seront pas.

Une position dans un méta-terme est un mot sur l'alphabet N. L'ensemble des positions d'un méta-terme T, noté Pos(T), est défini par une extension de la définition 20.

La définition de l'ensemble des positions d'un méta-filtrage peut être justifiée en considérant que informellement T₁{P by T₂} "est équivalent" quand nous raisonnons sur les positions à "app(λ P. T₁,T₂)".

Nous allons maintenant définir le sous-méta-terme à une position donnée d'un méta-terme donné. Cette définition est une extension de la définition 21.

Nous aurons besoin au cours de la preuve de confluence de la notion de position rigide.

Nous allons maintenant présenter la notion de chemin de liaison à une position p dans un méta-terme T. Informellement ce "chemin" est l'ensemble des variables et méta-variables qui se trouvent liées sur le chemin décrit par la position p depuis la racine de T.

Ainsi, si T=M{f(X,x) by µ [ξ ∣ Y,s(Y) ]. N}, nous avons:

Nous supposerons dans la suite que les différents méta-motifs se trouvant sur un même chemin de liaison d'un méta-terme ne partagent pas de méta-variables de motifs i.e. nous supposons que nous ne serons jamais dans le cas λ X. λ X. M. En revanche nous pourrons avoir un méta-terme de la forme λ f(X,X). M. Cette restriction peut être considérée comme une extension des conventions dites de Barendregt [Bar84].

Nous allons maintenant définir l'ensemble des méta-variables (libres) et des variables libres d'un méta-terme.

Ainsi si nous considérons le méta-terme suivant:

Nous aurons:

Dans tous les formalismes de réécriture d'ordre supérieur classiques existe une notion de méta-terme bien formé:

Ainsi le méta-terme T=f(u,x,M){f(X,x) by µ [ξ ∣ x,s(y) ]. g(N,t)} n'est pas bien formé puisque FV(T)={u,t} alors que le méta-terme λ [ξ ∣ x,y ]. M est, lui, bien formé.

Nous aurons de plus besoin, comme dans le cas du λ P_w-calcul du sous-ensemble des termes acceptables. En effet, si nous considérons la β_PM-règle et le terme t=app(λ [ξ ∣ x,y ]. [ξ ∣ y,x ],0), nous comprenons, bien que nous n'ayons pas encore défini la notion de réduction dans le cadre des ERSP, que la réduction t→_βPM x sera "possible" dans ce nouveau formalisme comme dans le cadre du λ P_w-calcul.

Nous présentons donc d'ores et déjà les notions de variables libres localisées d'un pré-terme et de terme acceptable.

Ainsi, FV_ξⁱ([ψ ∣ x,y,z ])={x,y,z,ψ} pour tout i et même, puisque nous travaillons modulo α-conversion:

Par cette définition, les pré-termes µ [ξ ∣ x,x ]. [ξ ∣ x,x ] et µ [ξ ∣ x,u ]. [ξ ∣ x,u ] sont acceptables alors que t=µ [ξ ∣ x,y ]. [ξ ∣ y,x ] ne l'est pas car, par exemple, FV_ξ¹([ξ ∣ y,x ])={y} et que ({y}∖{x})∩{y}≠∅.

Nous aurons de plus besoin de la notion de contexte.

Nous remarquons que la notion de pré-terme acceptable n'est pas close par pré-contexte. En effet bien que le pré-terme [ξ ∣ x,y ] soit acceptable, le pré-terme µ [ξ ∣ y,y ]. [ξ ∣ x,y ] ne l'est pas.

Nous devons maintenant définir les notions de méta-substitution et de substitution.

Nous sommes désormais en mesure définir l'opération de filtrage d'un terme par un motif. Cette opération est une opération ensembliste retournant un ensemble de substitutions. Nous donnerons dans la suite de ce chapitre un critère permettant d'assurer l'unicité de la substitution retournée.

Nous remarquons que:

• dans les trois derniers cas, { { p   by   t } } n'est défini que si  ⊔  l'est.
• Toute les substitutions de { { p   by   t } } sont bien formées puisqu'elles ne lient pas de méta-variables.
• Le non déterminisme de l'opération { {   by   } } provient uniquement du constructeur motif de choix. En d'autres termes, si aucun motif de choix n'est présent dans p, alors, sous réserve d'existence, { { p   by   t } } est unique.

L'ensemble { { [ξ ∣ 0,x ]   by   0 } } contient deux substitution {a ▷ 1 } et {a ▷ 2, x ▷ 0 }. Ceci vient du fait que le motif [ξ ∣ 0,x ] contient deux sous-motifs qui se "chevauchent".

 Preuve. Nous raisonnons par induction sur la structure du motif p.

• Si p= _ alors, par définition de { {   by   } } , nous devons avoir σ=id et le résultat est alors immédiat.
• Si p=x, par hypothèse.
• Si p=f(p₁,…,p_n) alors, par définition de { {   by   } } , nous devons avoir t=f(t₁,…,t_n) et ∀ i, { { p_i   by   t_i } } est défini. Puisque, par définition des termes acceptables, chaque t_i est acceptable, par hypothèse d'induction pour tout i, l'ensemble { { p_i   by   t_i } } est composé de substitutions acceptables. Le résultat est alors immédiat.
• Si p=@(p₁,…,p_n) ou p=[ξ ∣ p_i,…,p_n ] nous raisonnons comme dans le cas précédent.

---

Nous allons maintenant définir l'application d'une méta-substitution σ à un méta-terme T.

Afin de clarifier le fonctionnement de cette opération, considérons la méta-substitution σ=(σ_m,σ_v) où

Afin d'évaluer l'instanciation du méta-terme T=M{X by N} par σ, nous commençons par appliquer le remplacement du premier ordre

Nous appliquons alors une passe d'α-conversion et obtenons:

Nous devons alors évaluer { { [ξ ∣ x',f(z,y) ]   by   f(x,x) } } . Nous obtenons {σ₁,σ₂} où σ₁={ξ ▷ 1,x' ▷ f(x,x)} et σ₂={ξ ▷ 2,z ▷ x,y ▷ x}. Finalement nous obtenons l'ensemble:

 Preuve. Nous raisonnons par induction sur la structure du terme t.

• Si t=x, alors le résultat est immédiat par hypothèse.
• Si t=f(t₁,…,t_n) ou si t=[ξ ∣ t₁,…,t_n ], le résultat est immédiat par hypothèse d'induction.
• Si t=µ p. t' alors, par α-conversion, nous pouvons supposer que codom(σ)∩Var(p)=∅. Dès lors le résultat est immédiat par hypothèse d'induction.
• Si t=u{p by t'} alors, par α-conversion, nous pouvons supposer que codom(σ)∩Var(p). Dès lors, par hypothèse d'induction σ(t') ne contient que des termes acceptables et donc, par le lemme 20, { { p   by   t' } } ne contient que des termes acceptables. Nous en déduisons que si σ'∈{ { p   by   t' } } alors σ' ⊔ σ est acceptable par rapport à FV(u). Le résultat est alors obtenu par hypothèse d'induction.

---

5.2  Règles de réécriture et relation de réduction

Cette section définit formellement les notions de système de réécriture et de relation de réduction dans le cadre des ERSP. Nous présenterons de plus un certain nombre de résultats techniques tels que la préservation de l'ensemble des variables libres et de la notion d'acceptabilité par réduction.

La β_PM-règle, app(λ X. M,N)M{X by N}, appartient à ce formalisme. En revanche, ni M→  0, ni f(x)→  x, ni f(M)g(M,N), ni f(M)λ X. M ne sont des règles dans ce formalisme.

Afin de garantir la préservation des variables libres par réduction, nous aurons besoin de satisfaire la condition de chemin.

Nous remarquons que si σ satisfait la condition de chemin pour un méta-terme T, alors σ satisfait la condition de chemin pour tout sous-méta-terme de T.

Le contre-exemple classique à la condition de chemin est obtenu en considérant la η-règle du λ-calcul [Kha90, BKR00]. Une règle similaire mais utilisant le filtrage est la règle: λ f(X). M→  M. La méta-substitution σ={X ▷ x, M ▷ x} ne satisfait pas la condition de chemin pour M et cette règle.

Contrairement au λ P_w-calcul pour lequel nous pouvions vérifier que les règles préservaient la notion d'acceptabilité par réduction (c.f. lemme 20), nous ne pouvons ici assurer que cette notion sera préservée par réduction grâce aux règles de réécriture. Nous avons fait le choix de réduire le système de réduction induit par un système de règles plutôt que de réduire la notion de règles de réécriture. Pour cela nous introduisons maintenant la notion de méta-substitution admissible.

Quelques remarques s'imposent à ce stade. Tout d'abord, la notion d'admissibilité d'une méta-substitution σ pour une règle L→  R implique que σ(L) et σ(R) soient définis et donc en particulier dom(σ_m)⊂ MV(L).

Remarquons aussi que si L→  R est une règle et si σ est admissible pour L→  R alors σ(L) est un singleton puisque L ne contient pas d'occurrence du constructeur de méta-filtrage.

Remarquons que, bien que la relation de réduction —→^a  soit définie sur l'ensemble de tous les termes, la réduction ne peut avoir lieu que dans des sous-termes acceptables.

Avant de développer un exemple concret et complet de réduction, nous allons démontrer que la relation —→^a  préserve bien les variables libres et les termes acceptables.

 Preuve. Soit t∈σ(R). Supposons que x appartienne à FV_ξⁱ(t). Remarquons tout d'abord que, par définition des méta-termes bien formés (définition 11), x∉ FV(R). Donc x a été introduite par la méta-substitution σ. Plus précisément, il existe une méta-variable de terme M appartenant au domaine de σ telle que x∈ FV(σ M). Donc, il existe une position p_r de R telle que l'on ait:

• R∣_pr=M
• si l_pr est le chemin de liaison de R à la position p, alors x∉σ(l_pr).

Par définition des règles de réécriture, nous devons avoir M∈ FMV(L). Il existe donc un position p_l tel que L∣_pl=M. Considérons le chemin de liaison l_pl de L à la position p_l. x ne peut appartenir à l_pl puisque σ satisfait la condition de chemin pour M. Deux cas sont alors possibles:

• Si ξ∈σ l_pl alors, par la remarque 13, nous avons FV_ξⁱ(σ L)= FV(σ L). Le résultat est alors immédiat puisque x∈ FV(σ M)⊂ FV(σ L).
• Si ξ∉σ l_pl, alors par définition des règles de réécriture nous savons que ξ∉ FV(L)∪ FV(R). Nous obtenons donc x∈ FV_ξⁱ(σM)⊂ FV_aⁱ(σ L)

---

Nous déduisons de ce fait:

 Preuve. Le résultat est immédiat par induction sur la définition de la relation t₁—→^a_R t₂ et par le lemme 27.

---

 Preuve. Immédiat par le lemme 28 et la remarque 13.

---

 Preuve. Par induction sur la définition de s →_R  t et le lemme 28.

---

Nous n'utiliserons désormais, sauf mention explicite du contraire, que des termes acceptables.

Il est désormais temps de présenter un exemple concret de ERSP.

5.3  Un exemple concret

Cette section est consacrée à un exemple concret de ERSP et de réduction dans le cadre de ce formalisme. Nous allons pour cela tout d'abord définir un ERSP représentant la fonction map qui prend en entrée une fonction f et une liste l et retourne la liste composée des résultats de la fonction f appliquée aux éléments de l. Puis nous donnerons une séquence de réductions pour un terme de ce ERSP.

La fonction map peut être spécifiée en Ocaml [Obj] par le programme suivant:

type 'a liste = 
  | Vide 
  | Cons of 'a * 'a liste

let rec map(f,l) = 
  match l with 
    | Vide -> Vide
    | Cons(h,t) -> Cons(f(h),map(f,t))

Pour pouvoir encoder cette fonction dans les ERSP il nous faut donner au minimum les symboles de fonction suivants:

• Vide d'arité 0.
• Cons et map d'arité 2.

Nous nous donnons alors le système de réduction R={L→  R} suivant:

Nous enrichissons notre signature des deux symboles de fonctions Zero d'arité 0 et S d'arité 1 ce qui nous permettra d'encoder les entiers naturels dans notre système. Le terme définissant la fonction pred sur les entiers est alors:

Nous pouvons dès lors réduire le terme:

Pour cela, nous devons tout d'abord remarquer que t₁=σ(L) avec:

Donc t₁—→^a_R σ(R) si ce dernier terme est défini.

Or nous avons:

Nous devons évaluer:

ce qui nous donne:

De plus, nous avons:

Il nous faut alors calculer:

Le résultat de ce calcul est:

d'où:

Donc finalement nous avons:

Une seconde étape de réécriture nous conduit à la forme normale attendue:

5.4  Vers un ensemble d'ERSP confluents

Cette section est consacrée à l'introduction d'un sous-ensemble des ERSP, les ERSP l-constructeurs et orthogonaux, dont nous démontrerons la confluence dans la section suivante.

Intuitivement, un ERSP orthogonal est un ERSP linéaire gauche (i.e. pour chaque règle L→  R, toute méta-variable apparaît au plus une fois dans L) et non recouvrant (sans paire critique). Il est connu que les systèmes du premier ordre [BN98] et d'ordre supérieur orthogonaux [Raa96] sont confluents.

Un ERSP l-constructeur est un ERSP dans lequel l'ensemble des symboles de fonction peut être partitionné en l'ensemble des constructeurs qui ne peuvent pas être réduits (mais sur lesquels on peut filtrer) et l'ensemble des symboles définis (qui sont les symboles de tête des membres gauche des règles) et dont tout les motifs sont linéaires. La nécessité des systèmes l-constructeurs est évidente pour la confluence. En effet, considérons par exemple le système non l-constructeur suivant:

Le terme app(µ a. c,b) possède alors clairement deux réduits non joignables c et app(µ a. b,b). Ainsi R n'est donc pas confluent.

Malheureusement, les ERSP l-constructeurs orthogonaux ne sont pas confluents pour la réduction admissible. En effet nous considérons à présent le système composé uniquement de la β_PM-règle dont il est clair qu'il est tout à la fois orthogonal et l-constructeur. Le terme t=app(λ [ξ ∣ x,y ]. [ξ ∣ 0,1 ],3) possède, par —→^a_R , deux réduits 0 et 1 non joignables. La raison de ce phénomène est que le terme t contient deux motifs x et y se recouvrant mutuellement. La non confluence est, dans ce cas, totalement normale puisque le terme t correspond informellement à un système de réécriture de premier ordre "non orthogonal". Il nous faudra donc restreindre la relation de réduction induite par un ERSP.

Nous allons à présent formaliser les notions que nous venons d'introduire.

Nous allons maintenant définir les méta-motifs et les méta-termes l-constructeurs.

Si nous considérons le système R₁ défini précédemment, le méta-motif s(X) est l-constructeur alors que plus(X,Y) ne l'est pas puisque plus n'est pas un symbole constructeur de R₁.

Bien que la définition 33 dépende d'un ERSP R donné, nous ferons désormais un abus de notation en écrivant qu'un méta-motif ou un méta-terme est simplement l-constructeur sans préciser le système quand cela ne sera pas nécessaire à la compréhension.

Ainsi, dans le système R₁ de l'exemple 32, la substitution σ={X ▷ plus(0,0), M ▷ 0, N ▷ 0} n'est pas l-constructeur pour le membre droit de la β_PM-règle. En revanche la méta-substitution θ={X ▷ [ξ ∣ 0,s(x) ],M ▷ [ξ ∣ 0,x ],N ▷ plus(3,4)} est, elle, l-constructeur pour la β_PM-règle.

 Preuve. Le résultat est immédiat par induction sur la structure de p.

---

 Preuve. Nous raisonnons par induction sur la structure de t. Le seul cas non immédiat est le cas où t=t₁{p by t₂}. Dans ce cas, nous savons, par hypothèse d'induction, que σ(t₂) ne contient que des termes l-constructeurs. Soit t₂'∈σ(t₂). Par le lemme 35, nous savons que ∀σ'∈{ { p   by   t₂' } } ,∀ x∈dom(σ'), σ(x) est un terme l-constructeur. Le résultat est alors immédiat par hypothèse d'induction appliquée à t₁.

---

 Preuve. La preuve est obtenue par induction sur la structure de T. Le seul cas non immédiat est celui où T=T₁{P by T₂}. Dans ce cas nous savons que σ_m(T) est un pré-terme l-constructeur et donc, par hypothèse d'induction, que σ(T₂) ne contient que des termes l-constructeurs. De même, nous savons, par hypothèse d'induction, que σ_m(T₁) est un pré-terme l-constructeur. Nous concluons alors par le lemme 36.

---

Nous sommes maintenant en mesure de définir la réduction l-constructeur.

Ainsi, si nous considérons le système R₁ de l'exemple 32, nous avons plus(0,0)—→^c_R1  0 mais nous n'avons pas t=app(λ plus(0,0). 3,plus(0,0))—→^c_R1  3 car le terme t n'est pas l-constructeur.

 Preuve. Le résultat est immédiat par induction sur le contexte considéré dans la réduction et par le lemme 37.

---

Après avoir introduit les notions d'objet l-constructeurs, nous alons désormais définir les systèmes de réécriture orthogonaux.

Cette définition est en fait "équivalente" à l'absence de paire critique telle que présentées à la définition 37.

Ainsi, le système R₁ de l'exemple 32 est orthogonal. En revanche, si nous considérons le système:

Ce système n'est pas orthogonal puisque ces deux règles se superposent, par exemple, sur le terme µ _ . f(0).

Les motifs f( _ ,x) et f(y,g(0)) sont superposables tout comme les motifs [ξ ∣ 0,s(x) ] et 0.

Ainsi, le motif [ξ ∣ s(0),s(s(0)) ] est déterministe mais pas le motif [ξ ∣ s(0),s(_) ].

Nous remarquons que si un méta-terme est déterministe alors ses sous-méta-termes aussi.

Ainsi la méta-substitution σ={ X ▷ x,Y ▷ y} n'est pas déterministe pour le méta-terme T=µ f(X,Y). 0.

 Preuve. Le fait que { { p   by   t } } soit, sous réserve d'existence, tel que ∀σ∈{ { p   by   t } } ,∀ x∈dom(σ), σ(x) soit un terme déterministe est immédiat par induction sur p.

Il ne nous reste donc plus qu'a démontrer que, sous réserve d'existence, { { p   by   t } } est uniquement défini. Pour cela nous raisonnons une fois encore par induction sur p. Le seul cas non immédiat par hypothèse d'induction est le cas où p=[ξ ∣ p₁,…,p_n ], dans lequel nous concluons grâce au fait que p est déterministe.

---

 Preuve. Nous raisonnons par induction sur la structure de t. Le seul cas non immédiat est le cas où t=t₁{p by t₂}. Dans ce cas, nous savons que σ(t₂) est unique et déterministe. Par le lemme 47, nous savons que { { p   by   σ(t₂') } } est unique et que pour tout x appartenant à dom({ { p   by   σ(t₂') } } ), le pré-terme { { p   by   σ(t₂') } } (x) est déterministe. Le résultat est alors immédiat par hypothèse d'induction appliquée à t₁.

---

 Preuve. La preuve est obtenue par induction sur la structure de T. Le seul cas non immédiat est le cas où T=T₁{P by T₂}. Dans ce cas nous savons que σ_m(T) est un pré-terme déterministe et donc, par hypothèse d'induction, que σ(T₂) est unique et déterministe. De même, nous savons que σ_m(T₁) est un pré-terme déterministe. Nous concluons alors par le lemme 48.

---

Nous pouvons maintenant définir la relation de réduction déterministe induite par un ERSP.

Les ERSP orthogonaux préservent les termes déterministes par réduction déterministe.

 Preuve. Le fait que t soit acceptable découle de la préservation des termes acceptables par réduction admissible (lemme 30). Il ne nous reste donc plus qu'à prouver que tous les motifs apparaissant dans t sont déterministes. Pour cela nous raisonnons par induction sur la définition de s—→^d_R t.

• Si s=σ(L) et t=σ(R) pour une règle (L,R) ∈R, le résultat est immédiat par le lemme 49.
• Si s=µ p. s' et t=µ p. t' avec s'—→^d_R t' alors nous concluons par hypothèse d'induction pour les motifs apparaissant dans t' et par hypothèse sur s pour les sous motifs de p.
• Les autres cas sont immédiats par hypothèse d'induction.

---

Nous allons dans la prochaine section démontrer que les ERSP orthogonaux et l-constructeurs sont confluents.

5.5  Confluence des ERSP

Cette section est consacrée à la démonstration de la confluence de la relation —→^c,d  pour les ERSP orthogonaux et l-constructeurs. La preuve de cette propriété est obtenue par la méthode de Tait et Martin-Löf [Bar84] et peut être résumée en quatre points clés:

1. dans un premier temps, nous allons définir une relation de réduction "parallèle"  >>>^c,d_R ,
2. nous montrerons alors que  >>>^*c,d_R =—→^c,d_R^* ,
3. puis, en utilisant les termes de Takahashi [Tak89, Tak93], nous montrerons que la relation  >>>^c,d_R  est fortement confluente pour les ERSP l-constructeurs et orthogonaux,
4. nous conclurons alors en nous souvenant que la forte confluence implique la confluence.

Afin de pouvoir définir la relation  >>>^c,d , il nous faut étendre la notion de relation de réduction induite par un ERSP aux méta-substitutions.

Nous somme désormais en mesure de définir la relation >>>.

Afin de simplifier les notations, il nous arrivera désormais d'omettre le système R dans la relation parallèle.

Nous somme maintenant en mesure de donner la démonstration de  >>>^*c,d =—→^c,d* .

 Preuve. Nous raisonnons par induction sur la structure de p.

• Si p=x ou p= _ , le résultat est immédiat.
• Si p=f(p₁,…,p_n), alors, par définition de p, f est un constructeur. Par définition de { {   by   } } , nous devons avoir t=f(t₁,…,t_n) et de plus tous les { { p_i   by   t_i } } doivent être définis. Le terme t n'est pas un radical (pas plus que ses réduits successifs) puisque son symbole de tête est un constructeur. Nous devons donc obligatoirement avoir t'=f(t₁',…,t_n') où ∀ i,t_i—→^c,d* t_i'. Nous savons de plus que les p_i sont tous l-constructeurs et déterministes. Donc, par hypothèse d'induction, nous savons que tous les { { p_i   by   t_i } } sont définis et que ∀ i, { { p_i   by   t_i } } —→^c,d* { { p_i   by   t_i' } } . Montrons que { { p   by   t' } } est défini. Pour cela, il nous suffit de montrer que ⊔_i { { p_i   by   t_i' } } est défini ce qui est immédiat puisque p est linéaire par hypothèse. Dès lors le fait que { { p   by   t } } —→^c,d* { { p   by   t' } } est évident par hypothèse d'induction.
• Si p=@(p₁,…,p_n) nous raisonnons comme dans le cas précédent.
• Si p=[ξ ∣ p₁,…,p_n ], puisque p est déterministe, il existe un unique i tel que { { p_i   by   t } } soit défini et donc { { p   by   t } } ={ξ ▷ i } ⊔  { { p_i   by   t } } . Par hypothèse d'induction, nous obtenons le fait que { { p_i   by   t' } } est uniquement défini et que { { p_i   by   t } } —→^c,d* { { p_i   by   t' } } . Donc, puisque p est déterministe, nous savons que ∀ j≠ i, { { p_j   by   t' } } n'est pas défini. Nous obtenons donc l'unicité de la définition de { { p   by   t' } } .

---

Remarquons que le lemme précédent est faux si p n'est pas l-constructeur. En effet, considérons le système R={ a→  b }, le motif non linéaire p₁=f(x,x) et le motif "non constructeur" p₂=a. Alors { { f(x,x)   by   f(a,a) } } est bien défini et f(a,a)—→^c  f(a,b) mais { { f(x,x)   by   f(a,b) } } n'est pas défini. De même { { a   by   a } } est défini et a—→^c b mais { { a   by   b } } n'est pas défini.

 Preuve. Immédiat par le lemme 55 puisque, par définition, σ(P)=ρ(P).

---

Nous sommes désormais en mesure de démontrer que la réduction est "stable par application". Il nous faudra pour cela "α-convertir" certains méta-termes.

 Preuve. La condition de chemin garantit que pour toute méta-variable de terme M de T, il existe un unique ensemble de variables (usuelles et de choix) V_M tel que x∈ V_M si et seulement si x∈∪_p σ_m( PP(T,p)) où p décrit l'ensemble des positions de T telles que T∣_p=M. De même pour toute méta-variable de motif X de T, il existe un unique V_X= BV(σ_m(X)). Considérons enfin, l'ensemble A des variables (usuelles et de choix) liées dans T. Nous définissons alors un renommage de ∪_{M∈ T} V_M∪∪_{X∈ T} V_X∪ A dans un ensemble V' tel que V'∩ S=∅. Nous définissons alors T' en appliquant à T le renommage de premier ordre ρ. Enfin nous définissons σ'_m comme suit: σ'_m(X)=ρ(σ_m(X)) et σ'_m(M)=ρ(σ_m(M)).

---

 Preuve. Nous utilisons le lemme 57 pour construire σ'_m et T' à l'aide de S=dom(σ_v)∪codom(σ_v) puis nous choisissons σ'=(σ'_m,σ_v).

---