Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
@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.}}