L'étude formelle du filtrage dans les formalismes de réécriture d'ordre supérieur à été rendue très importante par l'apparition de langages de programmation fonctionnelle [LM92, Obj, HPJP92, Har02] et d'assistants de preuve [Coq00, , Hal, ELA, Isa] utilisant explicitement cette fonctionnalité. Au cours de cette thèse, nous nous sommes intéressé au filtrage tant explicite qu'implicite ainsi qu'à son interaction avec le mécanisme de substitutions. Nous avons présenté deux formalismes de réécriture d'ordre supérieur dans lesquels le filtrage sur des motifs complexes est une opération primitive. Afin de pouvoir définir des fonctions par cas, nous avons du développer les notions de variable de choix et de terme et motif de choix dans les deux formalismes. Le rôle principal des variables de choix est de mettre en relation les différentes occurrences des termes de choix et des motifs de choix. Ainsi, un programme OCAML [Obj] ayant le squelette suivant:
function | P1 -> M1 | P2 -> M2
pourra se traduire dans ces deux formalismes par une expression de la forme:
| λ | ⎡ ⎣ | ξ ∣ P1,P2 | ⎤ ⎦ | . | ⎡ ⎣ | ξ ∣ M1,M2 | ⎤ ⎦ |
dans laquelle [ξ ∣ P1,P2 ] est un motif de choix, [ξ ∣ M1,M2 ] est un terme de choix et ξ est une variable de choix.
Le premier de ces deux formalismes, le λ Pw-calcul, est une extension de la version faible du λσ-calcul [ACCL90] au filtrage avec motifs "à la ML". Ce formalisme propose des mécanismes de filtrage et de substitutions complexes totalement explicites contrairement aux formalismes précédemment étudiés [CK99a]. Le λ Pw-calcul possède toutes les propriétés classiques des λ-calculs. Ce calcul préserve les variables libres par réduction et possède la propriété de confluence sur l'ensemble de ses expressions, ce qui garantit l'unicité des résultats sous réserve d'existence. Le λ Pw-calcul préserve également les types par réduction pour un système de types simples ce qui nous a permis de démontrer la normalisation forte des expressions bien typées, dont le rôle est de garantir l'existence de résultats aux calculs. La mise au point de ce calcul et en particulier celle de la préservation de types par réduction s'est avérée particulièrement complexe et nous a conduit à la définition de deux nouvelles notions: les variables libres localisées et les expressions acceptables. La notion de variables libres localisées d'une expression du λ Pw-calcul, qui est un raffinement de la notion classique de variables libres, nous a permis de définir l'ensemble des expressions acceptables. Ces expressions sont celles préservant leur ensemble de variables libres par réduction. Une telle restriction est naturelle en cela qu'elle permet de retirer de l'ensemble des expressions des termes correspondant à un programme OCAML [Obj] tel que:
function | x -> y | y -> x
qui n'est pas un "bon" terme.
Le second de ces formalismes, les ERSP, est inspiré par les ERS [Kha90] l'un des formalismes de réécriture d'ordre supérieur bien connus. À ce titre, les ERSP permettent de modéliser aisément des systèmes de réécriture d'ordre supérieur complexes. Ce formalisme propose, de plus, des mécanismes de filtrage et de substitutions implicites. De tels mécanismes, nous permettent, par exemple, de modéliser la fonction map, prenant en entrée un fonction f et une liste l et retournant la liste des résultats de f sur les éléments de l, comme suit:
| map(µ X. F,L)→ | ⎡ ⎣ | ξ ∣ Nil,Cons(F{X by h},map(µ X. F,t)) | ⎤ ⎦ | { | ⎡ ⎣ | ξ ∣ Nil,Cons(h,t) | ⎤ ⎦ | by L} |
Nous avons de plus proposé un critère syntaxique de confluence pour les ERSP. Ce critère est une extension naturelle d'un critère classique de confluence des formalismes de réécriture d'ordre supérieur: l'orthogonalité. Bien que le mécanisme de réduction des ERSP soit complexe, la représentation de systèmes de réécriture d'ordre supérieur avec motifs se révèle très aisée dans ce formalisme. Deux points sont à noter concernant les ERSP. Ce formalisme comprend, en plus du non-déterminisme usuel obtenu par l'ensemble des règles d'un système de réécriture, une gestion complète du non-déterminisme grâce à un mécanisme de réduction permettant de réécrire un terme en un ensemble de termes par une seule application d'une règle. Enfin, la preuve de confluence des ERSP, nous offre en particulier un critère de confluence pour les SERSs [BKR00].
De nombreuses pistes de recherches s'ouvrent désormais devant nous.
Une extension des ERSP aux mécanismes de filtrage et de substitution explicites est actuellement en cours de développement. Cette étude, grâce aux travaux effectués sur le λ Pw-calcul, ne semble pas devoir poser de problèmes théoriques complexes. L'idée principale de ce travail est de proposer un système de "règles" Rpm des ERSP permettant d'effectuer de manière explicite tant le filtrage que la substitution. Cette extension nous permettra de nous rapprocher du niveau des implantations. En effet, dans le cadre d'une implantation ni l'opération de filtrage ni celle de substitution ne peuvent être implicites. Un tel système de règles devra en particulier posséder une propriété de préservation de la confluence: étant donné un ERSP R "classique", i.e. tel que présenté dans le chapitre 5 de ce document, si R est confluent alors le ERSP R∪Rpm devra être confluent.
Un autre travail actuellement en cours est la mise au point d'une traduction complètement automatique du fragment purement fonctionnel de OCAML vers les ERSP. Le principe de cette traduction est très simple. Il suffit de créer un symbole de fonction pour tout nouveau constructeur de type de OCAML et pour toute définition de fonction, puis d'utiliser la traduction suivante pour le filtrage de OCAML:
| ⎫ ⎪ ⎪ ⎬ ⎪ ⎪ ⎭ | ↦ | ⎡ ⎣ | ξ ∣ M1,…,Mn | ⎤ ⎦ | { | ⎡ ⎣ | ξ ∣ P1,…,Pn | ⎤ ⎦ | by t} | |||||||||||||||
Une telle traduction, nous permettrait d'étudier de manière explicite l'utilisation du filtrage grâce à un interpréteur de ERSP dont le code est actuellement en cours de développement. Cette traduction devra préserver les "bonnes propriétés" de confluence et de terminaison des programmes traduits.
Compte tenu de la proximité des ERSP et du ρ-calcul [CK01], une étude comparative de ces deux formalismes est également nécessaire. L'un des problèmes majeur de cette comparaison étant de déterminer la version du ρ-calcul avec laquelle comparer les ERSP. Deux pistes sont possibles: l'extension du mécanisme de filtrage des ERSP à des théories autres que purement syntaxiques ou la comparaison avec une version du ρ-calcul muni uniquement du filtrage syntaxique. Cette comparaison ne semble pas évidente puisque le mécanisme de filtrage du ρ-calcul prend en compte une classe plus large de motifs.
L'un des problèmes les plus complexes de la réécriture d'ordre supérieur est celui de la terminaison qui nous permet de garantir l'existence de résultats. Nous devrons à plus long terme proposer un système de types pour les ERSP et étudier la normalisation forte des ERSP. Plusieurs pistes s'offrent à nous dans ce domaine. L'une des plus simples conceptuellement est d'étendre l'une des méthodes déjà proposées pour les formalismes classiques d'ordre supérieur tel que le schéma général [BJO01] ou la méthode reposant sur les HORPO [JR99]. Une autre piste est d'essayer d'étendre certaines techniques de terminaison du premier ordre telles que celle des paires de dépendance [Art97, Urb01].
Les indices de de Bruijn [dB72, BKR00] permettent de rapprocher la théorie de l'implantation réelle. En effet ces indices, en remplaçant les noms de variables, permettent en particulier de ne plus avoir besoin d'α-conversion dans la théorie des ERSP. Il sera à terme nécessaire de proposer une version des ERSP utilisant de tels indices. L'un des problèmes majeurs de ce travail consiste en la mise au point de la notion d'indice de de Bruijn dans le cadre des motifs complexes. Il semble cependant envisageable de remplacer la notion classique d'indices représentés à l'aide d'entiers naturels par une notion fondée sur des arbres d'entiers.
Certaines questions devront être posées à propos de la "réduction en tant qu'objet" dans le cadre des ERSP. Le formalisme des ERSP rentre-il dans le cadre de la réécriture axiomatique [GLM92] ? Peut-on définir aiséement une notion de résidu dans les ERSP afin d'étudier la propriété de confluence d'un point de vue différent de celui abordé dans cette thèse? Le fait d'abstraire la notion de réduction dans les ERSP permettrait l'application de résultats bien connus en théorie de la réécriture, comme par exemple quelques résultats concernant la standardisation, la terminaison, …