[Prev][Next][Index][Thread]

paper available




The following is an advert for a tech report which is an expanded of my LICS'93
paper on relational properties of recursively defined domains. It is somewhat
different in emphasis and broader in scope than the LICS paper. It also has a
shorter title! 

It is available by anonymous ftp from
theory.doc.ic.ac.uk as papers/Pitts/rpd.{dvi,ps}.Z

or from ftp.cl.cam.ac.uk as 
reports/TR321-ap-relational-properties-of-domains.ps.gz
 

Andy Pitts

-------------------
Relational Properties of Domains
Andrew M. Pitts 
Univ. Cambridge Computer Laboratory 
TR No. 321, December 1993, 37pp

  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
  "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 (in Cambridge Univ. 
  Computer Laboratory Tech. Rept. No. 252), by which equalities
  between elements of recursively defined domains may be proved via an
  appropriate notion of `bisimulation'.
------------------