The Alternation Hierarchy for the Theory of mu-lattices - Santocanale, Luigi (BRICS Report Series, 2000)
The alternation hierarchy problem asks whether every mu-term, that is a term built up using also a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a mu-term where the number of nested fixed point of a different type is bounded by a fixed number. In this paper we give a proof that the alternation hierarchy for the theory of mu-lattices is strict, meaning that such number does not exist if mu-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free mu-lattices by means of games and strategies.