[Prev][Next][Index][Thread]

Re: monotonic subtype relations?

To: Clem Baker-Finch <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