Bounded fixed point iteration∗

In the context of abstract interpretation for languages without higher-order features we study the number of times a functional need to be unfolded in order to give the least fixed point. For the cases of total or monotone functions we obtain an exponential bound and in the case of strict and additive (or distributive) functions we ob-tain a quadratic bound. These bounds are shown to be tight in that sufficiently long chains of functions can be shown to exist. Specialis-ing the case of strict and additive functions to functionals of a form that would correspond to iterative programs we show that a linear bound is tight. This is related to the analyses studied in the literature (including strictness analysis).