@ARTICLE{PittsAM:coiprd,
AUTHOR={A.~M.~Pitts},
TITLE={A Co-induction Principle for Recursively Defined Domains},
JOURNAL={Theoretical Computer Science},
VOLUME=124,
YEAR=1994,
PAGES={195--219},
NOTE={(A preliminary version of this work appeared as Cambridge Univ.
Computer Laboratory Tech. Rept. No.~252, April 1992.)},
ABSTRACT={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 {\em
co-induction}. It closely resembles the way bisimulations are used in
concurrent process calculi.\par
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 {\em partial bisimulations}, whereas in the
second case they are his {\em 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.}}