This paper establishes a new property of predomains recursively defined
using the cartesian product, disjoint union, partial function space and
convex powerdomain constructors. We prove that the partial order on such a
recursive predomain D is the greatest fixed point of a certain
monotone operator associated to D. This provides a structurally
defined family of proof principles for these recursive predomains: to show
that one element of D approximates another, it suffices to find a
binary relation containing the two elements that is a post-fixed point for
the associated monotone operator. The statement of the proof principles is
independent of any of the various methods available for explicit
construction of recursive predomains. Following Milner and Tofte, the
method of proof is called co-induction. It closely resembles the way
bisimulations are used in concurrent process calculi.
Two specific instances of the co-induction principle already occur in work
of Abramsky in the form of `internal full abstraction' theorems for
denotational semantics of SCCS and the lazy lambda calculus. In the first
case post-fixed binary relations are precisely Abramsky's partial
bisimulations, whereas in the second case they are his applicative
bisimulations. The co-induction principle also provides an apparently
useful tool for reasoning about equality of elements of recursively defined
datatypes in (strict or lazy) higher order functional programming
languages.