Unifying Nominal Unification

Christophe Calvès 1
1 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Résumé : Il est prouvé que l'unification nominale est quadratique en temps et en espace. Elle le fût par deux approches différentes, toutes deux inspirées de l'algorithme d'unification linéaire de Paterson et Wegman, mais très différentes dans leur manière de prendre en compte les contraintes nominales et celles du premier ordre. Pour traiter les contraintes nominales, Levy et Villaret ont introduit la notion de "replacing" alors que Calvès et Fernández ont utilisés des permutations et ensembles d'atomes. Pour prendre en compte les contraintes structurelles, les premiers utilisent des multi-équations à la manière de l'algorithme de Martelli et Montanari tandis que les seconds miment celui de Paterson et Wegman. Dans ce papier nous proposons une abstraction de ces deux approches et les généralisons à travers la notion de modalité, soulignant les idées générales sous-jacentes à l'unification nominale. Nous montrons que les "replacings" et les environnements sont en fait isomorphes. Cet isomorphisme est de première importance dans la démonstrations de propriétés complexes des deux cotés et une étape supplémentaire vers la complexité réelle de l'unification nominale.
Type de document :
Communication dans un congrès
Femke van Raamsdonk. Rewriting Techniques and Applications, Jun 2013, Eindhoven, Netherlands. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21, pp.143-157, 2013, LIPIcs. 〈10.4230/LIPIcs.RTA.2013.143〉
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00926833
Contributeur : Christophe Calvès <>
Soumis le : vendredi 10 janvier 2014 - 13:27:58
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24
Document(s) archivé(s) le : jeudi 10 avril 2014 - 22:45:16

Fichier

calves_RTA2013.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Christophe Calvès. Unifying Nominal Unification. Femke van Raamsdonk. Rewriting Techniques and Applications, Jun 2013, Eindhoven, Netherlands. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21, pp.143-157, 2013, LIPIcs. 〈10.4230/LIPIcs.RTA.2013.143〉. 〈hal-00926833〉

Partager

Métriques

Consultations de la notice

96

Téléchargements de fichiers

85