WEIGHTED SYSTEMS OF EQUATIONS

This paper proposes a characterisation of some iterative phenomena in the operational behaviour of Horn clause languages. The termination an d the size of the SLD tree of a set of Horn clauses are difficult to e stimate or establish if some rules are recursive. These problems are o ften based on an iterative application of one or more sequences of rul es. We have proposed a new syntactical object, the weighted graph, whi ch is a generalisation of the directed graph. In this formalism, the t rees are not rational because of their infinity of variables, and they have been established to be the most general fixpoints of the binary recursive rules (i.e. p(t1,...,t(n))<--p(t1',...,t(n)').), this corres ponding to a bi-infinite application of such rules. In the finite and infinite cases, the weighted graphs could give an approximation of the finite or infinite sequence of inferences with respect to one binary rule. The goal of this paper is to show that the mathematical framewor k of the operational semantic of Horn clauses languages, i.e. systems of equations and their notions of unification and solvability, most ge neral solution can be extended to formalise any iterative application of binary rules, i.e. for any finite, infinite or bi-infinite number o f iterations. This is based on a new kind of systems of equations, cal led flat systems, whose concepts can be easily extended through their iterative interpretation to weighted systems.