This is an old revision of the document!
Mapping Fixpoints Under Lattice Morphisms
Definition: Let and be complete lattices. We call a complete join-morphism iff for each set we have \[
F(\sqcup X_1) = \sqcup \{ F(a).\ a \in X_1 \}
\]
For example, .
Lemma: Let and be complete lattices, and , , be complete join-morphisms such that \[
F(\Gamma(y)) \le \Gamma(F^\#(y))
\] for all . If denotes least fixpoint of a function, then \[
lfp(F) \le \Gamma(lfp(F^\#))
\]
In other words, we can approximate by computing .