Date: Mon, 4 Jul 1994 11:48:49 +0500 (GMT+4:00) Subject: Computing: the Australian Theory Seminar (CATS) Date: Mon, 4 Jul 1994 10:39:19 +1000 From: Barry Jay Computing: the Australian Theory Seminar (CATS) Sydney 17th-19th December, 1994 PRELIMINARY ANNOUNCEMENT CATS will be open to all aspects of the theory of computer science. It will provide an opportunity for the scattered community of computing theorists in Australia and New Zealand to meet and exchange views in an informal setting. The following people have already expressed an interest in coming. Robin Cockett (Calgary) Eugenio Moggi (Genoa) Maurice Nivat (France) Phil Wadler (Glasgow) The format would be informal, with an easy balance between lectures and discussions: registration costs will be kept low. Please reply NOW if you are interested in coming. Further details will be supplied when approximate numbers can be gauged. Please distribute this announcement widely. Barry Jay University of Technology, Sydney Australia cbj@socs.uts.edu.au Date: Tue, 5 Jul 1994 08:52:38 +0500 (GMT+4:00) Subject: Re: Birkhoff variety theorem Date: Mon, 4 Jul 94 09:01:23 EDT From: Michael Barr I have been away and then too busy to examine my mail in detail. I don't think I have such a result. However, it is likely that John Power's thesis has something on that. He is in Edinburgh, but is aliased on this machine[moderator note: `this machine'=`triples.math.mcgill.ca'], so you can write him here. Date: Tue, 5 Jul 1994 08:54:41 +0500 (GMT+4:00) Subject: Categorical completeness results for the simply-typed lambda calculus. Date: Mon, 04 Jul 94 18:35:50 +0100 From: Alex Simpson 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@dcs.ed.ac.uk LFCS, Dept. of Computer Science, University of Edinburgh, Edinburgh EH9 3JZ, UK. Tel: +44 (0)31 650 5113 Date: Tue, 5 Jul 1994 22:18:48 +0500 (GMT+4:00) Subject: ANNOUNCE: XY-pic version 2.11 released... Date: Tue, 5 Jul 1994 13:45:28 +0200 From: kris@diku.dk Dear CATEGORY THEORY COMMUNITY, [Thank you for all the positive replies ... so this time I'll only ask those who do NOT wish news about XY-pic or who get it from other sources to send me an email saying so :-] This is to announce yet another BUG FIX release of my DIAGRAM DRAWING PACKAGE, XY-pic: version 2.11. It fixes the following user visible bugs in version 2.10: * Arrow tips were reversed in a few cases (thanks to Clemens Beckstein for finding this (also)). * Repeated labels on arrows now works. * The PostScript backend sometimes did curves wrong; this is fixed. Futhermore it adds a new `Graph Combinator feature' which is specially designed for enterting diagrams with graph structure. Please test it and comment on it. Please retrieve the new version by anonymous ftp from ftp.diku.dk : /diku/users/kris/TeX ftp.mpce.mq.edu.au : /pub/maths/TeX or the CTAN `macros/generic/diagrams/xypic' mirror which will be up to date in a day or so. Regards, Kristoffer Rose -- Kristoffer Ho/gsbro ROSE Internet: kris@diku.dk DIKU, U of Copenhagen, Universitetsparken 1, 2100 Ko/benhavn O/, DANMARK phone: +45 35321400 direct: +45 35321420 fax: +45 35321401 -- W3 home Date: Wed, 6 Jul 1994 21:48:51 +0500 (GMT+4:00) Subject: Re: Categorical completeness results for the simply-typed lambda calculus. Date: Wed, 6 Jul 94 14:25:55 EDT From: Djordje Cubric I would like to make ``a point of an empty set'' and say that Friedman's completeness theorem for typed lambda calculus (with appropriate changes) implies the completeness result for free cartesian closed categories (as mentioned in a recent posting of Alex Simpson) provided that one proves first that in a free ccc all objects have a global support. One way to do that is to prove the confluence for the appropriate system of reductions. Some of the recent papers were dealing with these reductions. One can see that the completeness holds even when the free ccc has also free arrows among freely generated types. Djordje Cubric Date: Thu, 7 Jul 1994 11:24:43 +0500 (GMT+4:00) Subject: Revised version of Acyclic models Date: Thu, 7 Jul 94 09:02:39 EDT From: Michael Barr 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 Date: Thu, 7 Jul 1994 21:51:43 +0500 (GMT+4:00) Subject: Re: Empty types and typed lambda calculus Date: Thu, 07 Jul 94 09:37:26 -0700 From: "John C. Mitchell" 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 Date: Mon, 11 Jul 1994 21:39:03 +0500 (GMT+4:00) Subject: Conference: Category Theory and Computer Science (CTCS) Date: Mon, 11 Jul 94 11:39:36 BST From: David Rydeheard 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. ------------------------------------------------------------------------------- Date: Tue, 19 Jul 1994 13:38:24 +0500 (GMT+4:00) Subject: Re: Anouncement of Preprints Date: Tue, 19 Jul 1994 16:33:59 +1000 From: Murray Adelman 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 Date: Tue, 19 Jul 1994 13:37:10 +0500 (GMT+4:00) Subject: E-M factorization system question Date: Mon, 18 Jul 1994 20:35:02 -0700 From: "William H. Rowan" 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 Date: Tue, 26 Jul 1994 09:07:58 +0500 (GMT+4:00) Subject: New edition of "Category Theory for Computing Science" Date: Mon, 25 Jul 1994 14:13:54 -0400 From: "Charles F. Wells" 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@triples.math.mcgill.ca cfw2@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 Date: Tue, 26 Jul 1994 09:03:03 +0500 (GMT+4:00) Subject: characterization of geometric morphisms of the form Pi_I ?? Date: Wed, 20 Jul 94 20:32:52 +0200 From: Thomas Streicher 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 Date: Tue, 26 Jul 1994 09:13:08 +0500 (GMT+4:00) Subject: Papers Date: Sat, 23 Jul 1994 11:53:22 +1000 From: Murray Adelman 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 Date: Tue, 26 Jul 1994 09:05:46 +0500 (GMT+4:00) Subject: second call for papers, TLCA Date: Thu, 21 Jul 1994 14:16:59 +0000 From: Philippa Gardner 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@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@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}