Tech Report CS-92-25

A Universal Top-Down Fixpoint Algorithm

Baudouin Le Charlier and Pascal Van Hentenryck

May 1992

Abstract:

Computing fixpoints and postfixpoints of transformations has numerous applications in computer science. In this paper, we present a universal top-down fixpoint algorithm based on the weak assumption that the transformation is defined by an effective procedure. Given the procedure and a parameter value, the universal algorithm computes the value of the parameter value in the least fixpoint of the transformation has the property of focusing on the subset of elements necessary to compute the result. The total correctness of the algorithm is proven and requires some weak (but rather technical) assumptions. These conditions can be relaxed further if postfixpoints suffice for the application. As a consequence, the algorithm generalizes and abstracts numerous algorithms and provides a versatile alternative to bottom-up algorithms. It has been used to derive specific abstract interpretation algorithms for Prolog, which are practical both in terms of efficiency and accuracy and are, to our knowledge, the fastest algorithms available.

(complete text in pdf or gzipped postscript)