Free mu-lattices

Abstract

A mu-lattice is a lattice with the property that every unary
polynomial has both a least and a greatest fix-point. In this paper
we define the quasivariety of mu-lattices and, for a given partially
ordered set P, we construct a mu-lattice JP whose elements are
equivalence classes of games in a preordered class J (P). We prove
that the mu-lattice JP is free over the ordered set P and that the
order relation of JP is decidable if the order relation of P is
decidable. By means of this characterization of free mu-lattices we
infer that the class of complete lattices generates the quasivariety
of mu-lattices.
Keywords: mu-lattices, free mu-lattices, free lattices, bicompletion
of categories, models of computation, least and greatest fix-points,
mu-calculus, Rabin chain games.