Finding fixpoints in finite function
spaces using neededness analysis
and chaotic iteration
Niels Jørgensen.
Abstract:
A new and efficient algorithm for computing the least fixpoint
of a functional on a finite function space is defined.
The algorithm applies to the computation of the least fixpoint
(global or local) induced by an arbitrary system of functional
equations in a certain formalism.
The algorithm employs a variant of Cousot and Cousot's chaotic iteration,
and uses neededness (or dependency) information to guide the
fixpoint iteration, as for instance in Kildall's early
algorithm.
The neededness analysis is dynamic
as in the algorithms proposed by Muthukumar and Hermenegildo and Le Charlier
et al., with the main difference being that our
neededness analysis is of a more "shallow" nature,
and that our approach is more iterative and less recursive.
The complexity result implies that the worst-case number of iterations
per equation is independent of the total number of equations in the
equation system, where an iteration corresponds to evaluating an
equation once with respect to given values of the functional and
primitive parameters.