Higher-order chaotic iteration sequences

Chaotic iteration sequences is a method for approximating fixpoints of monotonic functions proposed by Patrick and Radhia Cousot. It may be used in specialisation algorithms for Prolog programs and in abstract interpretation when only parts of a fixpoint result is needed to perform program optimisations. In the first part of this paper we reexamine the definition of chaotic iteration sequences and show how a number of other methods to compute fixpoints may be formulated in this framework. In the second part we extend the technique to higher-order functions. The method of expressing solutions to problems in a recursive style has a long history in Computer Science. Often a solution algorithm may use itself on a subproblem and an implementation may be based on recursion. At times it is more natural to express the solution as a fixpoint equation in which well-definedness is only guaranteed using a fixpoint theorem. This is common in abstract interpretation, data flow analysis, “first ” and “follow” computation, etc. In strictness analysis [11] we may construct functions over the domain 2 = {0, 1} with 0 ≤ 1. If we want to evaluate the function f](x, y, z) = (y ∧ z) ∨ f](z, x, f](y, 1, 1)) for certain arguments, we will in general need to evaluate the function for all possible arguments and recompute until stability. It is, however, often only necessary to recompute the function for some of the possible arguments. 1 By restricting the iteration to a smaller set of arguments, we may greatly simplify the computational task of evaluating the function. In this paper we consider such recursively defined functions for which recursion is not sufficient in the implementation. 1 Language As a start we will consider a simple language consisting of one recursively defined function over a complete partially ordered set D. Programs p in this language will have the form p: letfix f(x1,..., xk) = ef in e where the expressions ef and e are built from parameters, constants, basic operations, and function calls. e: xi | ci | opi(e1,..., ek) | f(e1,..., ek) We may specify the semantics of this language using the functions M and E. M[[letfix f(x1,..., xk) = ef in e]] :