Relational properties of domains

New tools are presented for reasoning about properties of recursively de ned domains. We work within a general, category-theoretic framework for various notions of `relation ' on domains and for actions of domain con-structors on relations. Freyd's analysis of recursive types in terms of a property of mixed initiality / nality is transferred to a corresponding prop-erty of 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 denota-tional semantics for functional programming languages with user-declared datatypes. We show how the initiality / nality property of invariant re-lations can be specialized to yield an induction principle for admissible subsets of recursively dened domains, generalizing the principle of struc-tural induction for inductively dened sets. We also show how the ini-tiality / nality property gives rise to the co-induction principle studied by the author (Theoretical Computer Science 124, 195{219 (1994)), by which equalities between elements of recursively dened domains may be proved via an appropriate notion of `bisimulation'