1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 Maître de Conférences au Laboratoire d'Informatique Fondamentale de Marseille
The alternation hierarchy problem asks whether every µ-term φ, that is, a term built up also using a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a µ-term where the number of nested fixed points of a different type is bounded by a constant independent of φ. In this paper we give a proof that the alternation hierarchy for the theory of µ-lattices is strict, meaning that such a constant does not exist if µ-term are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free µ-lattices by means of games and strategies.
Theory and Applications of Categories, 2002, Vol 9/9, Issue CT2000, p. 166-197