Immediate fixpoints and their use in groundness analysis

Abstract

A theorem by Schröder says that for a certain natural class of functions F: B → B defined on a Boolean lattice B, F(x)=F(F(F(x))) for all x Є B. An immediate corollary is that if such a function is monotonic then it is also idempotent, that is, F(x)=F(F(x)). We show how this corollary can be extended to recognize cases where recursive definitions can immediately be replaced by an equivalent closed form, that is, they can be solved without Kleene iteration. Our result applies more generally to distributive lattices. It has applications for example in the abstract interpretation of declarative programs and deductive databases. We exemplify this by showing how to accelerate simple cases of strictness analysis for first-order functional programs and, perhaps more successfully, groundness analysis for logic programs.