A Co-induction Principle for Recursively Defined Domains

Front Cover
University of Cambridge, Computer Laboratory, 1992 - Abstract data types (Computer science) - 25 pages
0 Reviews
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

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.

Common terms and phrases

Bibliographic information