Presentation et evaluation de la complexite en moyenne des algorithmes d'unification

L'unification dans les langages du premier ordre est une operation fondamentale en calcul symbolique et en programmation logique. On dispose de beaucoup d'algorithmes d'unification, mais il n'y a pas de consensus quant a savoir lequel est le meilleur a utiliser en pratique. L'algorithme lineaire de Paterson Wegman a la plus faible complexite dans le cas le pire, de l'algorithme de Martelli Montanari et finalement c'est souvent l'algorithme de Robinson qui est employe dans beaucoup d'applications malgre sa complexite exponentielle dans le cas le pire. Cette situation s'explique de plusieurs facons : un fait important est que, dans la pratique, les sous-problemes d'unification ne sont pas independants et les algorithmes d'unification lineaires ne sont pas tres performants sur les sequences d'unification-desunification. Dans cet article, nous presentons des arguments theoriques bases sur l'etude de la complexite en moyenne. Nous montronts tout d'abord que la famille des paires d'arbres binaires unifiables est exponentiellement negligeable devant la famille des paires d'arbres binaires formes a partir de l symboles de fonctions binaires, c constantes et v variables. Nous analysons les differentes causes d'echec et nous obtenons des evaluations asymptotiques et numeriques. Nous generalisons ensuite les resultats pour ces familles de termes et nous montrons qu'une legere modification de l'algorithme de Herbrand-Robison a une complexite moyenne constante sur les paires d'arbres quelconques. D'autre part, nous montrons que l'algorithme de Martelli Montanari et une de ses ameliorations ont une complexite moyenne lineaire sur les paires d'arbres quelconques. Les echecs par clash ne sont en effet pas suffisants pour assurer une complexite moyenne constante, il est necessaire de disposer d'un test d'occurrence efficace (i.e. qui ne necessite pas un parcours complet des sous-arbres). Enfin dans la derniere partie, nous generalisons nos resultats sur la probabilite d'occurrence al'unmodele avec un nombre infini de variables