July 1994 - Categories - categories.org.au

New edition of "Category Theory for Computing Science"
by Charles F. Wells 26 Jul '94

26 Jul '94

We are revising our text, "Category Theory for Computing Science", for its second edition. We would appreciate any comments or suggestions concerning this revision, including papers and books we should refer to, new topics we should include, and topics we could delete. Please reply to either of us. Michael Barr Charles Wells barr(a)triples.math.mcgill.ca cfw2(a)po.cwru.edu -- Charles Wells, Department of Mathematics, Case Western Reserve University 10900 Euclid Avenue, Cleveland OH 44106-7058, USA Phone 216 368 2880 or 216 774 1926 FAX 216 368 5163

1 0

Papers
by Murray Adelman 23 Jul '94

23 Jul '94

There seems to be some problem obtaining the papers that I announced a few days ago. I have put them in a second location ftp.mpce.mq.edu.au in the directory /pub/maths/murray (This is more patriotic, as it is the Macquarie University server instead of the Sydney University server :-) Sorry for the inconvenience. Murray

1 0

second call for papers, TLCA
by Philippa Gardner 22 Jul '94

22 Jul '94

Please find enclosed the second call for papers for TLCA'95. I apologise to those who receive many copies of this announcement. Philippa Gardner --------------------------------------------------------------- Second Call for Papers, TLCA International Conference on Typed Lambda Calculi and Applications April 10--12, 1995, Edinburgh, Scotland The second international conference on Typed Lambda Calculi and Applications will be held April 10--12, 1995, at Edinburgh in Scotland. The conference aims at providing a forum for the presentation and discussion of recent research in the following areas: Proof theory of type systems Logic and type systems Typed lambda calculi as models of (higher order) computation Semantics of type systems Proof verification via type systems Type systems of programming languages Typed term rewriting systems The program of TLCA will consist of about 30 selected presentations in plenary sessions. The program committee for TLCA is chaired by M. Dezani and has the following members: H. Barendregt (Catholic University of Nijmegen) M. Dezani (Chairperson, University of Turin) J-Y. Girard (University of Marseilles) R. Hindley (University of Swansea) F. Honsell (University of Udine) J. W. Klop (CWI) G. Longo (ENS) A. Meyer (MIT) G. Plotkin (University of Edinburgh) P. Scott (University of Ottawa) J. Smith (University of Gothenburg/Chalmers) J. Tiuryn (University of Warsaw) Call for Papers Original contributions are solicited for TLCA; they should be sent to the conference secretariat. Electronic submission (PostScript only) is preferred; hard copy (6 copies required) will also be accepted. Papers should be clearly written and allow the program committee to assess the merits of the work. References and comparisons with related work should be included. Papers should not exceed 15 standard pages and should be accompanied by a one-page abstract. The deadline for submissions is September 8, 1994. Authors will receive notification of acceptance by November 12, 1994. Definitive versions of papers will be due December 15, 1994. Proceedings It is intended to publish the accepted papers as a volume of the Springer Verlag Lecture Notes in Computer Science series. Organizing Committee G. Cleland, P. Gardner, M. Lekuse, G. Plotkin (University of Edinburgh) Important Dates Sept. 8, 1994 Deadline for submissions Nov. 12, 1994 Notification of acceptance Dec. 15, 1994 Final version of paper April 10, 1995 TLCA TLCA Secretariat TLCA Secretariat Professor M. Dezani Universita di Torino Dipartimento di Informatica Corso Svizzera, 185 10149 Torino ITALY Tel: 39-11-7429232 Fax: 39-11-751603 Email: dezani(a)di.unito.it Lambda-Calculus Network Meeting Participants of TLCA are welcome to attend a Lambda-Calculus Network Meeting to be held immediately before the conference. ------------------------------------------------------------- \documentstyle{article} \parindent 0cm \pagestyle{empty} \textwidth 18cm \textheight 28cm \topmargin -2.5cm \oddsidemargin -1.2cm \evensidemargin 0cm \begin{document} \begin{center} {\LARGE Second Call for Papers} \end{center} \smallskip \begin{center} {\Huge Second International Conference on} \end{center} \begin{center} {\Huge Typed Lambda Calculi and Applications} \end{center} \begin{center} {\Huge TLCA} \end{center} \smallskip \begin{center} {\Large April 10--12, 1995, Edinburgh, Scotland} \end{center} \bigskip The second international conference on Typed Lambda Calculi and Applications will be held April 10--12, 1995, at Edinburgh in Scotland. The conference aims at providing a forum for the presentation and discussion of recent research in the following areas:\vspace{-1cm} \begin{itemize}\begin{center} \item[] \bf Proof theory of type systems \\ \item[] \bf Logic and type systems \\ \item[] \bf Typed lambda calculi as models of (higher order) computation \\ \item[] \bf Semantics of type systems \\ \item[] \bf Proof verification via type systems \\ \item[] \bf Type systems of programming languages \\ \item[] \bf Typed term rewriting systems \end{center} \end{itemize} \bigskip \begin{minipage}[t]{8.5cm} {\large \bf Program} \smallskip The program of TLCA will consist of about 30 selected presentations in plenary sessions. The program committee for TLCA is chaired by M.~Dezani and has the following members: \smallskip {\bf H.~Barendregt}~(Catholic University of Nijmegen) \\ {\bf M.~Dezani}~(Chairperson, University of Turin) \\ {\bf J-Y.~Girard}~(University of Marseilles) \\ {\bf R.~Hindley}~(University of Swansea) \\ {\bf F.~Honsell}~(University of Udine) \\ {\bf J.~W.~Klop}~(CWI) \\ {\bf G.~Longo}~(ENS) \\ {\bf A.~Meyer}~(MIT) \\ {\bf G.~Plotkin}~(University of Edinburgh) \\ {\bf P.~Scott}~(University of Ottawa) \\ {\bf J.~Smith}~(University of Gothenburg/Chalmers) \\ {\bf J.~Tiuryn}~(University of Warsaw) \\ \smallskip {\large \bf Call for Papers} \smallskip Original contributions are solicited for TLCA; they should be sent to the conference secretariat. Electronic submission (PostScript only) is preferred; hard copy (6 copies required) will also be accepted. Papers should be clearly written and allow the program committee to assess the merits of the work. References and comparisons with related work should be included. Papers should not exceed 15 standard pages and should be accompanied by a one-page abstract. The deadline for submissions is September 8, 1994. Authors will receive notification of acceptance by November 12, 1994. Definitive versions of papers will be due December 15, 1994. \end{minipage} \hspace{1cm} \begin{minipage}[t]{8.5cm} {\large \bf Proceedings} \smallskip It is intended to publish the accepted papers as a volume of the Springer Verlag Lecture Notes in Computer Science series.\smallskip\\ {\large \bf Organizing Committee} \smallskip {\bf G.~Cleland, P.~Gardner, M.~Lekuse, G.~Plotkin} \\(University of Edinburgh) \\ {\large \bf Important Dates} \smallskip \vspace{-0.25cm}\begin{tabbing} abcdefghijklmnop\=abcdefghijklmnop\kill Sept. 8, 1994 \>Deadline for submissions \\ Nov. 12, 1994 \>Notification of acceptance \\ Dec. 15, 1994 \>Final version of paper \\ April 10, 1995 \>TLCA \end{tabbing} \vspace{0.1cm}\smallskip {\large \bf TLCA Secretariat} \smallskip TLCA Secretariat \\ Professor M.~Dezani \\ Universit\'{a} di Torino \\ Dipartimento di Informatica \\ Corso Svizzera, 185\\ 10149 Torino \\ ITALY\\ Tel: 39-11-7429232~~Fax: 39-11-751603\\ Email: dezani(a)di.unito.it \\ {\large \bf $\lambda$-Calculus Network Meeting} \smallskip Participants of TLCA are invited to attend a $\lambda$-Calculus Network Meeting to be held in the weekend before the conference. \end{minipage} \end{document}

1 0

characterization of geometric morphisms of the form Pi_I ??
by Thomas Streicher 21 Jul '94

21 Jul '94

I would like to know whether somebody knows of an abstract characterization of those geometric morphisms (between elementary toposes) which are of the form Pi_I : E/I -> E for some I in E ? My - maybe misleading - intuition is that a topos is a generalized locale and the functor I* : E -> E/I corresponds to the locale morphisms corresponding to open subspace inclusions. (If L is a locale and x is in L then the mapping y |-> x inf y from L to { z : L | z less or equal x } is the locale morphism corresponding to the open subspace inclusion of the open subset given by x into the space given by L). Maybe it is also wrong to think of a topos simply as generalized locale and that the "generalized locale" is given by the fibration Sub(E) -> E and not by the fibration cod : Map(E) -> E . What I know about open geometric morphisms seems to confirm this latter viewpoint. So I am a bit confused and would appreciate any hints ! Thomas Streicher

1 0

Re: Anouncement of Preprints
by Murray Adelman 19 Jul '94

19 Jul '94

I have mounted four papers by John Corbett and myself that attempt to use sheaf theory to interpret Quantum Logic (or our version thereof) on the Sydney University ftp site. They are called Adelman-Corbett.ps ---Long with a lot of expository material for physicists. comparison.ps---Attempts to compare Birkhoff and vonNeumann Quantum logic to the internal logic of the category of sheaves over state space newpaper.ps--- Attempts to show how continuous data can become discrete data via the global sections functor heidelberg.ps---Derives a formula for interference of particles that allows more of the configuration of the experiment to be parametrized than the usual Hilbert Space description. The union of heidelberg.ps and comparison.ps approximates (and perhaps supersedes) Adelman-Corbett.ps which is somewhat older. They can be obtained by anonymous ftp from maths.su.oz.au in the directory sydcat/papers/murray Regards, Murray

1 0

E-M factorization system question
by William H. Rowan 19 Jul '94

19 Jul '94

I am working on a construction which, given a category with an E-M factorization system (such as onto-oneone functions in the category of sets or universal algebras of a given type) provides an embedding F:A --> B where A is the given category, and F embeds A fully into B. B also has an E-M factorization system. However, if a is an object of A, then the e's of Fa are exactly all filters in the lattice of e's of a in A, and the m's of Fa are exactly all filters in the lattice of m's of a in A. The question, of course, is, has this been done by anyone before and if so, please provide a reference to that work. whr

1 0

Conference: Category Theory and Computer Science (CTCS)
by David Rydeheard 11 Jul '94

11 Jul '94

Preliminary Announcement and Call for Papers ------------------------------------------------------------------------ CATEGORY THEORY AND COMPUTER SCIENCE CTCS-6 7th-11th August 1995 University of Cambridge, UK. ------------------------------------------------------------------------ The sixth of the biennial conferences on Category Theory and Computer Science is to be held in Cambridge in 1995, in conjunction with the third Cambridge Summer Meeting in Category Theory. The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory, algebra, geometry and logic. Whilst the emphasis is upon applications of category theory, it is recognised that the area is highly interdisciplinary and the organising committee welcomes submissions in related areas. Topics central to the conference include: Models of computation Program logics and specification Type theory and its semantics Domain theory Linear logic and its applications Categorical programming Submissions purely on category theory are also acceptable as long as the applicability to computing is evident. Previous meetings have been held in Guildford (Surrey), Edinburgh, Manchester, Paris and Amsterdam. It is anticipated that the proceedings will be published by Springer in the LNCS series. IMPORTANT DATES Submission of papers February 1, 1995 Notification of acceptance April 14, 1995 Final papers due June 1, 1995 SUBMISSION OF PAPERS. Authors should send 5 hard copies of a draft paper (maximum of 20 pages) to Dr. David Pitt, Department of Mathematical and Computing Sciences, University of Surrey, Guildford, Surrey, GU2 5XH, United Kingdom. LOCAL ARRANGEMENTS Dr. Peter Johnstone, Department of Pure Mathematics and Mathematical Statistics, 16 Mill Lane, Cambridge, CB2 1SB, United Kingdom. Registration forms for the joint conference will be available nearer to the date. Organising and programme committee: S. Abramsky, P.-L. Curien, P. Dybjer, P. Johnstone, G. Longo, G. Mints, J. Mitchell, E. Moggi, D. Pitt, A. Pitts, A. Poigne, D. Rydeheard, F-J. de Vries, E. Wagner. -------------------------------------------------------------------------------

1 0

Re: Empty types and typed lambda calculus
by John C. Mitchell 08 Jul '94

08 Jul '94

We looked into this kind of thing about seven or eight years ago. See @inproceedings( mmms87, author="A. R. Meyer and J. C. Mitchell and E. Moggi and R. Statman", Key="MMMS 87", Title="Empty types in polymorphic lambda calculus", Booktitle="Proc. 14th ACM Symp. on Principles of Programming Languages", Month="January",Year="1987", pages="253-262", Note="Reprinted with minor revisions in {\it Logical Foundations of Functional Programming,} ed. G. Huet, Addison-Wesley (1990) 273--284.") @article( mm87, author="Mitchell, J.C. and Moggi, E.", Title="Kripke-style models for typed lambda calculus", Journal="Ann. Pure and Applied Logic", Volume="51",Year="1991", pages="99--124", Note="Preliminary version in {\it Proc. IEEE Symp. on Logic in Computer Science,} 1987, pages 303--314.") @incollection( MitchScott,Author="Mitchell, J.C. and Scott, P.J.", Title="Typed lambda calculus and cartesian closed categories", Booktitle="Categories in Computer Science and Logic, Proc. Summer Research Conference, Boulder, Colorado, June, 1987", Series="Contemporary Mathematics", volume="92", publisher="Amer. Math. Society", editors="J.W. Gray and A. Scedrov", Year="1989", pages="301-316") Friedman's completeness theorem is completeness of beta,eta for full classical model (i.e., Set). Deductive completeness fails for Set and for models (interpretations into categories) where every type (every object named by a type expression) is required to be non-empty (have a global element). I tried to clarify this in my book (still to appear). If anyone is seriously interested, I could email the appropriate sections of the book. John Mitchell

1 0

Revised version of Acyclic models
by Michael Barr 07 Jul '94

07 Jul '94

A totally revised version of Acyclic models is now available for ftp on my directory on triples. .tex, .dvi and .ps versions are there. Michael

1 0

Categorical completeness results for the simply-typed lambda calculus.
by Alex Simpson 07 Jul '94

07 Jul '94

I would like to know if the results below are folklore. They don't seem to be, as some recent papers have given lengthy proofs of special cases. On the other hand, they do follow rather easily from an old result due to Statman. The results concern two categorical notions of completeness for beta-eta conversion relative to the interpretation of the simply-typed lambda-calculus in cartesian closed categories. Let C be any CCC (not necessarily with finite limits). Let I_X be the initial CCC generated by a nonempty set X of objects. We say that beta-eta conversion has a COMPLETE INTERPRETATION IN C if there is a faithful CC-functor from I_X to C. We say that beta-eta conversion is COMPLETE FOR C if the class of all CC-functors from I_X to C is collectively faithful. (REMARK. These two definitions do not depend upon X as there is a faithful CC-functor from C_X to C_1, where 1 is a singleton set.) EXAMPLES. One category in which beta-eta conversion has a complete interpretation is the category of sets. (This essentially follows from Friedman's completeness theorem. The inclusion of product types makes no significant difference. This latter remark also applies below, e.g. to the quoted Statman theorem.) It is clear that if beta-eta conversion has a complete interpretation in any C then it is also complete for C. The converse does not hold: the category of finite sets is complete but has no complete interpretation. (That it has no complete interpretation was observed by Friedman. That it is complete essentially follows from the Plotkin/Statman finite model theorem.) Finally, for a trivial example of a C for which beta-eta conversion is not complete, take C to be any cartesian closed preorder. The results give necessary and sufficient conditions on C for the two forms of completeness to hold. THEOREM 1. Beta-eta conversion has a complete interpretation in C iff C has an endomorphism all of whose iterates are distinct. THEOREM 2. Beta-eta conversion is complete for C iff C is not a preorder. Just some brief comments on the proofs. The stronger result is Theorem 1. Theorem 2 can be derived from it by showing that if C is not a preorder then C^omega (the countably infinite power of C) has a "non-repeating" endomorphism as required by Theorem 1. Theorem 2 can also be proved by mimicking the full type hierarchy over a finite set within C, or alternatively by using Statman's characterization of beta-eta conversion as a maximal congruence relation on closed terms satisfying "typical ambiguity". Theorem 1 is proved using a different Statman result. We use sigma to range over types defined using exponentials and finite products from one base type, 0. We use L,M,N to range over closed terms in the simply-typed lambda-calculus with types as above. We use =be for beta-eta equality between terms. Define the type T = (0 -> 0 -> 0) -> (0 ->0). THEOREM (Statman [1]). For any sigma there is an L of type sigma -> T such that, for all M, N of type sigma, M =be N iff L(M) =be L(N). To prove Theorem 1, let a: A --> A be a non-repeating endomorphism in C. One defines a CC-functor, F, from I_{0} to C by setting: F(0) = (A -> A) -> (A -> A). One can show that F is faithful on the hom-set I_{0}(1,T) (by encoding binary trees as Church numerals in F(0)). It follows from Statman's theorem above that F is faithful. [1] Statman, R. On the existence of closed terms in the typed lambda-calculus I. In Hindley, J. R. and Seldin, J. P. eds. To H. B. Curry Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press. 1980. ----------------------------------------------------------------------------- Alex Simpson email: Alex.Simpson(a)dcs.ed.ac.uk LFCS, Dept. of Computer Science, University of Edinburgh, Edinburgh EH9 3JZ, UK. Tel: +44 (0)31 650 5113

2 1