Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices

Fixpoint expressions built from functional signatures interpreted over arbitrary complete lattices are considered. A generic notion of automaton is defined and shown, by means of a tableau technique, to capture the expressive power of fixpoint expressions. For interpretation over continuous and complete lattices, when, moreover the meet symbol A commutes in a rough sense with all other functional symbols, it is shown that any closed fixpoint expression is equivalent to a fixpoint expression built without the meet symbol A. This result generalizes Muller and Schupp's simulation theorem for alternating automata on the binary tree.