[Prev][Next][Index][Thread]
the price of embedding-projection pairs
Date: Fri, 18 Oct 91 12:43:55 PDT
This message describes something that I recently realized
about embedding-projection pairs and solutions to domain
equations. I suspect that this is well-known in certain
circles, but I thought it might be of interest to the
rest of this list.
The main idea is that when we solve a recursive
domain equation X = F(X) by finding an initial F-algebra, we not
only get some A isomorphic to F(A), but a map A --> B for every
map B --> F(B). This gives us "primitive recursion" on A.
However, if we find our initial F-algebra in the category
with only embedding and projection pairs, then we only get an
embedding A --> B for every embedding B --> F(B).
As a result, we can only define embeddings by primitive
recursion on A, not arbitrary (continuous or whatever) functions.
This is the "price" we pay for going from the category we
are really interested in to the category with embedding-projection
pairs. The lack of primitive recursion goes unnoticed in
the category of cpo's with least elements, since we have
fixed point operators and therefore the ability to define
functions by unbounded recursion. However, in the category of
cpo's not necessarily having least elements (and total maps),
this seems to make a difference. This is comforting, I think:
Switching to from abitrary morphisms to embedding-projection
pairs makes every co-contravariant functor covariant.
This simplifies a lot of things. However, you should not be
able to get something for nothing, and so a price should be
paid somewhere.
The rest of this message elaborates this point.
A reference for background is Smyth and Plotkin
"The category-theoretic solution of recursive domain equations",
SIAM J. Computing 11 (1982) 761-783.
A type expression with one
free type variable defines a functor. This functor can
be made covariant, even if it is F(t) = t->t, by going
to the category of projection maps over domains.
To get the recursive type t=F(t), the standard thing
is to find the initial F algebra. An F algebra is a
pair <A,f> where A is an object (of whatever category)
and f:F(A) -> A. The category
of F algebras has morphisms which give commuting
squares. Specifically, h is a morphism from F algebra
<A,f> to <B,g> if h:A --> B such that the square
F(h)
F(A) -------------> F(B)
| |
| |
V V
A ---------------> B
h
commutes. A solution to t=F(t) is then found as an
initial object in the category of F-algebras.
IT is easy to prove that if <A,f> is initial, then f
is an isomorphism. However, the initiality of <A,f> is worth more
than just the fact that f is an isomorphism. Specifically,
initiality means that for any other F algebra <B,g>
there is a unique F-alg morphism from <A,f> to <B,g>.
The map guaranteed by initiality gives a form of
"primitive recursion." For example, if F(t) = 1 + t,
with initial F-algebra
<N,f>, then initiality says that whenever we have a
map g:1+B --> B, there is a map from N to B with the
diagram commuting. A map g:1+B --> B amounts to a
distinguished element g(inl *) from B, and a map
g':B--> B. It is not hard to check that the map h given
by initiality maps 0 to the distinguished element, and maps n+1 to
g'(h(n)). In other words, initiality gives us the
ability to define primitive recursive functions from
the initial F algebra to any other type.
In general, if we have initial F-algebra <A,f> and another
F-algebra <B,g>, the unique F-algebra-morphism from A to B
may be written R(g) as a function of g.
F(R(g))
F(A) -------------> F(B)
| |
f | | g
V V
A ---------------> B
R(g)
In this case, we get the following equation for R:
R(g)(x:A) = g( F(R(g))(f^{-1} x) )
It is easy to see that in the special case that F(X) = 1+X,
this gives the usual equations for a primitive recursion operator,
as in Godel's T.
HOWEVER, if we solve X=F(X) over the category with
embedding-projection pairs, this only makes sense
when g is an embedding.