Abstract FR:

Dans la plupart des interpretes prolog existants, l'unification est implantee, pour des raisons d'efficacite, sans test d'occurrence. Mais ceci peut avoir de graves consequences: creations de termes infinis non voulus, incorrection de la sld-resolution, bouclage dans l'algorithme d'unification, incorrection de certaines transformations,. . . Notre travail a pour objectif de definir des conditions suffisantes (le probleme du test d'occurrence etant indecidable en general) assurant qu'un programme logique (clauses de horn) peut s'executer sans test d'occurrence et sans pour autant modifier les proprietes declaratives et operationnelles du programme (aucun terme infini n'est cree et aucun echec ne peut etre du a un test d'occurrence positif). Pour cela, nous generalisons une methode introduite par p. Deransart et j. Maluzynski (1985) qui relie le probleme du test d'occurrence en programmation logique au probleme de circularite dans les grammaires attribuees: 1) en donnant une condition plus generale de non-necessite du test d'occurrence, independante de la strategie qui peut s'appliquer a de larges classes d'interpretes (sequentiels, avec appels retardes, paralleles. . . ); 2) en donnant un cadre theorique dans lequel on peut etudier clairement la relation entre le probleme du test d'occurrence et la circularite dans un systeme d'equations. Ce cadre permet de mettre en evidence la raison du lien entre la programmation logique et les grammaires attribuees et peut etre utilise pour d'autres problemes comme la verification de types et de modes