The alternation hierarchy problem asks whether every $\mu$-term $\phi$, 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 $\mu$-term where the number of nested fixed points of a different type is bounded by a constant independent of $\phi$.
In this paper we give a proof that the alternation hierarchy for the theory of $\mu$-lattices is strict, meaning that such a constant 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.
Theory and Applications of Categories, Vol. 9, 2002, No. 9, pp 166-197 http://www.tac.mta.ca/tac/volumes/9/n9/n9.dvi http://www.tac.mta.ca/tac/volumes/9/n9/n9.ps http://www.tac.mta.ca/tac/volumes/9/n9/n9.pdf ftp://ftp.tac.mta.ca/pub/tac/html/volumes/9/n9/n9.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/9/n9/n9.psTAC Home