In this paper we present a new fixed point theorem applicable for a countable system of recursive equations over a wellfounded domain. Wellfoundedness is an essential feature of many computer science applications as it guarantees termination of the corresponding fixed point computation algorithms. Besides being a natural restriction, it marks a new area of application, where not even monotonicity is required. We demonstrate the power and versatility of our fixed point theorem, which under the wellfoundness condition covers all the known 'synchronous' versions of fixed point theorems, by means of applications in data flow analysis and program optimization.
Ulrike Peiker, Martin Griebl