@ARTICLE{PittsAM:relpod,
AUTHOR={A.~M.~Pitts},
TITLE={Relational Properties of Domains},
JOURNAL={Information and Computation},
VOLUME=127,
YEAR=1996,
PAGES={66--90},
NOTE={(A preliminary version of this work appeared as Cambridge Univ.
Computer Laboratory Tech. Rept. No.~321, December 1993.)},
ABSTRACT={New tools are presented for reasoning about properties of
recursively defined domains. We work within a general,
category-theoretic framework for various notions of `relation' on
domains and for actions of domain constructors on relations.
Freyd's analysis of recursive types in terms of a property of mixed
initiality/finality is transferred to a corresponding property of
{\em invariant\/} relations. The existence of invariant relations is
proved under completeness assumptions about the notion of relation.
We show how this leads to simpler proofs of the computational
adequacy of denotational semantics for functional programming
languages with user-declared datatypes. We show how the
initiality/finality property of invariant relations can be
specialized to yield an induction principle for admissible subsets
of recursively defined domains, generalizing the principle of
structural induction for inductively defined sets. We also show how
the initiality/finality property gives rise to the co-induction
principle studied by the author ({\em Theoretical Computer
Science\/} {\bf 124}, 195--219 (1994)), by which equalities
between elements of recursively defined domains may be proved via an
appropriate notion of `bisimulation'.}
}