A Co-induction Principle for Recursively Defined Domains
University of Cambridge, Computer Laboratory, 1992 - Abstract data types (Computer science) - 25 pages
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
1 page matching natlist in this book
Results 1-1 of 1
What people are saying - Write a review
We haven't found any reviews in the usual places.
Abramsky applicative bisimulation associated partial projection bifinite domains bifinite predomain binary relations co-induction principle co-induction property coalgebra colimiting cone colimits of w-chains constructed constructor recursively defined continuous function convex powerdomain constructors Cts(V denotational semantics disjoint union domain equations embedding embedding-projection pairs extensional F(If family of binary fc(u functor F greatest fixed point higher order functional holds implies initial algebra injective function inl(x inr(x inr(y internal full abstraction invariant isomorphism Lawson-closed subset lazy lambda calculus least elements Lemma lifted predomains monotone functions monotone operator morphism n-tuple of predomains natlist natq natural transformation Nil I Cons order functional programming parameterized recursive partial exponential partial function space partial order partial projection sends predomain constructor recursively predomains recursively defined predornain proof principles Proposition 3.3 proved by induction r-simulation reca.<r recursive domains recursive predomains RECURSIVELY DEFINED DOMAINS satisfying semantics of SCCS simulation Standard ML structure sucq suffices suppose Theorem 2.5 underlying set w-continuous functor