La réécriture est utilisée depuis l'antiquité, bien que nos ancêtres en aient fait sans le savoir, mais son étude formelle ne date que du vingtième siècle. Elle comprend des aspects pratiques et théoriques.
Nous illustrons ici l'aspect pratique de la réécriture à l'aide de quelques exemples élémentaires. L'utilisation la plus courante de la réécriture est la fonction Rechercher/Remplacer présente dans tout "bon" éditeur de texte. Cette fonction permet de décrire un système de réécriture très simple qui remplace (réécrit) le mot à rechercher par celui donné comme remplaçant. Un deuxième exemple est celui de la classe des logiciels dits compilateurs qui réécrivent les programmes d'un formalisme dans un autre.
Remarquons que toute personne pratique quotidiennement la réécriture lorsqu'elle effectue des calculs. Si nous désirons connaître la valeur de 12*3 + 4*4, nous commençons par évaluer les expressions 12*3 et 4*4 puis nous remplaçons ces expressions par leurs valeurs respectives, obtenant ainsi 36+16, avant d'évaluer cette dernière expression et de trouver 52. L'opération consistant à remplacer l'expression 12*3 par sa valeur 36 est l'application de la règle de réécriture 12*3→ 36 à l'expression 12*3 + 4*4.
Mais la réécriture n'est pas seulement un outil pratique, c'est aussi (et avant tout pour nous) un outil théorique tant dans le domaine de l'informatique (modélisation de programmes ou de langages de programmation) que dans celui de la logique mathématique formelle. L'étude des propriétés des systèmes de réécriture forme un domaine très important depuis de nombreuses années. Parmi les propriétés les plus étudiées et les plus importantes des systèmes de réécriture se trouvent la terminaison qui assure l'existence d'un résultat à un calcul et la confluence qui nous permet de garantir l'unicité de ce résultat. Ainsi, dans le cas du système de réécriture:
| R = | ⎧ ⎪ ⎨ ⎪ ⎩ |
|
La terminaison de ce système garantit que, pour toute expression arithmétique, on ne peut effectuer qu'un nombre fini d'opérations. Il existe cependant deux manières de conduire les calculs pour obtenir 52 à partir de l'expression 12*3 + 4*4 à l'aide du système R. Nous pouvons obtenir la séquence de réduction 12*3 + 4*4→ 36 + 4*4→ 36+16 → 52 ou bien la séquence 12*3 + 4*4→ 12*3 + 16→ 36+16 → 52. La confluence garantit que, quelle que soit la manière de conduire les calculs, nous obtiendrons bien le même résultat.
Toutefois ces deux propriétés sont dites indécidables [Göd31]: il n'est pas possible de trouver un algorithme prenant en entrée un système de réécriture et rendant vrai si et seulement si ce système termine sur toute expression, ou conflue sur toute expression dans le second cas. L'un des enjeux de l'étude des systèmes de réécriture devient alors la recherche de critères simples à vérifier, dans notre cas syntaxiques, permettant de garantir ces propriétés.
La réécriture du premier ordre permet de modéliser les programmes tandis que celle d'ordre supérieur modélise les outils de manipulation de programmes. En conséquence, l'étude de la réécriture du premier ordre est relativement plus simple que celle de la réécriture d'ordre supérieur.
Ainsi, il nous sera possible d'exprimer le fait que le résultat de la somme de 0 et d'un entier n est l'entier n à l'aide de la règle de réécriture du premier ordre:
| plus(0,n)→ n |
Pour appliquer cette règle à l'expression plus(0,3) nous filtrons son membre gauche avec cette expression, et nous obtenons en particulier la valeur 3 pour la variable n, puis nous remplaçons la variable n de son membre droit par sa valeur obtenant ainsi le résultat 3.
Il nous sera en revanche impossible de manipuler la fonction plus comme argument ou résultat d'une autre fonction à l'intérieur du formalisme lui-même.
Les formalismes d'ordre supérieur tirent leur nom de la possibilité donnée à leur utilisateur de manipuler des fonctions d'ordre supérieur: des fonctions prenant en argument d'autres fonctions ou rendant des fonctions comme résultat.
Parmi les formalismes de réécriture d'ordre supérieur, le λ-calcul [Chu41, Bar84] est sans doute le plus connu, le plus ancien et le plus simple. C'est un formalisme très simple car il ne comporte qu'un très petit nombre de règles de syntaxe (de moyens de former des expressions) et une seule règle de réécriture. C'est un formalisme très puissant puisque il permet de représenter toutes les fonctions calculables par un ordinateur. La syntaxe du λ-calcul est composée d'un ensemble de variables que nous noterons par la suite f,g,x,y,z,… Les abstractions, que nous noterons λ x. t où x est une variable qui sera dite liée dans le terme t appelé corps de la fonction, nous permettront de définir des fonctions. Comme en mathématiques, les variables liées sont muettes. Cela signifie que, par exemple, les termes λ f. λ x. f(x) et λ g. λ y. g(y) désignent la même fonction (il seront dits α-équivalents). Enfin l'application (d'une fonction à son argument) notée par la suite ( f u) ou, quand la confusion ne sera pas possible, f u sera elle aussi une construction du λ-calcul. L'unique règle de réécriture du λ-calcul est la règle β (ou β-règle) qui nous permet de calculer le résultat de l'application d'une fonction à son argument:
| (λ x. f) u→β f{ x ← u } |
où l'opération f{ x ← u } est le remplacement, dont nous précisons le mécanisme au paragraphe suivant, des occurrences de la variable x par le terme u dans le corps f.
Nous venons d'évoquer le problème du remplacement des variables par des termes. Ce problème est particulièrement sensible pour les systèmes de réécriture d'ordre supérieur. Le remplacement pure et simple des occurrences d'une variable par un terme, comme il est effectué en réécriture du premier ordre, n'est pas une solution acceptable. En effet, considérons la fonction f=defλ x. λ x. x qui est α-équivalente à la fonction g=defλ x. λ y. y. Si nous appliquons la fonction f à un argument M, nous obtenons, grâce à la β-règle: (λ x. x){ x ← M } . Si maintenant nous effectuons un remplacement de la variable x par le terme M dans le terme λ x. x, nous obtenons λ x. M. Si nous effectuons la même suite d'opérations à l'aide de la fonction g, nous obtenons en revanche λ y. y. Il est évident que, sauf dans le cas spécifique où le terme M est égal à la variable x, les termes λ y. y et λ x. M ne désignent pas la même fonction. L'application de M à deux termes f et g désignant la même fonction conduit à deux termes ne désignant pas le même objet! Cet exemple montre qu'il est nécessaire en réécriture d'ordre supérieur de ne pas effectuer de remplacement de variables mais de substituer des variables libres (non muettes). La substitution en λ-calcul se définit par:
|
où FV(M) désigne l'ensemble des variables libres de M.
Cette opération de substitution ne fait pas partie du formalisme du λ-calcul lui-même: elle reste au niveau méta-théorique (ou implicite). Ainsi par exemple, la notation (λ y. ( x z)){ x ← t } n'appartient pas à la syntaxe du λ-calcul mais désigne le terme λ y. ( t z) (en supposant y∉ FV(t)). Cependant, puisque les formalismes de réécriture d'ordre supérieur sont, comme nous l'avons déjà mentionné, des modèles théoriques des langages de programmation, l'aspect "magique" de la gestion implicite des substitutions ne peut être considéré comme acceptable: il ne suffit pas de décréter théoriquement que deux expressions sont égales pour en "convaincre" un ordinateur. Il est nécessaire de rendre "explicite" la gestion de la substitution au moment de l'implantation. Cette constatation a conduit à l'intégration du mécanisme de substitution dans les formalismes de réécriture d'ordre supérieur. Ces formalismes permettent ainsi de traiter la substitution de manière explicite (à l'intérieur du formalisme). Il nous faut pour cela créer une nouvelle forme d'expression, notée dans notre exemple (λ y. x z) [ x/t ] , qui devient alors un terme du calcul, et donner des règles de réduction pour de telles expressions qui nous permettront d'effectuer à l'intérieur du formalisme les substitutions désirées. Ainsi par exemple nous obtiendrons le terme λ y. t à partir du terme (λ y. ( x z)) [ x/t ] par la séquence de réductions suivante:
| (λ y. ( x z)) [ x/t ] → | propagation de la substitution |
| λ y. ( x [ x/t ] z [ x/t ] )→ | substitution de la variable x |
| λ y. ( t z [ x/t ] )→ | substitution de la variable z |
| λ y. ( t z) |
Des solutions de gestion explicite de la substitution sont adoptées dans de nombreux calculs tels que le λx-calcul [BR95], le λυ-calcul [BBLRD96], le λσ-calcul [ACCL90] ou encore le λl-calcul [DG01].
L'apparition de formalismes de réécriture traitant de manière explicite le mécanisme de substitution a conduit à la découverte d'un phénomène étonnant par Paul-André Melliès [Mel95]: le fait de rendre explicite la gestion de la substitution peut briser la terminaison des calculs. Ainsi, une expression qui possède la propriété de terminaison dans une version d'un système de réécriture d'ordre supérieur traitant la substitution de manière implicite peut ne plus posséder cette propriété dans une seconde version de ce même système traitant le mécanisme de substitution de manière explicite. En d'autres termes, le mécanisme de substitution est, en fait, beaucoup plus complexe que le simple remplacement de variables (libres) par des termes.
Bien que le λ-calcul soit le plus ancien et le mieux compris des formalismes de réécriture d'ordre supérieur, sa trop grande "simplicité" rend l'expression de fonctions usuelles très complexe. En effet, il est impossible en λ-calcul d'utiliser de manière explicite les nombreux avantages de la réécriture du premier ordre tels que la manipulation de symboles de fonction et la définition de nouvelles règles de réécriture. Ainsi considérons, par exemple, la fonction map qui prend en entrée une fonction f et une liste d'éléments l, et qui renvoie la liste formée des éléments de l auxquels la fonction f a été appliquée. Il nous faudra pour cela donner une expression définissant la liste vide nil et une définissant le constructeur cons, ces deux symboles ne faisant pas partie de la grammaire du λ-calcul. Ce problème spécifique du λ-calcul a conduit à la mise au point et à l'utilisation de systèmes de réécriture d'ordre supérieur [Klo80, Klo90, Kha90, Nip91, BKR00]. Le trait commun à tous ces systèmes est la possibilité de manipuler à la fois des abstractions comme en λ-calcul et, à l'aide de nouvelles règles de réécriture, des symboles de fonctions.
Le formalisme des Combinatory Reduction Systems [Klo80] (CRS) a été le premier à combiner à la fois le λ-calcul et la réécriture du premier ordre. Plusieurs années plus tard, Tobias Nipkow [Nip91] a présenté les Higher-Order Rewrite systems (HRS) afin de donner un fondement théorique à l'assistant de preuve Isabelle [Isa] et au langage de programmation λProlog [NM88]. Femke van Raamsdonk et Vincent van Oostrom ont démontré [OR93a, OR93b] que les formalismes des CRS et des PRS (Pattern Rewrite Systems), qui sont une restriction des HRS, étaient similaires, en proposant deux simulations (CRS par PRS et inversement). Parallèlement à ces deux formalismes, Zurab Khasidashvili a proposé [Kha90] les ERS (Expression Reduction Systems). La différence principale entre les CRS et les ERS réside dans leur syntaxe. Les ERS correspondent à la famille des PRS pour lesquels il existe des résultats de confluence [MN98].
Tous ces formalismes peuvent être considérés comme des extensions du λ-calcul en cela qu'ils empruntent au λ-calcul son mécanisme de liaison.
Afin de redéfinir le λ-calcul dans le cadre des CRS, il nous faut donner deux symboles de fonction, app et lambda et la règle:
| app(lambda([x]Z(x)),Z')→ Z(Z') (Bêta) |
L'unique mécanisme de liaison des CRS est noté [x]t où t est un terme. On utilise la notation Z pour dénoter une métavariable de terme (un terme spécial pouvant être remplacé par n'importe quel terme) dans lequel la variable x peut être libre. L'inconvénient majeur des CRS est ici bien visible: cette "β-règle" est syntaxiquement bien éloignée de sa présentation classique: (λ x. Z) Z'→ Z{ x ← Z' } . Ce phénomène vient de la nécessité de déclarer les variables pouvant être libres dans les termes d'une part et de l'impossibilité de définir de nouveaux lieurs ayant chacun un comportement propre d'autre part. Pourtant de nombreux formalismes utilisent plusieurs sortes de lieurs: les formalismes de substitutions explicites (abstractions et substitutions), le λµ-calcul [Par91] ou le λΔ-calcul [RS94]…
En ce sens, la syntaxe des ERS est beaucoup plus agréable. Ainsi, pour représenter le λ-calcul à l'aide des ERS il nous faut donner un symbole de fonction app et un lieur lambda. La β-règle devient alors:
| app(lambda(x,Z),Z') → Z{ x ← Z' } |
La fonction map peut s'exprimer dans le cadre des ERS comme suit:
|
où nil représente la liste vide et cons(H,T) représente la liste composée de l'élément H et des éléments de la liste T.
Cependant tous ces formalismes de réécriture d'ordre supérieur ne prennent pas en compte un phénomène relativement nouveau des langages de programmation: la définition de fonctions par cas et le filtrage. Nous reviendrons sur ce point, crucial dans la suite de ce document, au paragraphe Filtrage et définition de fonctions par cas après avoir présenté rapidement la notion de typage et le problème de la cohérence des données.
Une fonction n'est pas uniquement définie par un algorithme (ou par des règles de réécriture): il est aussi nécessaire de préciser son domaine de définition, le domaine auquel doivent appartenir ses arguments, et son codomaine, celui auquel appartiennent ses valeurs. Par exemple, nous avons précisé lors de la spécification informelle de la fonction map que ses arguments étaient respectivement une fonction et une liste et que ses résultats étaient des listes. Cependant, il nous est encore à présent parfaitement possible d'écrire, dans les formalismes d'ordre supérieur tels que nous les avons présentés, un terme de la forme map(S(0),0) qui n'a, bien évidement, pas de sens et donc ne devrait pas pouvoir être écrit ou du moins devrait être aisément reconnaissable comme incorrect. De plus, la trop grande puissance du λ-calcul, et donc des formalismes de réécriture d'ordre supérieur, permet de définir des "fonctions" n'ayant pas d'interprétation "ensembliste". Ainsi le λ-terme Ω=defλ f. (f f) est un terme syntaxiquement bien formé du λ-calcul. Cependant, ce terme bien que formellement bien construit, n'est pas une "bonne" expression. En effet, essayons de trouver une interprétation de Ω en termes mathématiques: puisque Ω est une fonction, cette fonction doit être une fonction d'un ensemble E dans un ensemble F. Or l'argument f de Ω est appliqué à lui-même d'où nous pouvons déduire deux faits: les deux ensembles E et F sont les mêmes et f est à la fois une fonction de E dans E et un élément de E. La fonction Ω est donc une fonction d'un ensemble E qui vérifie la propriété d'être égale à l'ensemble de ses fonctions. Or il est connu qu'un tel ensemble n'existe pas. Il n'est donc pas étonnant que le terme Ω ne soit pas un "bon" terme. Il semble donc réaliste de fournir un mécanisme syntaxique permettant de restreindre les expressions des formalismes de réécriture d'ordre supérieur au termes possédant une interprétation ensembliste. Cette restriction est obtenu par l'ajout de systèmes de types à ces formalismes afin de pouvoir garantir la cohérence des données. De plus, les systèmes de types, en particulier les systèmes de types simples, nous permettront dans certains cas de garantir la terminaison.
Revenons maintenant au problème du filtrage.
Il est courant de définir explicitement une fonction par cas. Ainsi par exemple, la fonction caractéristique de l'ensemble des entiers pairs peut être définie comme suit:
| est_pair: | ⎧ ⎪ ⎨ ⎪ ⎩ |
|
Cette fonctionnalité à longtemps été absente des langages de programmation fonctionnelle fondés sur le λ-calcul [Wan84]. Il n'était alors possible que de programmer des définitions équivalentes à: "Si n=0 alors vrai sinon si n=1 alors faux sinon est_paire(n−2)". Cette formulation, par imbrication de tests sur les valeurs des arguments et non sur leurs formes, conduit souvent à des programmes plus longs et moins compréhensibles donc plus sujets aux erreurs de programmation que la formulation par cas. Depuis quelques années, les langages de programmations [LM92, Obj, HPJP92, Har02] et les assistants de preuve [Coq00, , Hal, ELA, Isa] permettent de définir des fonctions par cas et d'utiliser le filtrage comme mécanisme d'évaluation. Cependant, le fondement théorique de ces langages est resté le λ-calcul (ou ses extensions à l'ordre supérieur) où le filtrage n'est pas primitif.
De même, il est très difficile en λ-calcul de définir et d'utiliser aisément des types de données récursifs, pourtant très utilisés tant dans les langages de programmation que dans les assistants de preuve. À titre d'exemple, rappelons ici le codage des entiers de Church naturels en λ-calcul:
|
et celui du λ-terme définissant la fonction plus:
|
L'évaluation d'une addition très simple devient, dans ce cas, très complexe:
|
Il est en revanche très facile de définir les entiers naturels dans les langages de programmation modernes. Nous présentons ici une définition de ce type en OCAML:
type nat = | Zero | S of nat
que l'on pourrait traduire par: "Zero est un entier et si n est un entier, alors S(n) (le successeur de n) est aussi un entier".
Une définition de la fonction plus est alors:
let rec plus n m =
match n with
| Zero -> m
| S(k) -> S(plus k m)
qui exprime le fait que, pour calculer la somme de deux entiers, il suffit de considérer deux cas:
Lors de l'application de la fonction plus à deux entiers donnés n et m, le mécanisme de réduction de tels langages va tout d'abord filtrer n par les différents motifs possibles (les différentes formes possibles pour n, dans notre cas 0 ou s(k)) et exécuter le code correspondant.
La définition de fonctions par cas et l'utilisation du filtrage constituent donc une avancée importante dans le domaine de la programmation. Cette thèse est consacrée à l'étude de l'évaluation (implicite ou explicite) du filtrage dans les langages de programmation.
De nombreux travaux ont été effectués sur ce sujet recouvrant les différents cas de gestions implicites ou explicites des mécanismes de substitution et de filtrage. En effet, le problème de la gestion du filtrage vis à vis de l'implantation est le même que celui de la gestion de la substitution: il est nécessaire, lors de l'implantation, de rendre cette gestion explicite. Il est donc évident que l'étude du filtrage doit être incorporée dans les formalismes et ceci de manière d'autant plus évidente depuis le contre-exemple de terminaison de Melliès [Mel95].
L'étude du filtrage recouvre le domaine de la compilation de motifs [Aug85, Sch88, KL91, PS93, LM01, Mar92], auquel nous n'aurons pas l'occasion de nous intéresser dans ce document, et celui, plus proche de notre sujet, de l'évaluation du filtrage. Cette évaluation peut être implicite [KPT96, CK99a, CK98, Cir00, CK01] ou explicite [CK99a, BKKR01]. Le domaine de l'étude de l'évaluation du filtrage peut aussi être partitionné en fonction de la classe des filtres considérés. Certains formalismes acceptent toute expression comme filtre (y compris des abstractions). La famille de ces formalismes comprend en particulier le calcul de Vincent Van Oostrom [Oos90] et la grande famille des ρ-calculs [CK98, CK99b, Cir00, CKL01b, CKL01a, FK02]. Une deuxième famille est celle des formalismes n'acceptant que des filtres "à la ML" [KPT96, Kes93, CK99a]. Les travaux présentés dans ce document [For02a, FK03] sont issus de la seconde de ces deux familles en ce sens qu'ils étudient des filtres "à la ML".
Ce document est essentiellement consacré à l'étude du filtrage dans les langages de programmation.
Nous aurons pour cela besoin d'introduire, au chapitre 2, un certain nombre de notions formelles telles que les réécritures du premier ordre et d'ordre supérieur, la confluence, la terminaison ou encore les systèmes de types.
Le chapitre 3 sera consacré à l'étude de la terminaison d'un λ-calcul possédant un mécanisme explicite de gestion de la substitution: le λσ w-calcul. Ce formalisme est la version "faible" du λσ-calcul [ACCL90]. Les calculs de substitutions explicites dits faibles sont des formalismes qui ne permettent pas aux substitutions de traverser les abstractions: il n'existe pas, dans ces formalismes, de règle de la forme (λ x. M) [ s ] → λ x. (M [ s ] ). Cette restriction présente de nombreux avantages. Tout d'abord, ces formalismes fournissent une description plus proche des implantations des langages de programmation fonctionnels actuels qui implantent tous des stratégies faibles. Le deuxième avantage des calculs faibles est, tout en gardant des noms de variables, de ne plus recourir à l'α-conversion lors de l'évaluation pour garantir la non capture de variables. Enfin, les calculs faibles présentent l'avantage de permettre de recouvrer la terminaison des expressions bien typées. Nous montrerons que le λσ w-calcul possède la propriété de terminaison sur l'ensemble de ses expressions bien typées. Notre technique de démonstration est une adaptation d'une preuve due à Ritter [Rit94]. 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 alors 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. 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 enfin de remarquer que, puisque e ' termine, il en est de même pour e, nous conclurons que toute expression bien typée du λσ w/≡-calcul termine, nous en déduirons la terminaison du λσ w-calcul à l'aide d'un lemme technique.
Nous présenterons au chapitre 4, un nouveau formalisme: le λ Pw-calcul qui sera une extension du λσ w-calcul en ce sens que tout terme du λσ w-calcul sera en particulier un terme du λ Pw-calcul. Ce formalisme reprend le système de filtres des travaux antérieurs sur les filtres "à la ML" [KPT96, Kes93, CK99a]. Ces filtres sont essentiellement des variables, des paires de filtres et des filtres de choix. Informellement, un programme OCAML de la forme :
function | P1 -> M1 | P2 -> M2
pourra être "traduit" par le λ Pw-terme suivant :
| λ | ⎡ ⎣ | ξ ∣ P1,P2 | ⎤ ⎦ | . | ⎡ ⎣ | ξ ∣ M1,M2 | ⎤ ⎦ |
où [ξ ∣ P1,P2 ] est un filtre de choix.
L'avancée majeure du calcul λ Pw par rapport aux travaux antérieurs sur le filtrage est d'être le premier élément de cette branche de recherche à traiter simultanément de manière complètement explicite les deux mécanismes du filtrage et de la substitution. Nous démontrerons que ce calcul satisfait les propriétés usuelles: confluence sur l'ensemble de ses expressions et terminaison sur l'ensemble de ses expressions bien typées. Nous réutiliserons pour ce dernier point la technique présentée au chapitre 3. Cette technique s'appuie sur la préservation de types par réduction. Cette préservation est, en fait, le point crucial de la démonstration de la terminaison du λ Pw-calcul et sa démonstration s'est avérée particulièrement ardue. Il a été nécessaire d'introduire une nouvelle notion de variable libre localisée qui a permis de définir l'ensemble des termes acceptables qui sont les termes du λ Pw-calcul "bien formés". Nous ne considérons alors plus que des expressions bien formées.
La preuve de confluence est obtenue en remplaçant le λ Pw-calcul par une version avec "substitutions implicites" dont nous démontrons la confluence par une technique classique due à Tait et Martin-Löf [Bar84]. Nous concluons alors à la confluence de λ Pw sur l'ensemble de ses expressions "bien formées" par un lemme dit d'interprétation. Informellement ce lemme nous permet de déduire la confluence d'un système de réduction →R de la confluence d'un autre système →R' sous certaine condition.
Cette étude reprend les résultats présentés à Copenhague lors de la conférence internationale RTA en juillet 2002 [For02a, For02b].
Cependant, le λ Pw-calcul présente à nos yeux un défaut: il n'est pas possible d'utiliser des symboles de fonction ni de l'enrichir avec de nouvelles règles. Afin de pallier ce problème, nous avons, en collaboration avec Delia Kesner, entrepris une étude du filtrage dans les formalismes de réécriture d'ordre supérieur. Nous avons présenté [FK03], un formalisme permettant l'évaluation implicite de filtres complexes "à la ML". Cette étude présente un nouveau formalisme inspiré des SERS [BKR00]: les Expression Reduction Systems with patterns (ERSP). Ce formalisme nous permet par exemple de définir la fonction map en une seule règle de réécriture:
| map(f,l) → app(λ | ⎡ ⎣ | ξ ∣ nil,cons(h,t) | ⎤ ⎦ | . | ⎡ ⎣ | ξ ∣ nil,cons(f(h),map(f,t)) | ⎤ ⎦ | ,l) |
Nous donnerons un critère syntaxique de confluence pour ce formalisme. Les ERSPs vérifiant ce critère seront dit orthogonaux. Ils formeront une "extension" des systèmes orthogonaux du premier ordre. Nous utiliserons une fois encore la technique de preuve de confluence due à Tait et Martin-Löf [Bar84]. Ces résultats seront présentés au cours du chapitre 5.
Nous conclurons alors en rappelant, au chapitre 6, les résultats obtenus au cours de cette thèse et en présentant un certain nombre de travaux en cours et de perspectives de recherche.