The Alternation Hierarchy for the Theory of $\mu$-lattices

Luigi Santocanale

November 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

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.