On distributive fixed-point expressions

For every fixed-point expression e of alternation-depth r, we construct a new fixed-point expression e′ of alternation-depth 2 and size O(r · {e}). Expression e′ is equivalent to e whenever operators are distributive and the underlying complete lattice has a co-continuous least upper bound. We show that our transformation is optimal not only w.r.t. alternation-depth but also w.r.t. the increase in size of the resulting expression.