The Alternation Hierarchy for the Theory of mu-lattices
AbstractThe 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
How to Cite
Santocanale, L. (2000). The Alternation Hierarchy for the Theory of mu-lattices. BRICS Report Series, 7(29). https://doi.org/10.7146/brics.v7i29.20163
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.