Principe

Un terme est representé sous la forme d'un arbre. L'unification consiste à superposer deux arbres représentatifs de deux termes et à en retirer des contraintes sur les variables de ces deux arbres. Ces contraintes doivent être sauvegardées quelques part pour la prochaine unification, c'est le rôle de la pile d'environnements. Plus précisément, la procédure d'unification consiste à unifier deux instances d'arbre dans un certain environnement (contenant les contraintes initiales sur les variables de ces deux instances d'arbre) et à fournir en sortie un environnement résultant contenant les nouvelles contraintes (si l'unification a été possible).
La notion de constante a été intégrée dans le cas des foncteurs : une constante est simplement vue comme un foncteur sans argument. La procédure d'unification n'a donc plus que quatre cas différents à gérer : variable-foncteur, variable-variable, foncteur-variable et foncteur-foncteur, parmi lesquels les deux cas variable-foncteur et foncteur-variable sont symétriques. Les cinq autres cas envisagés dans le sujet (faisant intervenir des constantes) ne sont en fait que des cas particuliers des quatre autres précités (pour plus de détails, on se reportera à la section 2.4 du sujet : ébauche de l'algorithme d'unification, et au schéma correspondant à la page 26).