January 1995 - Categories - categories.org.au

Post-doc in Sydney
by Barry Jay 28 Jan '95

28 Jan '95

The SHAPE project ------------------ Post-doctoral Research Fellowship --------------------------------- The Shape project is developing some exciting new ideas in the semantics of data types so that they can be incorporated into programming languages, especially a parallel language suitable for numerical analysis. The key concept is that data is stored in shapes (or containers, or structures) which can be described and manipulated separately from the data. Expected benefits are: - that programs will be able to act on inputs of arbitrary shape (shape polymorphism); - that shape errors (e.g. array bound errors) can be detected during compilation (shape analysis), and; - that (most) run-time operations will act on arrays. Further information about the theory of shape can be obtained by anonymous ftp from ftp.socs.uts.edu.au in the directory users/cbj in the file shapelyTypes.ps.Z and the sub-directory P2. A prototype functional language is currently under development. When stable, it must be implemented so that it can run on the CM5. In addition to capturing the benefits listed above, shape information may help in optimisation. The UTS team currently has two staff and three graduate students, with additional collaborators in Australia, Canada and Europe. Now, with funding from a large ARC grant, we are looking for a post-doctoral research fellow. The position is for up to three years at a salary range of $42,198 - $43,781. A doctorate in computer science (or its equivalent) is essential. The candidate must be able to make a significant contribution to the project. The ideal candidate will have experience in implementing languages on parallel computers, optimisation of programs for parallel computers, functional programming, or; type theory. The candidate must have initiative, be able to work well as part of a team, and communicate effectively. Address initial enquiries to Barry Jay (cbj(a)socs.uts.edu.au) Responses may be erratic until 6/2/95. Applicants should send a curriculum vitae to: Dr C. Barry Jay School of Computing Sciences, University of Technology, Sydney PO Box 123 Broadway 2007 Australia Ph (6 12) 330-1814 Fax (6 12) 330-1807 before Friday, 24th February, 1995. The position will remain open until it is filled. Barry Jay

1 0

Announce: revision of paper
by Robert A. G. Seely 27 Jan '95

27 Jan '95

We wish to announce the availability (by ftp or WWW) of the following paper (revised version) Natural deduction and coherence for weakly distributive categories by R.F. Blute, J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble ABSTRACT: This paper examines coherence for certain monoidal categories using techniques coming from the proof theory of linear logic, in particular making heavy use of the graphical techniques of proof nets. We define a two sided notion of proof net, suitable for categories like weakly distributive categories which have the two-tensor structure (times/par) of linear logic, but lack a negation operator. Representing morphisms in weakly distributive categories as such nets, we derive a coherence theorem for such categories. As part of this process, we develop a theory of expansion-reduction systems with equalities and a term calculus for proof nets, each of which is of independent interest. In the symmetric case the expansion reduction system on the term calculus yields a decision procedure for the equality of maps for free weakly distributive categories. The main results of this paper are these. First we have proved coherence for the full theory of weakly distributive categories, extending similar results for monoidal categories to include the treatment of the tensor units. Second, we extend these coherence results to the full theory of *-autonomous categories - providing a decision procedure for the maps of free symmetric *-autonomous categories. Third, we derive a conservative extension result for the passage from weakly distributive categories to *-autonomous categories. We show strong categorical conservativity, in the sense that the unit of the adjunction between weakly distributive and *-autonomous categories is fully faithful. NOTES: This is a significant revision of an earlier version announced a year ago. The paper has been completely rewritten, and has been enhanced in several ways: 1) We now treat the cases with non-logical axioms, and with non-commutative tensor and par, in considerable detail, pointing out in passing where the traditional treatment (of the pure commutative case) does not work in these cases. For example, the traditional proof of sequentiality (via splitting links) does not work in the presence of non-logical axioms. 2) We develop a term calculus for proof nets, and a theory of expansion - reduction rewrite systems, both of which are of independant interest. 3) Using this new material has made the proofs clearer and more complete. TO OBTAIN THE PAPER: By ftp: ftp triples.math.mcgill.ca login as anonymous use your email address as password cd pub/rags/nets binary get nets.ps.gz (or nets.dvi.gz if you prefer) (You will have to gunzip this file to get the PostScript - or DVI - file for the paper.) By WWW (Mosaic, netscape, ...) My home page is: ftp://triples.math.mcgill.ca/pub/rags/ragstriples.html click on the item labelled with the paper's title - this will display the PostScript file. (other papers dealing with weakly distributive categories and proof nets may be found easily via my home page.) (If you need to get gunzip, you can find it at pip.shsu.edu: issue the command "quote site index gzip" once you have ftp'd the site to get a list of files suitable for various computer platforms.) = rags =

1 0

CT95 2'nd Announc't; Summer School on Category Theory
by Bob Rosebrugh 25 Jan '95

25 Jan '95

SECOND ANNOUNCEMENT INTERNATIONAL CATEGORY THEORY MEETING (CT95) Canadian Mathematical Society Annual Seminar July 9-15, 1995 Dalhousie University Halifax, Canada PREREGISTRATION IF YOU HAVE NOT ALREADY DONE SO, AND PLAN TO ATTEND THE CONFERENCE, PLEASE PREREGISTER BY FEBRUARY 15, 1995. To preregister, and thus receive detailed information, please send e-mail to ct95(a)cs.dal.ca with subject `preregistration'. Please provide your name and a postal address in the body of the message. (If you do not have access to e-mail, you may write to RJ Wood, Mathematics, Statistics and Computing Science, Dalhousie University, Halifax, Nova Scotia, B3H 3J5, CANADA.) REGISTRATION FEE The conference registration fee is $250(Canadian). Students may register for $125. The registration fee includes lunches during the days of the scientific program, an excursion and a banquet. Tickets for companions to attend any of the events will be available at cost. ACCOMMODATION To request residence accommodation at Dalhousie please send e-mail to ATANNER(a)KILCOM1.UCIS.DAL.CA mentioning CT95. (If you do not have access to e-mail, you may write to Conference Administrator, Conference Services, Dalhousie University, Suite 410, Student Union Building, Halifax, Nova Scotia, B3H 4J2, CANADA.) Rates, including taxes, are $35 nightly/$207 weekly for a single room, $51 nightly/$307 weekly for a double room. Breakfast is included with residence accommodation. Information on hotel accommodations will be included with a future mailing. SCIENTIFIC PROGRAMME Abstracts for talks should be sent to pare(a)cs.dal.ca (or R. Pare, Mathematics, Statistics and Computing Science, Dalhousie University, Halifax, Nova Scotia, B3H 3J5, CANADA) before May 1, 1995. ------------------------------------------------------------------------- FIRST ANNOUNCEMENT CATEGORY THEORY SUMMER SCHOOL June 25-July 8, 1995 Dalhousie University Halifax, Canada In conjunction with CT95, Professors F.W. Lawvere and S. Schanuel will be offering a series of preparatory lectures for graduate students who plan to attend the conference. There is no registration fee for this SUMMER SCHOOL. Student accommodation is $20 nightly/$110 weekly and should be requested from ATANNER(a)KILCOM1.UCIS.DAL.CA (or Conference Administrator, Conference Services, Dalhousie University, Suite 410, Student Union Building, Halifax, Nova Scotia, B3H 4J2, CANADA).

1 0

Preprint Available
by Walter Tholen 24 Jan '95

24 Jan '95

The following paper may be requested from Maria Manuel Clementino (paper or electronic copy) by writing to clementino(a)gemini.ci.uc.pt "Compact objects and perfect morphisms" by M.M. Clementino, E. Giuli and W. Tholen Abstract: In a category with a subobject structure and a closure operator, we provide a categorical theory of compactness and perfectness which yields a number of classical results of general topology as special cases, including the product theorems by Tychonoff and Frolik and the existence of Stone-Cech compactifications, both for spaces and maps. Applications to other categories are also provided.

1 0

is union associative?
by Ilya Beylin 19 Jan '95

19 Jan '95

I suspect that the following question is very natural and a known solution has to exist, but I cannot find any reference in books I have. Consider the following diagram A |a V b W <----- B and define union of two morphisms a U b := Pushout(Pullback(X)) In the category Set this operation is obviously associative: for any arrows a,b,c with common target, a U (b U c) = (a U b) U c , Can anybody tell, what conditions should be imposed to a category to guarantee this associativity? Thank you in advance, Ilya Beylin

2 1

answer to Samson
by Peter Freyd 17 Jan '95

17 Jan '95

As my last paragraph tried to make clear, we can't expect much. If we define Hom(X,Y) as (adj X) tensor Y then the functor A directsum Hom(x,Y) looks as if it ought to have an interesting fixed point. It doesn't.

1 0

neologism
by unknown＠categories.mta.ca 17 Jan '95

17 Jan '95

In answer to the obvious query: yes, I did indeed check the standard sources before I let that word pass. And I decided the standard sources need to be improved. Now I must agree we've lived all these years without feeling the need for yet another adverb that starts out with "there-". The O.E.D. lists 38 of them: thereabout, thereabove, thereafter, thereafterward, thereagain, thereagainst, thereamong, thereat, thereaway, therebefore, therebeside, thereby, theredown, thereforth, therefrom, therehence, therein, thereinto, there-nigh, thereof, thereon, thereout, thereover, therethrough, theretill, thereto, theretofore, theretoward, thereunder, thereuntill, thereunto, thereup, thereupon, thereward, therewhile, therewith, therewithal, therewithin But none of these works as a replacement for "therebetween" in either of the following two lines from my recent missive: the category whose objects are all Hilbert spaces that can be isometrically embedded in A and whose maps are all linear operators therebetween of bound at most 1. the subcategory of all closed subspaces of A and all inclusion maps therebetween. So why not shoot for 39? Best thoughts, Peter

1 0

Hilbert space proof
by Peter Freyd 16 Jan '95

16 Jan '95

On request: Theorem: The category of separable Hilbert spaces and linear operators of bound at most 1 is algebraically compact. More generally, Theorem: Let A be a Hilbert space. Let *A* be the category whose objects are all Hilbert spaces that can be isometrically embedded in A and whose maps are all linear operators therebetween of bound at most 1. Then *A* is algebraically compact. (The axiom of choice says that the objects of *A* can be described as all Hilbert spaces of (orthonormal) dimension bounded by a given cardinal.) The proofs work for both the real and complex cases. For the proof we'll need a few lemmas about *A* and its endofunctors. First note that any isometric embedding B -> C is a retract with the adjoint operator C -> B serving as its right- inverse. Left to the reader is the surprising fact (to me) that right- inverses are unique. So are left-inverses. That is, in *A* every map has at most one right-inverse and one left-inverse and all left- inverses are isometric embeddings and all right-inverses are orthogonal projections. Because any functor preserves the existence of right-inverses we may conclude that any given endofunctor, T, carries isometric embeddings to isometric embeddings. For convenience we'll replace T with a naturally equivalent functor that is invariant on the lattice of subobjects of A (that is, the subcategory of all closed subspaces of A and all inclusion maps therebetween). First choose a single isometric embedding TA -> A. For each A' contained in A define T'A' to be the image of TA' -> TA -> A where TA' -> TA is T applied to the inclusion map A' -> A. Let TA' -> T'A' be the obvious isomorphism. For all objects, B, not contained in A define T'B to be TB and TB -> T'B to be the identity map. Define T' to be the unique endofunctor that turns this collection of isomorphisms into a natural equivalence. For an inclusion map A' -> A we have that T'A' -> T'A is an inclusion map. And from that we may conclude that any inclusion map between subobjects of A is carried by T' to an inclusion map. We'll drop the dash-mark on T and notationally assume that our given functor preserves the lattice of subobjects of A. At this point it is clear (a la Tarski) what the initial T-algebra must be: any endofunctor on a complete lattice has a minimal fixed point, indeed, to domain theorists (a CS term) it is clear how to prove it to be the initial T-algebra: start by using the bottom-up construction for the minimal fixed-point for T as it operates on the lattice of subobjects of A. Define an ordinal sequence of subspaces of A as follows: for a limit ordinal 'a, take F['a] to be the supremum of the previous values; for a successor ordinal 1+'b take F[1+'b] to be T(F['b]). Note that for the limit ordinal 0 we have that F[0] is the trivial (one-element) subspace. And note that for all other limit ordinals, 'a, we have that F['a] is the closure of the union of the previous values. By an inductive argument this sequence is an increasing sequence (but, of course, not forever strictly increasing): for a limit ordinal 'a, we have that F['b] < F['a] for all 'b < 'a (using < for the containment sign) hence T(F['b]) < T(F['a]) that is, F[1+'b] < F[1+'a] for all 'b < 'a and the construction of F['a] forces F['a] < T(F['a]) = F[1+'a]; for a successor ordinal 1+'b we may (inductively) assume that F['b] < F[1+'b] hence T(F['b]) < T(F[1+'b]), that is, F[1+'b] < F[1+1+'b]. The sequence can not forever be strictly increasing. It stabilizes at a value F. We take 'c as the first limit ordinal such that F = F['c]. We need that F is not just the supremum of the constructing sequence as defined in the lattice but its colimit as defined in the entire category. Actually we need the general fact that for any limit ordinal 'a it is the case that F['a] is the colimit of the ordinal diagram of previous values. The proof is straigh- forward using again the fact that the maps in the category are of bound at most 1.) Given a T-algebra b:TB -> B we must construct a map x:F -> B so that F Tx / \ x TB -> B b (add downward arrowheads). We define, inductively, a sequence of maps x['b]:F['b] -> B such that x['b] T(x['b]) b F['b] -----> B = F['b] -> F[1+'b] --------> FB -> B where the unlabeled map is the inclusion map. For successor-ordinals define x[1+'b] as T(x['b]) b F[1+'b] --------> FB -> B. The inductive verification that x[1+'b] T(x[1+'b]) b F[1+'b] -------> B = F[1+'b] -> F[1+1+'b] ----------> FB -> B is straight-forward diagram chasing. For limit-ordinals define x['a]:F['a] -> B using the fact that F['a] is a colimit of the previous values. For the verification of x['a] T(x['a]) b F['a] -----> B = F['a] -> F[1+'a] --------> FB -> B it suffices to verify, for each 'b < 'a, that x['a] T(x['a]) b F['b] -> F['a] -----> B = F['b] -> F['a] -> F[1+'a] --------> FB -> B where, just as before, each unlabeled arrow is an inclusion map. This follows, inductively, from the two equations x['a] x['b] F['b] -> F['a] -----> B = F['b] -----> B, and F['b] -> F['a] -> F[1+'a] = F['b] -> F[1+'b] -> F[1+'a] where the last map (still an inclusion map) is the result of applying T to the inclusion map from F['b] to F['a]. The uniqueness can be verified, inductively, for each 'b. Alternatively, given a possibly different solution y:F -> B, let A' be the equalizer of x and y using the standard construction: A' is the closed subspace of points on which x and y agree. It follows that T(A') is contained in A', that is, A' is a "prefixed point" of T. But -- as is clear from the top-down construction -- minimal fixed points are automatically minimal prefixed points and F must be contained in A'. We have shown that T has an initial algebra (that is, the category is algebraically complete). Since the category is self-dual (via the adjoint-operator construction) it follows that T also has a final co-algebra (that is, the category is algebraically co-complete). But for compactness we need the two to be naturally isomorphic. We have reduced to the case that the structure map on the initial algebra is the identity map which means that the naturally isomorphic co-algebra is given by the same identity map. That is, we must show for every b:B -> TB the existence of a unique x:B -> F such that (add downward arrowheads) b B -> TB x \ / Tx F. F is not just the colimit of the ordinal sequence of inclusion maps, it's the limit of the ordinal sequence of their adjoint operators, the orthogonal projections. The comments at the very beginning, that T necessarily preserves the unique right-inverses, says that this ordinal sequence of orthogonal projections has all the requisite properties for the (dual) of the proof we've just seen. Done. Having done all this I must now note that my original purpose for algebraic compactness has been frustrated: the fact that contravariant functors and mixed-variance functors have minimal invariant objects was already evident for this category. I'm refering to the general theorem that given any algebraically compact category and "sesqui"- endofunctor, TXY, contravariant on X, covariant on Y, there's a T-invariant object, that is, an object F together with an isomorphism from TFF to F; indeed there is a _minimal_ T-invariant object, that is, one that appears uniquely as a natural retract of every T-invariant object. The trouble is that if we replace TXY with TX'Y, where X' denotes the adjoint-operator functor (which, note, is the identity operation on objects) then it's easy to see that the intial algebra of TX'Y is as desired. That is, algebraic completeness is enough when in the presence of an anti-involution that fixes identity maps. Peter Freyd

3 2

Book on Curry-Howard Isomorphism
by Charles Wells 13 Jan '95

13 Jan '95

I believe there is a new book out on the Curry-Howard Isomorphism, but I have lost the announcement. If someone can give me the details, I would like to order it for the CWRU library. Thanks, -- Charles Wells Department of Mathematics, Case Western Reserve University 10900 Euclid Avenue, Cleveland, OH 44106-7058, USA 216 368 2893

1 0

algebraically compact categories
by Peter Freyd 10 Jan '95

10 Jan '95

When I first introduced the notions of algebraically complete categories (every endo-functor has an initial algebra) and algebraically compact categories (every endo-functor has an initial algebra naturally isomorphic to a terminal co-algebra) I thought that such things would exist in the classical foundations only in degenerate form. It was a surprise when I noticed that the categories of countable sets and of countably dimensioned vector spaces are algebraically complete. I'm now surprised by: The category of separable Hilbert spaces and linear operators of bound at most 1 is algebraically compact. As in the earlier cases one doesn't really need the controlling cardinal number to be aleph-naught. To avoid using the axiom of choice one can state the more general result by taking an arbitrary Hilbert space A and defining *A* by: Objects of *A*: all those Hilbert spaces that can be isometrically embedded in A; Maps of *A*: all linear operators thereon of bound at most 1. Then: *A* is algebraically compact. The theorem holds for both the real and complex cases. In the proof I use the surprising (to me) fact that in the categories in question every half-invertible map has a _unique_ half-inverse. (That is, every map has at most one left-inverse and one right- inverse.) All the other examples from nature that I can think of are categories in which the only half-invertibles are invertible. Are there others? Peter Freyd

1 0