From MAILER-DAEMON Sun Jan 2 10:17:22 2000 Date: Sun, 2 Jan 2000 10:17:22 -0400 (AST) From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA X-IMAP: 0946343086 0000000022 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From cat-dist Wed Dec 1 17:47:45 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA15177 for categories-list; Wed, 1 Dec 1999 16:38:02 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from localhost (tac@localhost) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id VAA14233; Tue, 30 Nov 1999 21:35:25 -0400 (AST) Date: Wed, 1 Dec 1999 11:45:10 -0400 (AST) From: Bob Rosebrugh To: Categories Subject: categories: The Lambek Festschrift: Theory and Applications of Categories Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 1 The Editors of Theory and Applications of Categories are pleased to announce the publication of a special volume dedicated to Joachim Lambek in honour of his 75'th birthday. In addition to the articles abstracted below, the volume includes an Introduction by the guest Editors and a brief biographical essay presented by Michael Barr to the conference held at McGill University on December 5, 1997 in celebration of the same event. The Editors of TAC wish to thank Michael Barr, Philip Scott and Robert Seely who acted as guest editors for this special volume. Abstracts of the articles follow. The journal may be viewed from www.tac.mta.ca/tac/ ------------------------------------------------------------------------- *-Autonomous categories: once more around the track Michael Barr This represents a new and more comprehensive approach to the *-autonomous categories constructed in the monograph [Barr, 1979]. The main tool in the new approach is the Chu construction. The main conclusion is that the category of separated extensional Chu objects for certain kinds of equational categories is equivalent to two usually distinct subcategories of the categories of uniform algebras of those categories. Theory and Applications of Categories, Vol. 6, 1999, No. 1, pp 5-24 http://www.tac.mta.ca/tac/volumes/6/n1/n1.dvi http://www.tac.mta.ca/tac/volumes/6/n1/n1.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n1/n1.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n1/n1.ps ------------------------------------------------------------------------- A bicategorical approach to static modules Renato Betti The purpose of this paper is to indicate some bicategorical properties of ring theory. In this interaction, static modules are analyzed. Theory and Applications of Categories, Vol. 6, 1999, No. 2, pp 25-32 http://www.tac.mta.ca/tac/volumes/6/n2/n2.dvi http://www.tac.mta.ca/tac/volumes/6/n2/n2.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n2/n2.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n2/n2.ps ------------------------------------------------------------------------- The categorical theory of self-similarity Peter Hines We demonstrate how the identity $N\otimes N \cong N$ in a monoidal category allows us to construct a functor from the full subcategory generated by $N$ and $\otimes$ to the endomorphism monoid of the object $N$. This provides a categorical foundation for one-object analogues of the symmetric monoidal categories used by J.-Y. Girard in his Geometry of Interaction series of papers, and explicitly described in terms of inverse semigroup theory in [6,11]. This functor also allows the construction of one-object analogues of other categorical structures. We give the example of one-object analogues of the categorical trace, and compact closedness. Finally, we demonstrate how the categorical theory of self-similarity can be related to the algebraic theory (as presented in [11]), and Girard's dynamical algebra, by considering one-object analogues of projections and inclusions. Theory and Applications of Categories, Vol. 6, 1999, No. 3, pp 33-46 http://www.tac.mta.ca/tac/volumes/6/n3/n3.dvi http://www.tac.mta.ca/tac/volumes/6/n3/n3.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n3/n3.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n3/n3.ps ------------------------------------------------------------------------- A Note on Rewriting Theory for Uniqueness of Iteration M. Okada and P. J. Scott Uniqueness for higher type term constructors in lambda calculi (e.g. surjective pairing for product types, or uniqueness of iterators on the natural numbers) is easily expressed using universally quantified conditional equations. We use a technique of Lambek [18] involving Mal'cev operators to equationally express uniqueness of iteration (more generally, higher-order primitive recursion) in a simply typed lambda calculus, essentially Godel's T [29,13]. We prove the following facts about typed lambda calculus with uniqueness for primitive recursors: (i) It is undecidable, (ii) Church-Rosser fails, although ground Church-Rosser holds, (iii) strong normalization (termination) is still valid. This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system. Theory and Applications of Categories, Vol. 6, 1999, No. 4, pp 47-64 http://www.tac.mta.ca/tac/volumes/6/n3/n3.dvi http://www.tac.mta.ca/tac/volumes/6/n3/n3.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n3/n3.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n3/n3.ps ------------------------------------------------------------------------- Contravariant Functors on Finite Sets and Stirling Numbers Robert Pare Contravariant Functors on Finite Sets and Stirling Numbers We characterize the numerical functions which arise as the cardinalities of contravariant functors on finite sets, as those which have a series expansion in terms of Stirling functions. We give a procedure for calculating the coefficients in such series and a concrete test for determining whether a function is of this type. A number of examples are considered. Theory and Applications of Categories, Vol. 6, 1999, No. 5, pp 65-76 http://www.tac.mta.ca/tac/volumes/6/n5/n5.dvi http://www.tac.mta.ca/tac/volumes/6/n5/n5.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n5/n5.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n5/n5.ps ------------------------------------------------------------------------- Comparing coequalizer and exact completions M. C. Pedicchio and J. Rosicky We characterize when the coequalizer and the exact completion of a category $\cal C$ with finite sums and weak finite limits coincide. Theory and Applications of Categories, Vol. 6, 1999, No. 6, pp 77-82 http://www.tac.mta.ca/tac/volumes/6/n6/n6.dvi http://www.tac.mta.ca/tac/volumes/6/n6/n6.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n6/n6.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n6/n6.ps ------------------------------------------------------------------------- Enriched Lawvere theories John Power We define the notion of enriched Lawvere theory, for enrichment over a monoidal biclosed category $V$ that is locally finitely presentable as a closed category. We prove that the category of enriched Lawvere theories is equivalent to the category of finitary monads on $V$. Moreover, the $V$-category of models of a Lawvere $V$-theory is equivalent to the $V$-category of algebras for the corresponding $V$-monad. This all extends routinely to local presentability with respect to any regular cardinal. We finally consider the special case where $V$ is $Cat$, and explain how the correspondence extends to pseudo maps of algebras. Theory and Applications of Categories, Vol. 6, 1999, No. 7, pp 83-93 http://www.tac.mta.ca/tac/volumes/6/n7/n7.dvi http://www.tac.mta.ca/tac/volumes/6/n7/n7.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n7/n7.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n7/n7.ps ------------------------------------------------------------------------- Epimorphic regular contexts Robert Raphael A von Neumann regular extension of a semiprime ring naturally defines a epimorphic extension in the category of rings. These are studied, and four natural examples are considered, two in commutative ring theory, and two in rings of continuous functions. Theory and Applications of Categories, Vol. 6, 1999, No. 8, pp 94-104 http://www.tac.mta.ca/tac/volumes/6/n8/n8.dvi http://www.tac.mta.ca/tac/volumes/6/n8/n8.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n8/n8.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n8/n8.ps ------------------------------------------------------------------------- Natural deduction and coherence for non-symmetric linearly distributive categories Robert R. Schneck In this paper certain proof-theoretic techniques of [BCST] are applied to non-symmetric linearly distributive categories, corresponding to non-commutative negation-free multiplicative linear logic (mLL). First, the correctness criterion for the two-sided proof nets developed in [BCST] is adjusted to work in the non-commutative setting. Second, these proof nets are used to represent morphisms in a (non-symmetric) linearly distributive category; a notion of proof-net equivalence is developed which permits a considerable sharpening of the previous coherence results concerning these categories, including a decision procedure for the equality of maps when there is a certain restriction on the units. In particular a decision procedure is obtained for the equivalence of proofs in non-commutative negation-free mLL without non-logical axioms. Theory and Applications of Categories, Vol. 6, 1999, No. 9, pp 105-146 http://www.tac.mta.ca/tac/volumes/6/n9/n9.dvi http://www.tac.mta.ca/tac/volumes/6/n9/n9.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.ps From cat-dist Fri Dec 3 16:36:07 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA03509 for categories-list; Fri, 3 Dec 1999 15:01:12 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from zent.mta.ca (zent.mta.ca [138.73.101.4]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id MAA12067 for ; Fri, 3 Dec 1999 12:55:08 -0400 (AST) X-Received: FROM agnostix.bangor.ac.uk BY zent.mta.ca ; Fri Dec 03 13:12:33 1999 X-Received: from hysterix.bangor.ac.uk (hysterix.bangor.ac.uk [147.143.2.6]) by agnostix.bangor.ac.uk (8.8.8/8.8.8) with ESMTP id QAA17388 for ; Fri, 3 Dec 1999 16:55:04 GMT X-Received: from publix (publix [147.143.2.48]) by hysterix.bangor.ac.uk (8.8.8/8.8.8) with ESMTP id QAA15236 for ; Fri, 3 Dec 1999 16:55:03 GMT Date: Fri, 3 Dec 1999 16:54:24 +0000 (GMT) From: "R.Brown" To: Subject: categories: Workshop on Algebraic K-theory, algebraic homotopy, and global actions Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 2 Workshop on Algebraic K-theory, algebraic homotopy, and global actions Mathematics Division, School of Informatics, University of Wales, Bangor January 4-12, 2000 This workshop is the next in a series of Bangor/Bielefeld workshops which have formed part of a British Council/ARC programme in collaboration with Prof A Bak (Bielefeld). Colleagues outside Bangor/Bielefeld are welcome to participate at their own costs. The matters for lectures and discussion will include the following and their interactions (i) Global actions and groupoid atlases (ii) Homotopy limits and colimits (iii) Generalised dimension theory for categories (iv) Related topics Participants (as of December 3) Bangor Ronnie Brown Tim Porter Chris Wensley Anne Heyworth Jan Snellman (Stockholm and Bangor) Emma Moore Bielefeld Tony Bak Arun Munkur Rooz Hazrat Niko Inassaridze (Tbilisi, Bangor) . Background Bak's theory of Global Actions gives a framework for an algebraic approach to higher Algebraic K-theory, and in fact has more general applications. This framework has been generalised in joint work with Bangor to the notion of Groupoid Atlas. There have emerged from previous workshops links between single domain global actions and recent work in Geometric Group Theory, including complexes of groups, higher generation by subgroups, and identities among relations for presentations. Enquiries to: Prof R Brown r.brown@bangor.ac.uk We can give lists of local B&B and hotels. Prof R. Brown, School of Mathematics, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382475 fax: +44 1248 361429 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ (Links to survey articles: Higher dimensional group theory Groupoids and crossed objects in algebraic topology) Symbolic Sculpture and Mathematics: http://www.bangor.ac.uk/SculMath/ Mathematics and Knots: http://www.bangor.ac.uk/ma/CPM/exhibit/welcome.htm From cat-dist Thu Dec 9 23:56:22 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id WAA29676 for categories-list; Thu, 9 Dec 1999 22:52:05 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199912081539.LAA03094@mailserv.mta.ca> To: categories@mta.ca Subject: categories: 1st CFP CALCULEMUS-2000 Date: Wed, 08 Dec 1999 15:27:51 +0000 From: Manfred Kerber Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 3 CALCULEMUS-2000 Symposium on the Integration of Symbolic Computation and Mechanized Reasoning 6-7 August 2000 St Andrews, Scotland (collocated with ISSAC 2000) http://www.mathweb.org/calculemus/meetings/standrews00 SCOPE Both deduction systems and computer algebra systems are receiving growing attention from industry and academia. On the one hand, mathematical software systems have been commercially very successful. Their use is now wide-spread in industry, education, and scientific contexts. On the other hand, the use of formal methods in hardware and software development has made deduction systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved. As many application domains fall outside the scope of existing deduction systems and computer algebra systems, there is still need for improvement and in particular need for the integration of computer algebra and deduction systems. The symposium is intended for researchers and developers interested in combining the reasoning capabilities of deduction systems and the computational power of computer algebra systems. TOPICS Topics of interest for the symposium include all aspects related to the combination of deduction systems and computer algebra systems. We explicitly encourage submissions of results from applications and case studies where such integration results are particularly important. FORMAT The symposium will feature invited talks, contributed presentations with ample time for discussion, and a panel session. Consistent with the tradition of the symposium as a lively forum for discussing controversial ideas, we expect and encourage contributed talks to present work in progress, rather than polished final results. INVITED SPEAKERS - Henk Barendregt, U. Nijmegen, Mathematics and Computer Science - Arjeh Cohen, Eindhoven University of Technology, Dept. Math. - Gaston Gonnet, ETH Z"urich, Institute for Scientific Computation SUBMISSION Authors are invited to submit papers in the following categories: - Full papers up to 15 pages describing original results not published elsewhere. - System descriptions of up to 5 pages describing new systems or significant upgrades of existing ones, especially including experiments. Details of the submission format will be available from the web page (see top) closer to the deadline. Authors of accepted full papers and system descriptions are expected to present their contribution at the symposium. Authors of system descriptions are expected to demonstrate their systems. The symposium will have published proceedings, the organizers are currently negotiating with major publishers. The results and details will be published at the web page together with the submission specification. IMPORTANT DATES Submission deadline: 1 April 2000 Notification of acceptance: 22 May 2000 Final versions for proceedings: 9 July 2000 Workshop: 6-7 August 2000 ISSAC: 7-9 August 2000 ORGANIZATION and PROGRAMME CHAIRS Manfred Kerber, U. Birmingham, Michael Kohlhase, U. Saarbr"ucken, LOCAL ORGANIZER Steve Linton, St. Andrews U. PROGRAMME COMMITTEE Alessandro Armando, U. Genova Michael Beeson, San Jose State U. Manuel Bronstein, INRIA Sophia Antipolis Bruno Buchberger, RISC, Linz Jaques Calmet, U. Karlsruhe Olga Caprotti, TU. Eindhoven Edmund Clarke, CMU Therese Hardin, Paris VI John Harrison, Intel Corp. Tudor Jebelean, RISC, Linz Helene Kirchner, Nancy LORIA/INRIA Deepak Kapur, U. New Mexico, Albuquerque Steve Linton, St. Andrews U. Ursula Martin, St. Andrews U. Julian Richardson, U. Edinburgh J"org Siekmann, U. Saarbr"ucken Carolyn Talcott, Stanford U. Andrzej Trybulec, U. Bialystok From cat-dist Fri Dec 10 11:22:14 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA21391 for categories-list; Fri, 10 Dec 1999 09:18:59 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 10 Dec 1999 11:30:18 +0100 From: Philippe Gaucher Message-Id: <199912101030.AA04947@irmast1.u-strasbg.fr> To: categories@mta.ca Subject: categories: preprint: Combinatorics of branchings in higher dimensional automata Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Content-Md5: lVG6A+5uLWebQDtkuAGTZA== Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 Title : Combinatorics of branchings in higher dimensional automata Abstract : We explore the combinatorial properties of the branching areas of paths in higher dimensional automata. Mathematically, this means that we investigate the combinatorics of the negative corner homology of a globular $\omega$-category and the combinatorics of a new homology theory called the reduced negative corner homology. This latter is the homology of the quotient of the corner complex by the sub-complex generated by its thin elements. As application, we calculate the corner homology of some $\omega$-categories and we give some invariance results for the reduced corner homology. We only treat the negative side. The positive side, that is to say the case of merging areas of paths is similar and can be easily deduced from the negative side. URL : math.CT/9912059 (XXX archive http://arXiv.org/) Comments : LaTeX2e, 42 pages From cat-dist Fri Dec 10 20:30:43 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA00370 for categories-list; Fri, 10 Dec 1999 19:33:51 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <38516135.700E4F0D@disi.unige.it> Date: Fri, 10 Dec 1999 21:23:17 +0100 From: Giuseppe Rosolini X-Mailer: Mozilla 4.51 [en] (X11; I; Linux 2.2.12-7 i686) X-Accept-Language: en MIME-Version: 1.0 To: types@cis.upenn.edu, categories@mta.ca Subject: categories: Cfp: Realizability Semantics and Applications (MSCS special issue) References: <3639.939056653@unbox.fox.cs.cmu.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 Call for Papers REMINDER with deadline extension Special Issue of Mathematical Structures in Computer Science (MSCS) on Realizability Semantics and Applications Editors: L. Birkedal, J. van Oosten, G. Rosolini, D.S. Scott There has been recently a reawaking of interest in many aspects of realizability interpretations -- especially as regards semantics of type theories for constructive reasoning and semantics of programming languages. But, the details of realizability can be quite technical, and therefore a tutorial workshop on realizability and appliations was held in June/July 1999 in Trento, Italy. The workshop contained both tutorial lectures and also contributed research talks, see http://www.cs.cmu.edu/afs/cs/user/birkedal/www/realizability-workshop/ for an overview. A special issue of the journal Mathematical Structures in Computer Science (MSCS) will be devoted to papers on realizability semantics and applications. The volume will contain the tutorial presentations given by invited speakers at the realizability workshop in Trento, see http://www.cs.cmu.edu/afs/cs/user/birkedal/www/realizability-workshop/ for an overview. We now also solicit contributions of research papers on realizability and applications for the special MSCS volume. Everyone is invited to contribute a paper (i.e., not only researchers who contributed a paper to the realizability workshop). Papers will be refereed to the usual high standards of MSCS. Instruction to Authors Authors are invited to submit full original research papers. Papers should be submitted via email to wr99@athena.disi.unige.it as a postscript file, or by mailing a hard copy to Lars Birkedal School of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213, USA before January 20, 2000. Important Dates Submission Deadline: 20/01/2000 From cat-dist Tue Dec 14 15:54:29 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA05697 for categories-list; Tue, 14 Dec 1999 14:28:25 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199912102015.MAA06201@dtthp127> To: categories@mta.ca Subject: categories: TPHOLs 2000 --- call for papers Date: Fri, 10 Dec 1999 12:14:55 -0800 From: John Harrison Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 [We apologize if you receive multiple copies of this message] CALL FOR PAPERS: TPHOLs 2000 The 13th International Conference on Theorem Proving in Higher Order Logics Portland, Oregon, USA Monday 14 August - Friday 18 August 2000 *************************************** * http://www.cse.ogi.edu/tphols2000 * *************************************** The 2000 International Conference on Theorem Proving in Higher Order Logics will be the thirteenth in a series that dates back to 1988. The conference will be held Monday 14 August through Friday 18 August, 2000, at the DoubleTree Hotel, Portland, Oregon, USA. The first day of the conference will be devoted to tutorials, with the remaining 4 days covering the main conference program. TOPICS The program committee welcomes submissions on all aspects of theorem proving in higher order logics, and on related topics in theorem proving and verification. This includes, but is not limited to, the following topics: o Hardware and software verification, refinement and synthesis o Verification of security and communications protocols o Formal specification and requirements analysis of systems o Industrial applications of theorem provers o Advances in theorem prover technology o Comparisons of various approaches to theorem proving o Proof automation and decision procedures o Incorporation of theorem provers into larger systems o Combination of theorem provers with other provers and tools o User interfaces for theorem provers o Development and extension of higher order logics SUBMISSION Submissions are invited in the following categories: o Category A: Full research paper o Category B: Informal progress report Submissions under category A will be fully refereed, and accepted papers will be published as a volume of Springer-Verlag's Lecture Notes in Computer Science series ("http://www.springer.de/comp/lncs/index.html"), which will be available at the conference. Authors of accepted papers are expected to present their work at the conference. Submissions under category B will not be formally refereed, but their content and relevance will be reviewed. Those submissions accepted will be published in a technical report, which will be available at the conference. Authors of accepted papers are expected to present a brief outline of their work at the conference and to prepare a poster for display at the conference venue. Unless otherwise requested, submissions rejected under category A will also be considered for inclusion under category B. DEADLINES AND SUBMISSION PROCEDURE o Deadline for category A submissions: 25 Feb 2000 o Deadline for category B submissions: 17 Mar 2000 o Notification of acceptance: 3 Apr 2000 o Camera-ready copy for category A due (provisional): 5 May 2000 o Conference: 14-18 Aug 2000 Papers should be no more than 16 pages in length and should be written using LaTeX2e and the LNCS style file, which is available from "http://www.springer.de/comp/lncs/authors.html". Submissions should be sent electronically following the instructions on the TPHOLs web page, or emailed directly to the organizers using the email address "tphols2000@cse.ogi.edu". This email address can also be used for any inquiries concerning the conference. PROGRAM COMMITTEE Mark Aagaard (Intel) Bart Jacobs (Nijmegen) Flemming Andersen (IBM) Paul Jackson (Edinburgh) David Basin (Freiburg) Steve Johnson (Indiana) Richard Boulton (Edinburgh) Sara Kalvala (Warwick) Albert Camilleri (HP) Tom Melham (Glasgow) Gilles Dowek (INRIA) Paul Miner (NASA) Harald Ganzinger (Saarbrucken) Tobias Nipkow (Muenchen) Ganesh Gopalakrishnan (Utah) Sam Owre (SRI) Mike Gordon (Cambridge) Christine Paulin-Mohring (INRIA) Jim Grundy (ANU) Lawrence Paulson (Cambridge) Elsa Gunter (Bell Labs) Klaus Schneider (Karlsruhe) John Harrison (Intel) Sofiene Tahar (Concordia) Doug Howe (Bell Labs) Ranga Vemuri (Cincinnati) Warren Hunt (IBM) CONFERENCE ORGANIZATION The conference is being organized by Intel Corp. and the Oregon Graduate Institute (OGI). The organizing committee is as follows: Mark Aagaard (General Chair) John Harrison (Program Chair) Kelly Atkinson Naren Narasimhan Robert Beers Tom Schubert Nancy Day From cat-dist Tue Dec 14 17:06:51 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA24352 for categories-list; Tue, 14 Dec 1999 15:26:55 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 14 Dec 1999 16:44:52 +0000 From: Tony Seda Subject: categories: MFCSIT2000 -- First Call for Papers X-Sender: stmt8002@bureau.ucc.ie To: categories@mta.ca Message-id: <3.0.5.32.19991214164452.007b0320@bureau.ucc.ie> MIME-version: 1.0 X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.5 (32) Content-type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 7 *** apologies for multiple copies *** First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT2000 National University of Ireland, Cork 20th and 21st July, 2000 FIRST CALL FOR PAPERS Background MFCSIT2000 is the first conference to be held in Ireland with a focus on mathematical and foundational issues arising out of Computer Science and IT. There has been a very significant increase in Ireland over the last few years in activities relating to the production of software and hardware by some of the major computer manufacturers. This conference is intended to be a forum for discussion of related theoretical questions. Topics The intended coverage of the conference includes: Semantics of Procedural and Declarative Programming Languages, Logic in Computer Science, Categorical and Topological aspects of Computer Science, Computer Algebra Systems in Mathematics, Number Theory in Computer Science. Especially welcome are papers which broadly relate to the interests of the main speakers and which therefore fall into one or other of two main themes: (i) Mathematical Foundations of Computational Logic and Artificial Intelligence, and Categorical, Domain-Theoretic and Topological Methods in Computer Science, (ii) Computer Algebra Systems in Mathematics. Invited Speakers Confirmed main speakers are Abbas Edalat (Imperial College) Dick Hamlet (University of Portland, Oregon) Giorgio Levi (University of Pisa) Dana Scott (Carnegie Mellon University) Steering Committee James Bowen (NUI, Cork), Ted Hurley (NUI, Galway), Micheal MacanAirchinnigh (Trinity College, Dublin), Michel Schellekens (NUI, Cork), Anthony K. Seda (NUI, Cork) Programme Co-Chairs Ted Hurley (NUI, Galway) and Anthony K. Seda (NUI, Cork) Publication of Proceedings Papers will be refereed, and it is expected that the Conference proceedings (or a selection thereof) will appear as a volume in ENTCS, Elsevier's series "Electronic Notes in Theoretical Computer Science". Sponsorship The Conference is being sponsored by The Arts Faculty, NUI, Cork The Department of Computer Science, NUI, Cork The Department of Mathematics, NUI, Galway The School of Mathematics, Applied Mathematics and Statistics, NUI, Cork Enterprise Ireland Logic Programming Associates, London The National Software Directorate, Dublin Important Dates Abstract submission: abstracts of one page in length should be submitted electronically to aks@ucc.ie by 1st May, 2000; talks will be of 30 minutes duration including 5 minutes for questions. Conference dates: 20th and 21st July, 2000. Full paper submissions: papers of not more than 18 pages in length should be submitted electronically by 15th August, 2000 to aks@ucc.ie in LaTeX, Postscript or PDF format. Papers must be original and not submitted for publication elsewhere, although survey papers of sufficiently high quality may be considered. Notification of acceptance: authors will be notified of the refereeing decision by 31st October, 2000. Final versions of papers: authors should return final versions of papers by 30th November, 2000. For authors who are unable to submit electronically, five paper copies should be mailed to: Anthony K. Seda, Department of Mathematics, National University of Ireland - Cork, Cork, Ireland so as to arrive on or before the submission deadline. Conference website http://maths.ucc.ie/~seda/uccconf.html Queries Please address all queries to aks@ucc.ie A.K. Seda (Co-Chairman) 14th December, 1999. From cat-dist Tue Dec 14 18:11:35 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id RAA25087 for categories-list; Tue, 14 Dec 1999 17:14:08 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199912131450.PAA19744@insatlse.insa-tlse.fr> X-Sender: motet@insatlse.insa-tlse.fr X-Mailer: QUALCOMM Windows Eudora Pro Version 4.0.2 Date: Mon, 13 Dec 1999 15:50:36 +0100 To: categories@mta.ca From: Gilles Motet Subject: categories: CFP: Journal of Theoretical Computer Science, Special Issue on "Dependable Computing" Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 8 Dear Sir/Madam, I wonder would it be possible for you to circulate this listing about CFP for Journal of Theoretical Computer Science, Special Issue on "Dependable Computing"? Journal of Theoretical Computer Science (http://www.elsevier.nl/locate/tcs). Special Issue on "Dependable Computing". Call for papers. Papers should be sent as attached rtf, postscript or pdf files to Guest Editor Gilles Motet by - December the 20th, 1999 for preliminary abstracts and by - January the 15th, 2000 for complete papers. Email: Gilles.Motet@insa-tlse.fr Address: LESIA / DGEI, INSA, 135, avenue de Rangueil, 31077 Toulouse cedex 4, France. More information: http://wwwdge.insa-tlse.fr/~lesia/tcs-call-for-paper.html Respectfully yours, Gilles Motet - - - - Prof. Gilles MOTET tel : +(33/0) 5 61 55 98 18 Directeur du LESIA, DGEI / INSA fax : +(33/0) 5 61 55 98 00 135, avenue de Rangueil sec : +(33/0) 5 61 55 98 13 31077 Toulouse cedex 4 E-mail : Gilles.Motet@insa-tlse.fr France URL: http://wwwdge.insa-tlse.fr/~lesia/ - - - - From cat-dist Thu Dec 16 10:33:59 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA12675 for categories-list; Thu, 16 Dec 1999 08:49:33 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 16 Dec 1999 11:16:32 GMT Message-Id: <23970.199912161116@craro.dcs.ed.ac.uk> To: categories@mta.ca Subject: categories: CTCS '99 Special Issue in TCS From: "Martin Hofmann" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 9 Call for Papers Special Issue of Theoretical Computer Science (TCS) on Categories in Computer Science Editors: J. Adamek, M. Escardo, M. Hofmann The eighth conference on Category Theory and Computer Science (CTCS'99) has been held in Edinburgh 10-12 September 1999. A special issue of the journal Theoretical Computer Science (TCS) will be devoted to journal versions of papers presented at that conference and other papers on the same topic. Submissions will undergo the usual refereeing process for TCS; authors of submissions are not required to have participated at CTCS'99. >From the call for papers: "The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory. While the emphasis is upon applications of category theory, it is recognized that the area is highly interdisciplinary. Topics of interest include but are not limited to category-theoretic aspects of the following: concurrent and distributed systems, constructive mathematics, declarative programming and term rewriting, domain theory and topology, linear logic, models of computation, program logics, data refinement, and specification, programming language semantics, type theory". See also http://www.dcs.ed.ac.uk/home/ctcs99 for the conference programme. Instructions to Authors ----------------------- Authors are invited to submit full original research papers. Papers should be submitted via email to ctcs99@dcs.ed.ac.uk as a postscript file, or by mailing a hard copy to Martin Hofmann Laboratory for Foundations of Computer Science JCM, Rm 2606 The King's Buildings Mayfield Rd Edinburgh EH9 3JZ UK before 31st March, 2000. Important Dates Submission Deadline: 31st March, 2000. From cat-dist Thu Dec 16 14:54:51 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA04284 for categories-list; Thu, 16 Dec 1999 12:58:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.19991216105035.00a33df0@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Thu, 16 Dec 1999 10:54:21 -0500 To: categories@mta.ca From: Charles Wells Subject: categories: Retirement Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 10 I am retiring from Case Western Reserve University. Future postal mail should be sent to Charles Wells 105 South Cedar Street Oberlin, OH 44074, USA and you should use only the email address and phone number below. The University has not yet told me whether they will allow me to keep my webpage at the address below, but the odds are that they will. Charles Wells, Oberlin, Ohio, USA. EMAIL: charles@freude.com. HOME PHONE: 440 774 1926. PROFESSIONAL WEBSITE: http://www.cwru.edu/artsci/math/wells/home.html PERSONAL WEBSITE: http://www.oberlin.net/~cwells/index.html From cat-dist Sat Dec 18 11:24:11 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA05237 for categories-list; Sat, 18 Dec 1999 10:05:04 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: street@hera.mpce.mq.edu.au Message-Id: Date: Fri, 17 Dec 1999 11:40:44 +1100 To: categories@mta.ca From: Ross Street Subject: categories: Postgraduate Scholarships Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 11 Mathematicians: Below is an advertisement for Postgraduate Fellowships in memory of Scott Russell Johnson. I should explain what the ad really means. For those people without permanent residency in Australia, Macquarie University charges fees in the order of $16000 per year for enrolment in a PhD program. There are a few scholarships at Macquarie available to cover those fees but the rules for those (and the conventions followed by the committee) make it hard for a standard good student with an excellent undergraduate record (or even with a Masters degree) to get one. For a person with permanent residency and a good record (equivalent of First Class Honours in our system), there are generally enough Australian Postgraduate Awards (APAs) to go around. An APA pays a living allowance of around $17000 per year tax free (it lasts 3 years subject to performance and is rarely extended much beyond that). What we are trying to do with the SRJ Memorial Scholarship is two-fold: (1) given that an overseas student has paid the Macquarie fees, this Scholarship will provide $15000 towards a living allowance; (2) for Australian students, this Scholarship will supplement the APA with an extra $5000 per annum. We cannot afford very many of these scholarships at one time, so they are competitive. All postgraduate students are able to get a little extra from tutoring or assignment marking. Overseas students may also be able to obtain a supplement of around $3000 per annum from our Department. Regards, Ross http://www.math.mq.edu.au/~street/ MACQUARIE UNIVERSITY New South Wales 2109 Australia Scott Russell Johnson Memorial Scholarships for PhD Research Applications are invited for Scott Russell Johnson Memorial Scholarships which are offered for full-time PhD studies in the Centre of Australian Category Theory (CoACT) at Macquarie University. Applicants should hold or expect to obtain a First class Bachelor Honours degree (or equivalent) in an appropriate field, and be eligible for admission to the degree of Doctor of Philosophy in the Division of Information and Communication Sciences in the area of Mathematics. The award will be made to the best qualified applicants on the basis of academic merit. The full Scholarship provides a living allowance of $15,000 per annum tax exempt. A supplementary scholarship, up to the maximum allowed, may be awarded to students who already hold an APA or MUPGRA; see . The full scholarship may not be held concurrently with any other equivalent scholarship, and the Scholarship holder will be responsible for any student or other fees payable in relation to candidature. Additional funds for conference travel and thesis production may be available from CoACT. The Scholarship will be initially awarded for a maximum of three years, with the possibility of a one year extension. It is tenable only up to the date of submission of the thesis, subject to satisfactory progress. Conditions related to overseas study, suspension of award, multiple awards, employment, sick, maternity and recreation leave will be the same as those for the Australian Postgraduate Award Scheme. The Scholarship holder shall be free to publish any results arising from the research. Any publications shall acknowledge that the work was done while holding the Scholarship. Applications should be made on the application form available from Postgraduate Studies Section Level 1 Council Building Macquarie University N S W 2109 AUSTRALIA email no later than 31 January 2000. For further details contact Professor Ross Street by electronic mail or phone <+61 (0)2 9850 8921>. From cat-dist Mon Dec 20 17:48:57 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA26489 for categories-list; Mon, 20 Dec 1999 16:44:52 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <385D1476.4FDB096B@di.unipi.it> Date: Sun, 19 Dec 1999 18:23:02 +0100 From: Andrea Corradini Organization: Dipartimento di Informatica - Pisa X-Mailer: Mozilla 4.7 [en] (X11; I; Linux 2.2.5-15smp i686) X-Accept-Language: en, it MIME-Version: 1.0 To: categories@mta.ca Subject: categories: CfP: Wksp. on Graph Transformation and Visual Modeling Techniques Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 12 [sorry for multiple copies] ---------------- FIRST CALL FOR CONTRIBUTIONS ----------------- Workshop on Graph Transformation and Visual Modeling Techniques Geneva, Switzerland Saturday July 15, 2000 A Satellite Event of ICALP'2000 -------------------------------------------------------------------- SCOPE AND OBJECTIVES OF THE WORKSHOP Visual modelling techniques provide an intuitive, yet precise way in order to express and reason about concepts at their natural level of abstraction. The success of visual techniques in computer science and engineering resulted in a variety of methods and notations addressing different application domains and different phases of the development process. Diagrammatic languages are used, for example, during requirement specification in order to support the communication between developers and customers; but also for describing the architecture of systems and as high-level visual programming languages. However, despite the wide-spread usage of visual modelling techniques there is a lack of well-understood (and integrated) methodologies for defining their syntax and semantics. Until now, there exists no equivalent to Backus-Naur-Form which would be the notation for defining the syntax of a visual language. The same applies to type systems, deductive proof methods, operational or denotational semantics for visual modelling techniques. In fact, the situation could be compared with the state-of-the-art in programming languages about thirty years ago when the definition and implementation of languages was an ad-hoc task, and formal semantics was an exception rather than the rule. The workshop aims at bringing together scientists and researchers interested in discussing formal methodologies for the definition of syntax and semantics of visual modelling techniques. All aspects of this problem are of potential interest ranging from the concrete syntax defined, for example, by Constraint Grammars or Picture Layout Grammars, the abstract syntax specified by means of Meta Modelling or Graph Grammars, and the semantics of visual modelling techniques given, e.g., in terms of Graph Transformation, Process Algebra, Abstract State Machines, Type Theory, Logic, etc. In particular, we believe that Graph Grammars and Graph Transformation may play a central role in the definition of visual modelling techniques because they provide the graphical analogous to Chomsky Grammars and Term Rewriting which are widely used for defining the syntax and semantics of textual languages. CALL FOR CONTRIBUTIONS Authors are invited to submit extended abstracts of up to 5 (five) A4 pages. The contributions should report about ongoing research in the area of graph transformation and visual modelling techniques, especially on the syntax and semantics of visual languages according to the scope and objectives of the workshop. Contributions exploring the use of Graph Grammars and Graph Transformation Systems are particularly welcome, as well as papers which cover several aspects or integrate different formalisms for the definition of visual modelling techniques. Position papers and contributions making methodological statements are strongly encouraged. Submissions should be sent preferably in postscript format to the address (Andrea Corradini) before the submission deadline. In the case electronic submission is not possible, three copies should be sent to the address: Andrea Corradini Dipartimento di Informatica Corso Italia 40 56125 - Pisa - ITALY IMPORTANT DATES Deadline for submissions: March 1, 2000 Notification of acceptance: April 3, 2000 Final version of accepted extended abstracts: April 28, 2000 PROGRAM COMMITTEE Andrea Corradini (University of Pisa, I) [co-chair] Hartmut Ehrig (Technical University Berlin, D) Wolfgang Emmerich (University College London, GB) Reiko Heckel (University of Paderborn, D) [co-chair] Dirk Janssens (University of Antwerp, B) Hans-Joerg Kreowski (University of Bremen, D) Fernando Orejas (University of Catalonia, Barcelona, E) Grzegorz Rozenberg (University of Leiden, NL) Andy Schuerr (University of the German Federal Armed Forces, Munich, D) PROCEEDINGS The abstracts of the contributions accepted for presentation will be published in a volume collecting the contributions to all satellite workshops of ICALP 2000. The volume will be published by Carleton Scientific, and it will be distributed to all ICALP participants. On the basis of the number and quality of the submissions, the Program Committee will consider the possibility of inviting submissions for a special issue of an international journal dedicated to the workshop. INVITED SPEAKERS Gregor Engels (University of Paderborn, D) Martin Gogolla (University of Bremen, D) Francesco Parisi Presicce (University of Rome, I) Mauro Pezze' (Politecnico di Milano) ACKNOWLEDGEMENTS We acknowledge the financial support by the TMR Research Network GETGRATS (General Theory of Graph Transformation Systems) and the ESPRIT Working Group APPLIGRAPH (Applications of Graph Transformation) -- Dr. Andrea Corradini Tel: +39-050887266 Dipartimento di Informatica Fax: +39-050887226 Corso Italia 40 Email: andrea@di.unipi.it 56125 - Pisa - ITALY WWW: http://www.di.unipi.it/~andrea From cat-dist Mon Dec 20 17:54:17 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA27729 for categories-list; Mon, 20 Dec 1999 16:48:52 -0400 (AST) Date: Mon, 20 Dec 1999 12:13:55 -0500 (EST) Message-Id: <199912201713.MAA12785@alonzo.cse.psu.edu> X-Authentication-Warning: alonzo.cse.psu.edu: concur2k set sender to concur2k@alonzo.cse.psu.edu using -f From: Concur2000 To: categories@mta.ca Subject: categories: CONCUR 2000: Call for Papers Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 13 FIRST CALL FOR PAPERS CONCUR 2000 11th International Conference on Concurrency Theory State College, Pennsylvania, August 22-25, 2000 URL http://www.cse.psu.edu/concur2000/ E-mail concur2000@cse.psu.edu (apologies for multiple copies) SCOPE The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency, and promote its applications. Interest in this topic is continuously growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. Submissions are solicited in all areas of semantics, logics and verification techniques for concurrent systems. Topics include (but are not limited to) concurrency related aspects of: models of computation and semantic domains, process algebras, Petri nets, event structures, real-time systems, hybrid systems, decidability, model-checking, verification techniques, refinement techniques, term and graph rewriting, distributed programming, logic constraint programming, object-oriented programming, typing systems and algorithms, case studies, tools and environments for programming and verification. PROGRAM COMMITTEE Samson Abramsky (Edinburgh University, UK) Jos C. M. Baeten (University of Eindhoven, NL) Eike Best (Oldenburg University, Germany) Michele Boreale (University of Florence, Italy) Steve Brookes (Carnegie Mellon University, USA) Luca Cardelli (Microsoft, UK) Ilaria Castellani (INRIA, France) Philippe Darondeau (INRIA, France) Thomas Henzinger (UC Berkeley, USA) Radha Jagadeesan (Loyola University, USA) Marta Kwiatkowska (University of Birmingham, UK) Dale Miller (Co-chair, Penn State University, USA) Robin Milner (Cambridge University, UK) Uwe Nestmann (BRICS, Denmark) Catuscia Palamidessi (Co-chair, Penn State University, USA) Prakash Panangaden (McGill University, Canada) John Reppy (Bell Labs, USA) Vladimiro Sassone (University of Catania, Italy) Moshe Y. Vardi (Rice University, USA) Wang Yi (Uppsala University, Sweden) ORGANIZATION Dale Miller and Catuscia Palamidessi (Co-chairs, Penn State University, USA) SUBMISSIONS Submissions will be evaluated by the Program Committee for inclusion in the proceedings, which will be published by Springer-Verlag. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Papers (of at most 15 pages, accompanied by a one-page abstract) should preferably be submitted electronically as uuencoded PostScript files at the address given below. The mailing addresses (both postal and electronic), telephone number and fax number (if available) of the author to whom correspondence should be sent should be clearly indicated. In case of hardcopy submissions, send five copies to the address below. CALL FOR SATELLITE WORKSHOPS The CONCUR 2000 conference will host several satellite workshops, which will take place on Monday August 21 and Saturday August 26. Proposals for satellites are solicited. They should contain a brief description of the scope and organization of the workshop, and be sent to the workshop chair Uwe Nestmann . IMPORTANT DATES Deadline for submission: 3 March 2000 Notification of acceptance: 1 May 2000 Final version due: 29 May 2000 Extended deadline for satellite workshop proposals: 10 January 2000 ADDRESSES Dale Miller and Catuscia Palamidessi Computer Science and Engineering Department 220 Pond Lab, Penn State University University Park, PA 16802 Phone: +1-814-865-9505, FAX: +1-814-865-3176 URL http://www.cse.psu.edu/concur2000/ E-mail concur2000@cse.psu.edu From cat-dist Tue Dec 21 13:04:58 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA25862 for categories-list; Tue, 21 Dec 1999 12:04:48 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Organization: Universitaet des Saarlandes, D 66123 Saarbruecken Message-Id: <199912211115.MAA21513@goedel.ags.uni-sb.de> To: categories@mta.ca Subject: categories: 3 JOBS AT SAARBR"UCKEN, please distribute Date: Tue, 21 Dec 1999 12:15:54 +0100 From: Michael Kohlhase Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 14 [We apologize, if you receive multiple copies of this] Three Open Positions Researcher at the German National Research Centre for Artificial Intelligence (DFKI) Saarbr"ucken AND Scientific Assistants at the University of Saarbr"ucken a) For the research project "Interactive Textbook" (VIL) funded by the BMBF (The German Ministry for Education and Research) we seek applications for an open researcher position at the German National Research Centre for Artificial Intelligence, http://www.dfki.de/). For a more detailed description see below (VIL position). b) Within the research project "OMEGA: A mathematical Assistant System" funded by DFG (Deusche Forschungsgemeinschaft, the German analogue of the NSF) within the Corporate Research Center SFB-378 "Resource-Adaptive Cognitive Processes" we seek applications for open positions as Scientific Assistant. For a more detailed description see below (LIMA and MBASE positions). OMEGA is a mixed-initiative system with the ultimate purpose of supporting theorem proving in main-stream mathematics and mathematics education. The current system is an integrated, distributed collection of tools for interactive theorem proving, automated proof planning, proof presentation, and storing mathematical knowledge. The project home pages are http://www.ags.uni-sb.de/~omega VIL is a new project that is designed to apply AI-techniques such as proof planning, distributed systems, web communication, user modelling, and user-adaptive interfaces to an education system for mathematics. VIL has its basis in and is tightly connected with the OMEGA project. We offer - an innovative research project, - a highly motivated and cooperative team of about ten researchers working on the system, - a stimulating and well equipped working environment, with intimate connections between the DFKI (German Research Center for Artificial Intelligence) and the university research teams, - the possibility to work on a related PhD thesis. Applications are invited from suitably qualified applicants who - have completed an above average Master's Degree in computer science, mathematics, cognitive science, or equivalent, - enjoy teamwork and have a taste for interdisciplinary work - are committed to success-oriented work Applications including a list of publications and a curriculum vitae should be forwarded to: Prof.Dr. J"org Siekmann Universitat des Saarlandes / DFKI D-66041 Saarbr"ucken E-mail submission to or respectively is preferred. Priority will be given to applications received by February 1st. 2000 ====================================================================== Position (VIL) The applicant is expected to work on theoretical and practical aspects of mixed-initiative systems, user-adaptive learning systems, and student modelling within a maths education system. Applicants for this position should - have experience in formal reasoning, maths education systems, user-adaptive systems, and/or student modelling The position is available starting February 1. 2000 and will be for a period of one year with the option of further extension. Payment amounts to an annual salary of approximately 78 000.- DM before tax. Please, do not hesitate to contact Erica Melis for further information. ====================================================================== Position (LIMA) The applicant is expected to work on theoretical and practical aspects of automatically understanding mathematical texts and translating them into proof plans. Applicants for this position should - have experience in formal reasoning and/or natural language understanding, = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Position (MBASE) The applicant is expected to work on theoretical and practical aspects of formalizing mathematics, building a mathematical data base, and web communication with mathematical content. Applicants for this position should - have experience in formal reasoning, automated deduction, data bases, or web tools, = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Both position are available starting January 1. 2000 and will be for a period of two years with the option of an additional year. Payment for will be according to BAT2a on the German scale for federal employees. BAT2a amounts to an annual salary of 56 000.- to 86 000.- DM before tax strongly depending on age and family status. Please, do not hesitate to contact Michael Kohlhase for further information. From cat-dist Tue Dec 21 13:07:12 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA25778 for categories-list; Tue, 21 Dec 1999 12:03:15 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 20 Dec 1999 22:01:55 -0800 From: "William H. Rowan" Message-Id: <199912210601.AA24938@crl.crl.com> To: categories@mta.ca Subject: categories: Category-theoretic generalization of modular commutator Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 15 Hello all, I believe someone said, at the 1994 conference on Category Theory and Universal Algebra, that there was a category-theoretic generalization of the modular commutator. Can someone give me a reference about this? Bill Rowan From cat-dist Tue Dec 21 13:10:21 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA23990 for categories-list; Tue, 21 Dec 1999 12:01:59 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from zent.mta.ca (zent.mta.ca [138.73.101.4]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id JAA24973 for ; Tue, 21 Dec 1999 09:18:51 -0400 (AST) From: moerdijk@math.uu.nl X-Received: FROM bommel.math.uu.nl BY zent.mta.ca ; Tue Dec 21 09:37:04 1999 X-Received: from verkwil.math.uu.nl (verkwil.math.uu.nl [131.211.23.35]) by bommel.math.uu.nl (Postfix) with ESMTP id B5AA0FAD4 for ; Tue, 21 Dec 1999 14:18:48 +0100 (MET) X-Received: by verkwil.math.uu.nl (8.8.8/nullclient) id OAA12877; Tue, 21 Dec 1999 14:18:47 +0100 (MET) Date: Tue, 21 Dec 1999 14:18:47 +0100 (MET) Message-Id: <199912211318.OAA12877@verkwil.math.uu.nl> To: categories@mta.ca Subject: categories: Preprint: Proper maps of toposes X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 16 Dear category theorists, I would like to inform you that my preprint with Japie Vermeulen, "Proper maps of toposes", can now be obtained electronically from . (This paper will eventually appear as an issue of the Memoirs of the AMS.) With best wishes for the holidays, Ieke Moerdijk. From cat-dist Thu Dec 23 11:16:53 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA32601 for categories-list; Thu, 23 Dec 1999 09:24:13 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 22 Dec 1999 11:49:50 -0500 (EST) From: Peter Freyd Message-Id: <199912221649.LAA14585@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Real coalgebra Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 17 I've been looking at the Proceedings of the Second Workshop on Coalgebraic Methods in Computer Science (CMCS'99), Electronic Notes in Theoretical Computer Science, Volume 19, to be found at www.elsevier.nl:80/cas/tree/store/tcs/free/noncas/pc/menu.htm There's a nice paper by Dusko Pavlovic and Vaughan Pratt. It's entitled On Coalgebra of Real Numbers and it has turned me on. Their abstract begins: We define the continuum up to order isomorphism (and hence homeomorphism) as the final coalgebra of the functor X x omega, ordinal product with omega. This makes an attractive analogy with the definition of the ordinal omega itself as the initial algebra of the functor 1;X, prepend unity, with both definitions made in the category of posets. I thought of using another functor. And damned if it isn't just what I should have had for my CTCS talk last September at Edinburgh. In the category of posets with top and bottom consider the binary functor, X v Y, obtained by starting with the disjoint union X;Y, with everything in X ordered below Y, and then identifying the top of X with the bottom of Y. The functor X v X preserves the terminator (the one-element poset) hence the terminator is its final coalgebra. So restrict to the category of posets with _distinct_ top and bottom. The functor X v X again has a final coalgebra: this time it's the closed interval, I. (For Dusko and Vaughan's functor it's the half-open interval. For yet another functor, one that ought to have the open interval as its final coalgebra, but doesn't, see PS below.) If X v Y is described as the subobject of the product X x Y consisting of those pairs such that either x is top or y is bottom, then a coalgebra structure for X v X can be described as a pair of endo-functions d,u such that for each x either d(x) is top or u(x) is bottom. On the interval [a,b] the final-coalgebra structure is understood to be given by d(x) = min (b, 2x - a) and u(x) = max (a, 2x - b). In fact, we didn't need to start in the category of posets. It would have sufficed to work in the category of sets with distinct top and bottom (see PPS below for a proof). The final coalgebra is still the closed interval and, yes, the ordering is implicit: it is the most inclusive relation preserved by d and u that avoids placing top below bottom. (It can also be obtained by constructing either of the two lattice operations on I as the unique coalgebra map I x I --> I for an appropriately chosen coalgebra structure on I x I. A similar construction works for the Pavlovic-Pratt coalgebra.) Indeed, all of the structure of the closed interval is definable from this coalgebra definition. Go back to the category of posets with distinct top and bottom. It is routine to verify that X v X commutes with the opposite-poset functor hence -- using the fact that that functor is an equivalence -- its final coalgebra will be invariant under that functor. That is, there is an isomorphism from I to its opposite. It takes more work, but not an infinite amount, to construct a coalgebra structure on I x I so that the induced binary operation I x I --> I is the midpoint operation, the values of which will be denoted here as x|y. It is pretty much characterized by the equations: idempotence, x|x = x; commutativity, x|y = y|x; and middle- two-interchange, (u|v)|(x|y) = (u|x)|(v|y); together with cancelation: a|x = a|y => x = y. If one chooses a zero, then one may prove that there's an ambient abelian group with unique division by 2, such that the given midpoint algebra is a subset closed under the operation x|y = (x + y)/2. (There must be an existent reference for this.) Actually we want that ambient abelian group for I; it's none other than the reals. The order-duality makes its construction easier than in the general case. So let's use 1 to denote the top of the final coalgebra, I, -1 for the bottom, and 0 for their midpoint, -1|1. Let h:I -> I denote the "halving" map that sends x to 0|x. Note that h is an endomorphism with respect to 0, the ordering, the duality, the midpoint structure (and not, of course, the top and bottom). For a moment enter the category of endomorphisms, and reflect the object into the full subcategory of automorphisms. (The reflection may be explicitly constructed as the colimit of the diagram h h h I --> I --> I -->...) The result is a poset-with-0-and-duality-and- midpoint-operation we'll denote as R. The midpoint operation respects the order and commutes with duality. 0 is self-dual. By making h an automorphism we know that for all y there is a unique x such that 0|x = y. On R define a + b by the equation 0|(a + b) = a|b and verify 0 + b = b = b + 0 and (a + b) + (c + d) = (a + c) + (b + d). Use the duality to define -a and verify (-a) + a = 0. Use h to define a/2 and verify a/2 + a/2 = a. All of this makes R an abelian group with unique division by 2. Viewing R as an ordered abelian group it is easy to verify that any endomorphism is determined by where it sends 1 (inherited from I -> R). That, of course, allows us to define the multiplication. Those who heard my CTCS talk last September at Edinburgh, "Path Integrals, Bayesian Vision, and Is Gaussian Quadrature Really Good?", (there's an abstract at the same website as above) can appreciate why I'm particularly happy. I started by defining ordinary integration of continuous functions using -- without knowing it -- this coalgebra structure on I. Let C be the functor that assigns to a space X the set, C(X), of continuous real-valued functions on X. The "mean-value" function M:C(I) -> R can be characterized -- indeed, evaluated -- from its order-preservation together with what it does to constant functions and MxM C(I v I) --> C(I + I) --> C(I) x C(I) ---> R x R C(F) | | m v v M C(I) ------------------------------------> R where F:I -> I v I is the coalgebra structure and m is the midpoint operation. If C(F) is inverted then this diagram can be read as a fixed-point definition of M. (It's the unique fixed-point of an operator acting on the set of all those order-preserving maps from C(I) to R that do the right thing on constant functions.) PS Just for comparison, consider the category of posets and the functor that sends X to X;1;X. The open interval is an invariant object for this functor but it is not the final coalgebra. For that we need -- as we called it in Cats and Alligators -- Wilson space. Actually, not the space but the linearly ordered set, most easily defined as the lexicographically ordered subset, W, of sequences with values in {-1, 0, 1} consisting of all those sequences such that for all n a(n) = 0 => a(n+1) = 0 (take a finite word on {-1,1} and pad it out to an infinite sequence by tacking on 0s). PPS Given a coalgebra structure described by endo-functions d and u on X, let End(X) be the monoid of endo-functions on X. We will need to compose in the diagrammatic order: "ud" means "first u then d". Let {0,1}* be the free monoid with generators named 0 and 1 and Let M_X:{0,1}* --> End(X) be the monoid homomorphism such that M_X(0) = d and M_X(1) = u. Given x in X let L be the subset of {0,1}* consisting of those words w such that M_X(w) sends x to top in X. The elements of {0,1}* may, of course, be viewed as finite words on 0 and 1. By catenating "0." on the left of any such word we obtain a description -- in binary -- of a dyadic rational in the half-open unit interval [0,1). Define f:X -> I by sending each x to the supremum in [0,1] of the dyadic rationals, r(L), named by the words in its corresponding L. The L corresponding to d(x) can thus be obtained by taking each word in L that starts with 0 and deleting that 0. The resulting r(L) can be described by first throwing away each dyadic rational bounded below by 1/2 and then doubling each dyadic rational that remains, that is,doubling each dyadic rational bounded above by both f(x) and 1/2. The resulting supremum is thus min (1, 2f(x)). That's what f(d(x)) is. And it's also what d(f(x)) is. Same sort of argument for u. A little too easy. The recipe above does work for f but the proof that it works requires work. Note that the above argument requires -- among other things -- that r(L) be a downdeal. (And note that it never invoked the facts that d and u preserve top and bottom nor the fact that d(x) is top or u(x) is bottom for all x.) I think a return to Dedekind works best. Besides defining the "lower" set, L, define the "upper" set U as the subset of {0,1}* consisting of those words w such that M_X(w) sends x to bottom. We have the facts: w:L => w0:L and w1:L (using w:U => w0:U and w1:U ":" w:{0,1}* => w0:L or w1:U for membership) We may infer, just from w:L => w0:L and w:U => w0:U, that if a dyadic rational has a name in either L or U then it does not have a name in the other. Thus we obtain a disjoint pair of sets of dyadic rationals r(L) and r(U). For any pair of dyadic rationals x,y:[0,1) where x is _not_ in r(L) and x < y, it is the case that y is in r(U): it suffices to check, for any word w, that if w0 can be prolonged to a name of x, then w0 is not in L forcing w1 to be in U and, hence, any prolongation of w1 to be in U. It follows that r(U) is an updeal and if there's a dyadic rational in [0,1) that is in neither r(U) nor r(L) then there's only one such dyadic rational, to wit, the greatest lower bound of r(U). It follows that r(L) is a downdeal. The pair r(L) and r(U) thus forms a Dedekind cut and we can use it to name the value of f(x). The compatibility with d and u is a straightforward computation. For uniqueness, first verify that for every pair a < b in I there's a word w:{0,1}* such that M_I(w) sends a to bottom and b to top. If f,f':X -> I were both coalgebra maps, and x:X were such that f(x) < f'(x) let w be as described. Note that M_I(w0) = M_I(w) = M_I(w1). But either M_X(w0) sends x to top or M_X(w1) sends x to bottom. The first case contradicts that M_I(w0) sends f(x) to bottom. The second case contradicts that M_I(w1) sends f'(x) to top. From cat-dist Fri Dec 24 10:05:40 1999 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA17219 for categories-list; Fri, 24 Dec 1999 08:30:22 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199912241213.EAA03788@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Re: Real coalgebra In-reply-to: Your message of "Wed, 22 Dec 1999 11:49:50 EST." <199912221649.LAA14585@saul.cis.upenn.edu> Date: Fri, 24 Dec 1999 04:13:57 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 18 Apropos of Peter's kind remarks, the journal version of our paper should be in TCS soon, entitled The continuum as a final coalgebra. Meanwhile it's on the web as http://boole.stanford.edu/pub/continuum.ps.gz Abstract: We define the continuum up to order isomorphism, and hence up to homeomorphism via the order topology, in terms of the final coalgebra of either the functor NxX, product with the set of natural numbers, or the functor 1 + NxX. This makes an attractive analogy with the definition of N itself as the initial algebra of the functor 1 + X, disjoint union with a singleton. We similarly specify Baire space and Cantor space in terms of these final coalgebras. We identify two variants of this approach, a coinductive definition based on final coalgebraic structure in the category of sets, and a direct definition as a final coalgebra in the category of posets. We conclude with some paradoxical discrepancies between continuity and constructiveness in this setting. PF>So restrict to the category of posets with _distinct_ top and bottom. ...which has no final object, making the following all the nicer: PF>The functor X v X again has a final coalgebra: The bipointed-set version of this seems like *the* right way to generate the topology of the continuum. Verry nice. PF>PS PF>Just for comparison, consider the category of posets and the functor PF>that sends X to X;1;X. The open interval is an invariant object PF>for this functor but it is not the final coalgebra. For that we need PF>-- as we called it in Cats and Alligators -- Wilson space. Actually, PF>not the space but the linearly ordered set, most easily defined as the PF>lexicographically ordered subset, W, of sequences with values in PF>{-1, 0, 1} consisting of all those sequences such that for all n PF>a(n) = 0 => a(n+1) = 0 (take a finite word on {-1,1} and pad it PF>out to an infinite sequence by tacking on 0s). In other words the continuum plus *two* additional copies of each rational (as opposed to Cantor space's one additional copy). PF>It takes more work, but not an infinite amount, to construct a PF>coalgebra structure on I x I so that the induced binary operation PF>I x I --> I is the midpoint operation, the values of which will be PF>denoted here as x|y. It is pretty much characterized by the PF>equations: idempotence, x|x = x; commutativity, x|y = y|x; and middle- PF>two-interchange, (u|v)|(x|y) = (u|x)|(v|y); together with cancelation: PF>a|x = a|y => x = y. If one chooses a zero, then one may prove that PF>there's an ambient abelian group with unique division by 2, such that PF>the given midpoint algebra is a subset closed under the operation PF>x|y = (x + y)/2. (There must be an existent reference for this.) Here I should be understood as [-1,1]. Peter's implicit definition of this coalgebra structure on I x I has the following equivalent five-equation explicit definition (or seven if you count each of (3) and (4) as two equations). My apologies to anyone reading this with a variable-width font. x + y y + x (1) ----- = ----- 2 2 0 + 0 (2) ----- = 0 2 xo1 x + t --- + 0 -----o1 where the 2 o's are + and t is -1 (3) 2 = 2 or the 2 o's are - and t is 1 -------- ------- (o = operator, t = terminator) 2 2 xo1 yo1 x + y --- + --- -----o1 where the 3 o's are either (4) 2 2 = 2 all - or all + ------- ------- 2 2 x-1 y+1 x + y --- + --- ----- + 0 (5) 2 2 = 2 ------- --------- 2 2 All these equations clearly hold on I; the question is, what is their content? Well, spacing around + and - is significant: without a space the form x-1 x+1 --- (resp. --- ) denotes a non-middle (nonzero) element of I which when 2 2 represented as a string over {-1,0,1} has head -1 (resp. 1) and tail x, x + y while with a space the form ----- denotes a pair (x,y) of I x I. 2 Finally, if -1, 0, or 1 (which includes t) are preceded by a space then they denote the respective infinite constant sequences -1,-1,-1,... or 0,0,0,.. or 1,1,1... (each of which has that constant as its value). (Once a sequence hits a zero it stays zero.) The left hand side always has exactly one spaced +, and at the outermost level, since that's what we're trying to define. On the right hand side, each occurrence of a spaced + denotes a corecursive call (so two corecursive calls in the last equation --- it might seem like a lot of bother to do a corecursive call merely to add 0, but the real point of the second call is of course to divide the result of the first call by 2, which we can do by taking the mean with 0.) Equation (1) merely ensures that any pair (x,y) will match the left hand side of one of (2)-(5) one way round or the other. Equations (2)-(4) provide instant gratification inasmuch as they allow immediate production of the first "trit" (ternary digit) of the mean of x and y given only the first trit of each of them, thereby explicitly defining the desired coalgebra structure on I x I. But if you hit equation (5) you may be in for a long or even infinite wait (consider taking the mean of -1,1,-1,1,... (= -2/3) with 1,-1,1,-1,... (= 2/3), which to us is obviously zero but not so obviously to equation (5)). So equation (5) does not give the coalgebra structure at this part of I x I explicitly, one must regrettably deduce it by corecursion. Vaughan From rrosebru@mta.ca Sun Dec 26 15:03:47 1999 -0400 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA06018 for categories-list; Sun, 26 Dec 1999 13:54:03 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199912242159.NAA07485@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Re: Real coalgebra -- replacing equations by geometry In-reply-to: Your message of "Fri, 24 Dec 1999 04:13:57 PST." <199912241213.EAA03788@coraki.Stanford.EDU> Date: Fri, 24 Dec 1999 13:59:52 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 19 The continuum is intrinsically geometrical, so it is a shame to specify Peter's midpoint coalgebra on IxI with a mess of algebraic-looking equations as per my previous message when it has a relatively short and transparent geometric specification. (I must have got this idea from the paper on higher dimensional automata that I'm just finishing up.) Incidentally there were two ambiguities in my equations, arising from respectively equations (1) and (5). I was going to offer fixes for these, but one of the degeneracies that made these ambiguities possible in the first place (that with (5)) does not even arise in the geometric presentation, while the other, arising with (1), is just as readily dealt with geometrically as algebraically. In the following I'll refer to this coalgebra as Fm for Freyd's midpoint (unrelated to Scott's bottom). (For listeners who just tuned in to Fm, its role is to promote the final coalgebra I of Peter's fusion functor X v X from a linear order, and hence a topological space via the order topology, to a metric space understood as the real interval [-1,1]. It does this by furnishing IxI with a coalgebra, which determines a unique coalgebra homomorphism from IxI to I, I being the final coalgebra. This homomorphism is then taken to be (x+y)/2, while the endpoints of I are taken to be -1 and 1, thereby uniquely determining a continuous metric on I qua topological space.) For both the equational and geometric specifications, here's what the domain and codomain of Fm look like. (1,1) IxI ^ / \ / \ (1,1) (1,-1)< 1 >(-1,1) /\ \ / / \ Fm \ / (1,-1)< >(-1,1) -------------> 0 IxI v IxI \ / / \ \/ / \ (-1,-1) (1,-1)< -1 >(-1,1) \ / \ / V (-1,-1) So Fm maps pairs of the form (x,-x) to 0 (where the two copies of IxI are fused) and all other pairs (x,y) to a pair (h,(x',y')) whose head h specifies which copy of IxI to land in, 1 for upper and -1 for lower, and (x',y') gives the landing point within that copy. Here -1 <= x,y,x',y' <= 1, -x is defined by changing all the signs on the sequence representing x and h is unproblematically determined by whether (x,y) is in the upper or lower half of IxI oriented as shown. The tricky part is to specify x' and y' reasonably. (Although it is convenient to think of x and y as reals in [1,-1], at this stage they are merely infinite sequences over {-1,0,1} with the properties that once zero alway zero and infinite runs of -1 or 1 are only allowed in constant sequences.) The domain of Fm, namely I x I, can be blown up as (1,1) /\ / \ (1,0) (0,1) / \ / \ / \/ \ (1,-1)< (0,0) >(-1,1) \ /\ / \ / \ / (0,-1) (0,1) \ / \/ (-1,-1) In my previous mess-age, my five equations implicitly decomposed this domain into nine regions, namely the midpoint (0,0) (equation (2)), the four lines leading out of it (equation (3)), the upper and lower diamonds (equation (4)), and the left and right diamonds (equation (5)). For the geometric description of Fm, a simpler decomposition suffices, namely three regions: the upper and lower diamonds as one region, call it M for Middle, and the interior of each side diamond along with its outer sides, call them L and R. (So M is closed and L + R = IxI - M.) (1,1) /\ / \ . (1,0) (0,1) . / . \ / . \ / . \/ . \ (1,-1)< L . M (0,0) . R >(-1,1) \ . /\ . / \ . / \ . / . (0,-1) (0,1) . \ / \/ (-1,-1) In addition we need one more region, S for Shrunk, as a subregion of IxI v IxI, shown below. S is simply IxI v IxI shrunk in half (or pushed twice as far away). /\ / \ / \ / \ \ /\ / \/S \/ \ / \/ IxI v IxI /\ / \ /\ S/\ / \/ \ \ / \ / \ / \/ We now describe Fm as follows. Its restriction to M is the evident similarity between M and IxI v IxI. And its restriction to each of L and R lands in S, and in each case is the whole of Fm shrunk in half (the corecursion is essential, not even geometry can eliminate it). Note that these maps are defined on sequences, i.e. we are not assuming the metric we set out to construct. Fm as defined is not commutative, but can be made so by composing its restriction to L with commutativity of (x+y)/2, viz. reflection of L about its central vertical axis, thereby symmetrizing Fm. (This commutativity ambiguity also arose via equation (1) of my 5-equation approach.) This symmetrical Fm would appear to be the canonical choice for Freyd's midpoint coalgebra. (The apparent competitor obtained by reflecting R instead of L is slightly more discontinuous, if that's a reasonable tie breaker.) This coalgebra is of course not final, nor is it even injective, though it is surjective, witness subdomain M. It is also not continuous: points near (1,0) in L go to points near (1,(0,0)) in IxI v IxI, while points near (1,0) in M go to points near (1,(1,-1)) in IxI x IxI. On the other hand points near (1/2,0) in both M and L.M (the M of L) go to points near (1/2,0) in IxI v IxI, which has no counterpart in the above-mentioned competitor. Question. Is there a corecursively defined Freyd midpoint coalgebra that is continuous? (x,y) |--> ((x+y)/2,(x+y)/2) (projection onto the center axis) is a continuous midpoint coalgebra, but that assumes the metric before we've defined it. What corecursion would define this? Vaughan From rrosebru@mta.ca Mon Dec 27 13:12:35 1999 -0400 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA06855 for categories-list; Mon, 27 Dec 1999 11:15:59 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sun, 26 Dec 1999 13:45:08 -0500 (EST) From: Peter Freyd Message-Id: <199912261845.NAA19441@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Real midpoints Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 20 It could well be that Vaughan and I are defining the midpoint structure in the same way. Here's how I described it (using the conventions from my last posting). Let F:I --> I v I be a final coalgebra. We will denote the top of I as T and the bottom as B. Construct the "halving" map, h:I --> I, (on [-1,1] it will send x to x/2) as: T v F v B F'v F' F' I --> 1 v I v 1 ------> I v I v I v I ---> I v I --> I where F' denotes the inverse of F, and, by a little overloading, T and B denote the maps constantly equal to T and B. The leftmost map records the fact that the terminator is a unit for the ordered-wedge functor. Let g be the endo-function on I x I defined recursively by: g = if dx = T and dy = T then else if dx = T and uy = B then h(g(dx,uy>) else if ux = B and dy = T then h(g) else if ux = B and uy = B then . The values of g lie in the first and third quadrants, that is, those points such that either dx = dy = T or ux = uy = B. The two maps g d x d g u x u I x I --> I x I --> I x I and I x I --> I x I --> I x I give a coalgebra structure on I x I. The midpoint operation may be defined as the induced map to the final coalgebra. From rrosebru@mta.ca Fri Dec 31 11:20:14 1999 -0400 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA00752 for categories-list; Fri, 31 Dec 1999 09:42:43 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <199912290803.AAA30583@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Re: Real midpoints In-reply-to: Your message of "Sun, 26 Dec 1999 13:45:08 EST." <199912261845.NAA19441@saul.cis.upenn.edu> Date: Wed, 29 Dec 1999 00:03:53 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 21 From: Peter Freyd >It could well be that Vaughan and I are defining the midpoint structure >in the same way. Yes, after changing g(dx,uy) to g(ux,dy) in line 2 of Peter's definition of g and similarly for line 3 (otherwise g(dx,uy) simplifies to the nonsensical g(T,B)) Peter and I have essentially the same coalgebra on IxI, and exactly the same after some inessential permutations within that definition. While I rather like Peter's nonrecursive definition T v F v B F'v F' F' I --> 1 v I v 1 ------> I v I v I v I ---> I v I --> I of the halving map h:I --> I sending x to x/2, it should be remarked that the effect of this map as an operation on sequences is to preserve the empty sequence, and for nonempty sequences simply to prepend a copy of the leading digit, e.g. -++-+000... becomes --++-+000.... (This takes the 3-symbol alphabet for Peter's number system to be {-,0,+}.) In other words, right shift by one with sign extension, a well-known realization of halving. Along the same lines, Peter's d and u maps shift the sequence left. If d (resp. u) shifts a + (resp. -) off the left end, the result is replaced by the constantly + (resp. -) sequence, i.e. "clamp overflow to +1 (resp. -1)". Although the interval [-1,1] goes naturally with Peter's final coalgebra, it occurrs to me that a fragment of Conway's surreal numbers is perfectly matched to it, namely the interval [-\omega,\omega] consisting of the real line plus two endpoints. With respect to the Conway story this can be described as what Conway produces by day omega, modulo infinitesimals (identify those surreals that are only infinitesimally far apart). At no day does exactly the real line appear in Conway's scenario. Prior to day omega only the finite binary rationals have appeared. Day omega sees the sudden emergence of all the reals along with 1/omega added to and subtracted from each rational, as well as -omega and omega. Except for -omega and omega, the quotienting eliminates the 1/omega perturbations, yielding exactly the real line plus endpoints. Exactly the same quotienting happens with Peter's final coalgebra, whose elements are representable as finite and infinite strings over {-,+} (the 0 is eliminated by allowing strings to be finite; if you want all strings to be infinite, put 0 back in the alphabet and use it to pad the infinite strings to infinity). For example ---+++++... and --+----... are identified by both Conway and Freyd. Using Peter's choice of [-1,1] as the represented interval, these are both -1/4. Using Conway's number system, these are respectively -2 - 1/omega and -2 + 1/omega, which with the identification I described above become -2. In Conway's setup the finite constant sequences are the integers, with the empty sequence being 0 and counting being done in unary. At the first sign reversal the bits jump mysteriously from unary to binary, not by fiat but as a surprising consequence of a definition of addition that on the face of is so natural that you would not dream it could cause a radix jump like that. So both [-1,1] and [-omega,omega] each admit a natural final coalgebra structure for Peter's functor, namely Peter's and Conway's respectively, and I would be surprised to see a different final coalgebra in either case that was as natural. In contrast, Dusko and I exhibited a number of more or less equally convincing final coalgebra structures on [0,1) and [0,omega) for the functor product-with-omega, no one of which I would be willing to call *the* right one. Vaughan From rrosebru@mta.ca Fri Dec 31 21:57:31 1999 -0400 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA31833 for categories-list; Fri, 31 Dec 1999 20:14:46 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 31 Dec 1999 17:54:56 -0500 (EST) From: Peter Freyd Message-Id: <199912312254.RAA21550@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Pre-calculus Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 22 Starting with the closed interval, regarded as an ordered midpoint algebra with duality, what's the best way to get the reals? My previous answer was first to reflect the midpoint algebra in the subcategory of abelian groups and then define the multiplication via monotonic endomorphisms. I think there's a more natural way. First, a re-cap of the definitions. A midpoint operation is a binary operation, with values here denoted as x|y, satisfying: idempotence, x|x = x; commutativity, x|y = y|x; middle-two-interchange, (u|v)|(x|y) = (u|x)|(v|y); and cancelation, x|y = x|z => y = z. The closed interval is a totally ordered midpoint algebra with anti-involution, with values here denoted as -x. It follows that there's a unique element of the form (-x)|x. We'll call it the center. The middle-two-interchange law is just what is needed to see that the monoid of midpoint-endomorphisms is itself a midpoint algebra (where the midpoint of f and g is defined pointwise: (f|g)(x) = (fx)|(gx)). If f and g are both order-preserving or both order- reversing then it's easy to see that so is f|g. But we'll want all the _monotonic_ endomorphisms (the OED defines "monotonic" as "varying in such a way that it either never increases or never decreases") and there's no apparent reason to expect that monotonicity is preserved by midpointing. The wonderful fact, though, is: Midpoint-preserving functions between intervals are monotonic. (The axiom of choice yields 2^{2^N} counterexamples if the interval is replaced by the reals.) It follows that a midpoint-preserving function is determined by its values on any two points. The monoid of midpoint- and duality- preserving endo-functions on a closed interval is naturally isomorphic (via evaluation at Top) to the closed interval. For the entire reals use the stalk at the center of the germs of such functions. PS For a proof suppose that f:[-1,1] --> [-K,K] preserves midpoints and duality. For any x:[-1,1] and dyadic rational q such that qx:[-1,1], we may uniquely identify qx using just midpoints and duality, hence f(qx) = qf(x). Suppose that f is not monotonic. We wish to reach a contradiction. Let u < v and x < y in [-1,1] be such that fu < fv and fx > fy. Define a = (-u)|v and b = (-x)|y to obtain a,b > 0 and fb < 0 < fa. Let q > 0 be a dyadic rational such that a/b - (fa)/(bK) < q < a/b and define c = (-qb)|a. Let r be a dyadic rational such that (2K)/(fa) < r < 1/c. Then rc is in [-1,1] but f(rc) can not be in [-K,K] (because fc > (fa)/2). The theorem I stated doesn't say anything about preserving duality. So let g be a midpoint-preserving function between intervals. Let a be the dual of the value of g at the center. Then the function \x.a|(gx) preserves the center and continues to preserve midpoints. Since -x may be uniquely identified by (-x)|x = 0 the preservation of the center implies preservation of the duality and \x.a|(gx) is monotonic. Since \y.a|y not only preserves but reflects the order, we know that g is monotonic.