[Prev][Next][Index][Thread]
Re: monotonic subtype relations?

To: types

Subject: Re: monotonic subtype relations?

From: John.Reynolds@proof.ergo.cs.cmu.edu

Date: Wed, 10 Apr 91 12:38:51 EDT

InReplyTo: Your message of Tue, 09 Apr 91 22:31:22 0400. <9104100231.AA01926@stork>

InReplyTo: Your message of Tue, 09 Apr 91 22:31:22 0400. <9104100231.AA01926@stork>

Sender: meyer@theory.lcs.mit.edu
To: Clem BakerFinch <clem@echo.canberra.edu.au>
Cc: types@theory.lcs.mit.edu
Date: Wed, 10 Apr 91 10:02:34 EDT
In Dana Scott's work, there are several notions of "subdomain" that may
fit your needs. A retraction pair <f,g> from a domain D to a domain E
consists of continuous functions f from D to E and g from E to D
such that f;g is the identity on D. (I use semicolons for composition
in diagrammatic order.) If g;f approximates the identity on E, then
the retraction pair is called a projection pair; if the identity on E
approximates g;f then the retraction pair is called a closure pair.
If <f,g> is a retraction (projection, closure) pair from D to E and
<f',g'> is a retraction (projection, closure) pair from D' to E' then
<f",g"> is a retraction (projection, closure) pair from D>D' to E>E',
where f"(h) = g;h;f' and g"(h) = f;h;g'.
Thus one could give a semantics to a subtyping relation where > is
monotonic in both arguments by using a functor from the preorder of
types to the category of retraction pairs (or either of its subcategories
of projection or closure pairs). Informally, one interprets "a is a
subtype of b" as "There is a retraction pair from the domain denoted by a
to the domain denoted by b".
I hope this helps.  John Reynolds