Strongly Reduced Systems of Equations

Generally, the idempotent most general unifier is used for expressing the constraints of unification [Eder 85]. A more general syntactic object is the system of equations, that is, a set of equations of the form t = t' where t and t' are trees. However, the advantages of the systems of equations are first the memory size, secondly the efficency of the unification algorithm, and also that within the context of termination and complexity, the behaviour of resolution can be understood better through the constraints between the variables than from the final susbtitution of these variables. The reduced systems of equations introduced by [Colmerauer 84] express this feeling and this is strongly linked with the representative notion introduced by [Huet 1976] and the directed acyclic graph and the directed graph are based on the same idea : the common informations are shared [Fages 83]. Similarly, within backtracting intelligent, an important aspect is to express the dependancy graph of variables. The goal of this paper is to show that the shortest expression of a reduced system can be used to express as clearly as possible the constraints generated by a system of equations, however also to understand the convergent, invariant or periodic phenomenons for some recursive Prolog programs.