Does there exist a comprehensive treatment of the category Pfn, objects are sets and morphisms are partial functions - specifically I`m interested to know if someone has proven the existence of colimits and other such concepts in Pfn. Thanks, Lars Birkedal (birkedal@diku.dk) =====================================================================
Mike Barr gave a particularly lucid answer to the question of Lars Birkedale about limits and colimits in Pfn: it is complete and cocomplete since it is the category of algebras for a triple. The only problem with this answer is that it fails to take account of the natural ordering of partial functions (by extension) which is often of great importance to computer scientists. The difficulties can be seen with the binary product in Pfn. The product of two sets A and B in Pfn is given by A+(A\x B)+B whose three components represent pairs (x,y) in which at least one of x and y is defined. The problem is that if x<x' and y<y' then it doesn't follow that (x,y)<(x'y') since the two pairs may both be defined but take values in different components of the product. Turning this result around, it is clear that any notion of product whose pairing *does* preserve the order cannot be the cartesian product in the usual sense. Let us re-examine the product from Sets in this context. First of all it is a local cartesian product. That is, given partial functions f:C-> A and g:C-> B there is a pair (f,g):C->AxB whose domain of definition is the intersection of those of f and g. Let p and q be the projections of the product onto A and B respectively. Then (writing < for less-than-or-equals) we have p.(f,g) < f q.(f,g) < g If p.h < f and q.h < g then h < (f,g). This is enough to determine h uniquely, but it does not determine the object AxB. After all, the empty set would do instead! In order to capture AxB one must consider its properties in relation to the total functions. This would be almost tautologous except that it is possible to define the total morphisms in any ordered category, and so specify the total functors, natural transformations, adjoints etc, so that the products arise naturally from the general theory. Details can be found in my tech. report LFCS 90-107 Extending properties to categories of partial maps Total pullbacks, pushouts, etc can all be defined but have yet to be tested against real problems. Perhaps Lars can help here. Barry Jay ===================================================================
participants (2)
-
cbj@dcs.edinburgh.ac.UK -
Lars Birkedal