The Alternation Hierarchy for the Theory of -lattices
Luigi Santocanale November 2000 |

## Abstract:
The alternation hierarchy problem asks whether every
-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
-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 -lattices is strict, meaning that such number does not exist if -terms 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
Available as |

Last modified: 2003-06-08 by webmaster.