For programming languages whose denotational semantics uses fixed points of
domain constructors of mixed variance, proofs of correspondence between
operational and denotational semantics (or between two different
denotational semantics) often depend upon the existence of relations
specified as the fixed point of non-monotonic operators. This paper
describes a new approach to constructing such relations which avoids having
to delve into the detailed construction of the recursively defined domains
themselves. The method is introduced by example, by considering the proof
of computational adequacy of a denotational semantics for expression
evaluation in a simple, untyped functional programming language.