Higher-order unification via explicit substitutions

G. Dowek, T.Hardin, C. Kirchner

IBP-Litp 1995/03: Rapport de Recherche Litp / Litp research reports
43 pages - Janvier/January 1995 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: Higher-order unification via explicit substitutions

Résumé : L'unifcation d'ordre supérieur peut être définie comme l'unification équationnelle associée à la théorie bh. Mais elle diffère de l'unification équationnelle du premier ordre par le processus de substitution, qui doit effectuer des renommages pour éviter des captures. Or, les méthodes classiques d'unification équationnelle (comme la surréduction) sont fondées sur la greffe, mot désignant ici la substitution du premier ordre. Elles ne peuvent donc pas être directement utilisées pour effectuer l'unification d'ordre supérieur, réalisée actuellement à l'aide d'algorithmes spécifiques. Dans cet article, nous montrons comment ramener l'unification d'ordre supérieur à l'unification équationnelle du premier ordre, dans une théorie appropriée.
.L'idée générale est de remplacer la substitution par la greffe, mais ce remplacement n'est pas du tout immédiat et soulève deux problèmes majeurs. Tout d'abord, certains problèmes d'unification d'ordre supérieur peuvent avoir des solutions si la greffe est utilisée comme mécanisme d'instanciation et ne pas en avoir si l'instanciation est faite par la substitution. Ensuite, la validité des algorithmes d'unification équationnelle repose sur le fait que greffe et réduction commutent. Ce n'est pas le cas pour la théorie bh et la greffe, et donc, la réduction d'une équation peut changer son ensemble de solutions. Cette difficulté est dûe à l'interaction entre la bh-conversion et l'instantiation par unification, cette difficulté ne venant pas des calculs eux-mêmes mais tout simplement du double rôle des variables au cours de ces processus. En fait, deux catégories de variable interviennent : celles qui sont instanciées par le processus d'unification, celles qui sont gérées par la bh-conversion, chacune des catégories jouant en quelque sorte le rôle de constante pour le processus gérant l'autre. Nous définissons un calcul dans lequel ces deux catégories sont complètement disjointes, calcul dans lequel la greffe et la réduction commutent. Pour que ce dernier point soit réalisé, il faut retarder la substitution d'une variable d'unification par une variable de réduction jusqu'au moment où la variable d'unification devient instanciée. Ce retard de la substitution de la b-reduction et la séparation des deux catégories de variables sont des caractéristiques du ls-calcul, une théorie équationnelle du premier ordre, contenant le lambda-calcul comme sous-système. Les variables de réduction sont codées par des indices de de Bruijn, les variables d'unification sont codées à l'aide des variables du ls-calcul.
Le ls-calcul étant une théorie du premier ordre, nous pourrions utiliser des algorithmes classiques, tels la surréduction, pour y effectuer l'unification. Nous présentons cependant un algorithme spécifique à cette théorie pour des raisons d'efficacité. Puis nous montrons comment ramener l'unifcation d'ordre supérieur à l'unification dans ce calcul de substitutions explicites. Nous fournissons ainsi un nouvel algorithme d'unification d'ordre supérieur, débarassé de certaines des diffcultés des algorithmes antérieurs, en particulier de la gestion fonctionnelle des portées des variables. L'algorithme original de G. Huet peut être vu comme une stratégie particulière de notre algorithme, chacune de ses étapes étant décomposée en étapes plus élémentaires, donnant ainsi une vision plus atomique du calcul de l'unification. De plus, les formes résolues de l'algorithme de G. Huet sont obtenues à partir des formes résolues de notre algorithme par un calcul très simple.

Abstract : This paper investigates the general idea of using a calculus of explicit substitution to perform unification in simply typed l-calculus. In order to fulfill such a program, we first recall the ls-calculus of explicit substitutions with a special emphasis on using it for performing unification. For this purpose two kinds of variables are handled, one for the lambda computations and the other one for the unification computations. The typed version of the calculus is set up in such a way that it reduces to a first order many sorted equational theory.
We then study the unification problem in this equational theory. Using a rule based approach, we give a complete algorithm for solving unification problems not involving variables of sort substitution. This algorithm uses in a deep way our knowledge of the underlying equational theory of explicit substitution, so that unnecessary computations are avoided in a large extend. In the last part of the paper, we relate the previous algorithm to the problem of unification in simply typed l-calculus. This is performed by proving that the previous complete unification algorithm for the ls-calculus can be used to compute complete set of solutions for equation systems in the l-calculus. The resulting approach can be seen as the decomposition of Huet's algorithm in elementary steps, all based on a first order equational theory, that can consequently be easily implemented.

Publications internes Litp 1995 / Litp research reports 1995