[Prev][Next][Index][Thread]
Co-induction for recursive domains
Date: Thu, 23 Apr 92 17:42:26 +0100
The following paper may be of interest to subscribers to this list. It is
available by anonymous ftp from theory.doc.ic.ac.uk [146.169.2.37] as
/theory/papers/Pitts/coinduction.dvi or /theory/papers/Pitts/coinduction.ps
Andrew M. Pitts, "A Co-induction Principle for Recursively Defined Domains",
University of Cambridge Computer Laboratory Technical Report No.~252, May 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 [3], 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 [1,2] 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.
References
[1] S.Abramsky, "A Domain Equation for Bisimulation",
Information and Computation 92(1991) 161--218.
[2] S.Abramsky, "The Lazy Lambda Calculus". In: D.Turner
(ed.), "Research Topics in Functional Programming"
(Addison-Wesley, 1990), pp 65--116.
[3] R.Milner and M.Tofte, "Co-induction in relational
semantics", Theoretical Computer Science 87(1991) 209--220.