From rrosebru@mta.ca Mon Oct 2 13:01:13 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA28445 for categories-list; Mon, 2 Oct 2000 11:49:58 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: To: categories@mta.ca Subject: categories: Preprint: Behavioural differential equations: a coinductive calculus of streams, automata, and power series Date: Mon, 02 Oct 2000 16:26:49 +0200 From: Jan Rutten Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 1 The following technical report is now available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R0023.ps.Z (also via my home page: http://www.cwi.nl/~janr): J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series Technical Report SEN-R0023, CWI, Amsterdam, 2000. Abstract: Streams, (automata and) languages, and formal power series are viewed coalgebraically. In summary, this amounts to supplying these sets with a deterministic automaton structure, which has the universal property of being final. Finality then forms the basis for both definitions and proofs by coinduction, the coalgebraic counterpart of induction. Coinductive definitions take the shape of what we have called behavioural differential equations, after Brzozowski's notion of input derivative. A calculus is developed for coinductive reasoning about all of the afore mentioned structures, closely resembling (and at times generalising aspects of) calculus from classical analysis. (This report combines and extends earlier papers on automata and languages (CONCUR '98) and formal power series (ICALP '99).) From rrosebru@mta.ca Mon Oct 2 20:31:31 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA05324 for categories-list; Mon, 2 Oct 2000 19:29:10 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 03 Oct 2000 00:06:36 +0200 From: mhebert Subject: categories: Manuscripts available To: categories@mta.ca Message-id: <39D57E29@mail.aucegypt.edu> MIME-version: 1.0 X-Mailer: WebMail (Hydra) SMTP v3.60 Content-type: text/plain; charset="ISO-8859-1" X-WebMail-UserID: mhebert X-EXP32-SerialNo: 00002917 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id TAA02083 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 2 The following manuscripts are available on request, or can be downloaded in postscript form from http://www.aucegypt.edu/schools/sse/maths/Staff/Hebert/HebertHomePage.htm On abstract data types presented by multiequations J.Adamek, M Hebert, J.Rosicky. Abstract: Equational presentation of abstract data types is generalized to presentation by multiequations, i.e., exclusive-or's of equations, in order to capture parametric data types such as array or set. Multiinitial-algebra semantics for such data types is introduced. Classes of algebras described by multiequations are characterized. Uncountable orthogonality is a closure property M.Hebert, J.Rosicky Abstract: We show that, for lambda-orthogonality classes in locally lambda-presentable categories coincide with full subcategories closed under limits and lambda-directed colimits. This comes as a surprise, since the statement is known to be false for lambda = omega. More on orthogonality in locally presentable categories M. Hebert, J. Adamek and J. Rosicky Abstract: A new solution of the orthogonal subcategory problem in locally presentable categories is exhibited, substantially different from the classical one of Gabriel and Ulmer. It has various applications: we use it to characterize omega-orthogonality classes in locally finitely presentable categories, i.e., the full subcategories orthogonal to a set of morphisms the domains and codomains of which are finitely presentable. We also use it to find a sufficient condition for reflectivity of subcategories of accessible categories. And finally, we describe categories of fractions in all small, finitely complete categories. Lambda*-injectivity + special lambda-compactness = lambda-injectivity Michel Hébert Abstract: J.Rosicky, J.Adamek and F.Borceux recently showed that lambda-injectivity classes in locally presentable categories are precisely the classes closed under products, lambda-filtered colimits and lambda-pure subobjects. We present a simpler and more conceptual proof of this result, obtaining it as a consequence of our characterization of lambda-injectivity classes (JPAA 129 (1998) 143-147) and of an infinitary compactness result. From rrosebru@mta.ca Wed Oct 4 20:25:42 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA11575 for categories-list; Wed, 4 Oct 2000 19:34:28 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39D9A7BD.8A80A634@dcs.kcl.ac.uk> Date: Tue, 03 Oct 2000 09:32:45 +0000 From: Jane Spurr Reply-To: jane@dcs.kcl.ac.uk X-Mailer: Mozilla 4.5 [en] (X11; I; Linux 2.2.12-20 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: History of Logic Workshop announcement Content-Type: text/plain; charset=iso-8859-1 X-MIME-Autoconverted: from 8bit to quoted-printable by helium.dcs.kcl.ac.uk id JAA00321 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id FAA14726 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 3 The Second DeMorgan Workshop on the History of Logic is to be held at King's College, London on Monday 6th and Tuesday 7th November The programme is as follows: Monday 6th November 9.00 - 9.30 Registration 9.30-10.30 John Woods:& Intro to Handbook/ Aristotle's earlier logic 10.30-11.30 Coffee 11.30-12.30 Andrew Jones: Topics in deontic logic 12.00-14.00 Lunch 14.00-15.00 I. Grattan-Guinness: The mathematicalc turn in logic 15.00-15.30 Tea 15.30-16.30 Graham Priest: Paraconsistent Logic 16.30-17.30 Wilfrid Hodges: Logic vs theory of language in the late 19th century Tuesday 7th November 9.00-10.00 Stephen Read: The Liar Paradox 10.00-10.30 Coffee 10.30-11.30 G. Boger: Aristotle's later logic 11.30-12.30 C Burnett: Latin Translations of arabic texts in the middle ages and renaissance 12.30-14.00 Lunch 14.00-15.00 J. Ganeri: Indian logic 15.00-15.30 Tea 15.30-17.30 D. M. Gabbay: The Way Forward / Panel To cover the cost of administration and refreshments, there will be a registration fee in the region of £10. If you wish to attend, please contact Jane Spurr: jane@dcs.kcl.ac.uk -- Please note new telephone numbers!! Department of Computer Science, tel: + (0)20 7848 2987 King's College, Strand, fax: + (0)20 7240 1071 London WC2R 2LS. email: jane@dcs.kcl.ac.uk From rrosebru@mta.ca Wed Oct 4 20:25:42 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA10647 for categories-list; Wed, 4 Oct 2000 19:36:22 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200010031110.IAA11206@mailserv.mta.ca> Date: Tue, 03 Oct 2000 07:07:56 EDT From: Rohit Parikh Subject: categories: Open position at City University Graduate Center To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 ========================================================================== Ph.D. Program in Computer Science Professor The CUNY Graduate Center seeks Professor with outstanding record or Associate Professor with great promise. Program is looking for an individual who has had major impact in the field, is active in preferably more than one area, has a consistent grant record, and some of whose work is applied. A distinguished candidate of substantial merit with an international reputation may be nominated as Distinguished Professor. Primary responsibilities include teaching doctoral-level students, research, departmental service, and supervision of dissertations. Requires: earned doctorate; record of significant (for Associate) or exceptional (for full) academic achievement; demonstrated ability to teach graduate students successfully. Review of applications begins 10/31/00. Send letter of application, curriculum vitae, and names and addresses of three references to: Search Committee Chair Ph.D. Program in Computer Science CUNY Graduate Center 365 Fifth Avenue New York, NY 10016 EO/AA/IRCA/ADA Employer From rrosebru@mta.ca Wed Oct 4 20:25:54 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA28609 for categories-list; Wed, 4 Oct 2000 19:30:35 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Subject: categories: PSSL 74 -- Second announcement To: categories@mta.ca Date: Wed, 4 Oct 2000 15:24:00 +0100 (BST) X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: From: "Dr. P.T. Johnstone" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 PSSL 74 -- Second announcement The 74th meeting of the Peripatetic Seminar on Sheaves and Logic (wrongly labelled the 73rd meeting in the previous announcement) will be held in the new Centre for Mathematical Sciences, University of Cambridge, on the weekend of 4--5 November 2000. As usual, we invite contributions from anyone interested in the application of categorical and sheaf-theoretic methods in logic and theoretical computer science. If you wish to attend, please complete the attached registration form and return it to ptj@dpmms.cam.ac.uk as soon as possible, and in any case by Wednesday 25 October. We shall attempt to reserve accommodation, either in College guest rooms or in local `bed and breakfast' accommodation, for all those who request it; but if you want us to do this please let us know as early as you can. Further information on accommodation, and a provisional programme, will be circulated about a week before the meeting. Martin Hyland Peter Johnstone Tom Leinster ------------------------------------- REGISTRATION FORM Name: Address: E-mail: I intend to come to the 74th meeting of the PSSL. *I should like to give a talk lasting about _____ minutes, entitled: *I should like to reserve accommodation for *Friday/Saturday/Sunday* night(s). * Please delete if inapplicable. From rrosebru@mta.ca Wed Oct 4 20:29:50 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA29390 for categories-list; Wed, 4 Oct 2000 19:32:22 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: TACS 2001 CFP Reply-to: bcpierce@cis.upenn.edu Date: Mon, 02 Oct 2000 13:54:11 EDT Message-ID: <1084.970509251@saul.cis.upenn.edu> From: "Benjamin C. Pierce" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 Preliminary Call for Papers Fourth International Symposium on Theoretical Aspects of Computer Science (TACS 2001) October 29-31, 2001 Tohoku University, Sendai, Japan The TACS Symposium will focus on the theoretical foundations of programming and their applications. The topics of interest include... Theoretical aspects of the design, semantics, analysis, and implementation of programming languages and systems; logics of programs; calculi and models of concurrency and parallel computation; theories of mobile computation and system security; categories and types in computer science; formalisms, methods, and systems for program specification, verification, synthesis, and optimization; constructive, linear, and modal logics in computer science. The scientific program will consist of invited lectures, contributed talks, and demo sessions. A proceedings containing the full papers of the invited and contributed talks will be published by Springer-Verlag as a volume of Lecture Notes in Computer Science. IMPORTANT DATES Submission deadline: April 1, 2001 Notification to authors: June 15, 2001 Deadline for final versions: July 20, 2001 INVITED SPEAKERS Luca Cardelli Microsoft Research Daniel Jackson Massachusetts Institute of Technology Christine Paulin-Mohring Universite Paris Sud & INRIA Andrew Pitts University of Cambridge Jon Riecke Lucent Technologies Kazunori Ueda Waseda University CONFERENCE CHAIR: Takayasu Ito Tohoku University PROGRAM CO-CHAIRS: Naoki Kobayashi University of Tokyo koba@is.s.u-tokyo.ac.jp Benjamin Pierce University of Pennsylvania bcpierce@cis.upenn.edu PROGRAM COMMITTEE: Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann Edinburgh University Zhenjiang Hu University of Tokyo Naoki Kobayashi University of Tokyo Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark Edinburgh University Makoto Tatsuta Kyoto University SUBMISSION INFORMATION Authors are invited to submit full papers (up to 6000 words, including figures and bibliographies). Papers must be unpublished and not submitted for publication elsewhere. Submissions should be in Postscript format, on A4 or US letter pages. They must be printable on common printers and viewable with ghostview. The first page of each submission should include the email address, telephone, and fax numbers of the corresponding author. Accepted papers must be presented at the symposium, and the final manuscript must be prepared in the LNCS format. Detailed submission procedure will be announced later at the TACS 2001 web page (http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/). From rrosebru@mta.ca Thu Oct 5 17:08:06 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA14932 for categories-list; Thu, 5 Oct 2000 15:35:54 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39DCA14A.1A7C3E29@iml.univ-mrs.fr> Date: Thu, 05 Oct 2000 17:42:02 +0200 From: Paul RUET Organization: Institut de =?iso-8859-1?Q?Math=E9matiques?= de Luminy X-Mailer: Mozilla 4.51 [en] (X11; I; Linux 2.2.5-15 i686) X-Accept-Language: fr, en, it MIME-Version: 1.0 To: linear-tmr-book@iml.univ-mrs.fr Subject: categories: CFP : Book on Linear Logic Content-Type: multipart/alternative; boundary="------------6153BCBA80A4F824A502B96B" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 7 --------------6153BCBA80A4F824A502B96B Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit CALL FOR PAPERS Book on Linear Logic On the occasion of its International Summer School http://linear.di.fc.ul.pt/ held in the Azores from August 30 to September 7, 2000, the TMR Linear network http://iml.univ-mrs.fr/ldp/LINEAR/ wishes to edit a book devoted to recent advances in Linear Logic. This book will consist of a few invited papers and some refereed contributions (not necessarily written by people who gave a talk at the School). All submitted contributions will be refereed. They must be in English and may not exceed 25 pages, and the results must be unpublished and not submitted for publication elsewhere, including the proceedings of symposia or workshops. Submissions (in postscript format) must be sent by E-mail to linear-tmr-book@iml.univ-mrs.fr by February 1st, 2001. Suggested, but not exclusive, topics of interest for submissions include: * Proof theory: proof-nets, ludics, non-commutative logic, proof theory of classical logic. * Complexity: polynomial and elementary linear logics, decision problems, feasible arithmetics. * Semantics: phase semantics, categorical semantics, denotational semantics, game semantics, geometry of interaction. * Concurrency: categorical models for concurrency, interaction nets. * Applications: sharing reductions in lambda-calculus and optimality, linear functional programming, linear constraint logic programming, proof search and focalisation. Submission deadline: February 1st, 2001. Tentative publisher: Cambridge University Press, in the "London Mathematical Society Lecture Note Series". Editorial board: Thomas Ehrhard Jean-Yves Girard Paul Ruet Phil Scott --------------6153BCBA80A4F824A502B96B Content-Type: text/html; charset=us-ascii Content-Transfer-Encoding: 7bit CALL FOR PAPERS
Book on Linear Logic

On the occasion of its International Summer School

http://linear.di.fc.ul.pt/
held in the Azores from August 30 to September 7, 2000, the TMR Linear network
http://iml.univ-mrs.fr/ldp/LINEAR/
wishes to edit a book devoted to recent advances in Linear Logic. This book will consist of a few invited papers and some refereed contributions (not necessarily written by people who gave a talk at the School). All submitted contributions will be refereed. They must be in English and may not exceed 25 pages, and the results must be unpublished and not submitted for publication elsewhere, including the proceedings of symposia or workshops. Submissions (in postscript format) must be sent by E-mail to
linear-tmr-book@iml.univ-mrs.fr
by February 1st, 2001.

Suggested, but not exclusive, topics of interest for submissions include:

  • Proof theory: proof-nets, ludics, non-commutative logic, proof theory of classical logic.
  • Complexity: polynomial and elementary linear logics, decision problems, feasible arithmetics.
  • Semantics: phase semantics, categorical semantics, denotational semantics, game semantics, geometry of interaction.
  • Concurrency: categorical models for concurrency, interaction nets.
  • Applications: sharing reductions in lambda-calculus and optimality, linear functional programming, linear constraint logic programming, proof search and focalisation.
Submission deadline: February 1st, 2001.

Tentative publisher:
Cambridge University Press, in the "London Mathematical Society Lecture Note Series".

Editorial board:
Thomas Ehrhard
Jean-Yves Girard
Paul Ruet
Phil Scott
  --------------6153BCBA80A4F824A502B96B-- From rrosebru@mta.ca Tue Oct 10 17:18:40 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9AJ7g930050 for categories-list; Tue, 10 Oct 2000 16:07:42 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 9 Oct 2000 18:28:29 -0400 (EDT) From: Andre Scedrov Message-Id: <200010092228.e99MSTB06613@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: CFP: Computer Security Foundations Workshop Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 9 Call For Papers 14th IEEE Computer Security Foundations Workshop June 11-13, 2001 Keltic Lodge, Cape Breton, Nova Scotia, Canada Sponsored by the Technical Committee on Security and Privacy of the IEEE Computer Society This workshop series brings together researchers in computer science to examine foundational issues in computer security. For background information about the workshop, and an html version of this Call for Papers, see the CSFW home page http://www.csl.sri.com/csfw/csfw14/ This year the workshop will be in Cape Breton, Nova Scotia, Canada. We are interested both in new results in theories of computer security and also in more exploratory presentations that examine open questions and raise fundamental concerns about existing theories. Both papers and panel proposals are welcome. Possible topics include, but are not limited to: access control authentication data and system integrity database security network security distributed systems security anonymity intrusion detection security for mobile computing security protocols security models decidability issues privacy executable content formal methods for security information flow The proceedings are published by the IEEE Computer Society and will be available at the workshop. Selected papers will be invited for submission to the Journal of Computer Security. Instructions for Participants ----------------------------- Submission is open to anyone. Workshop attendance is limited to about 40 participants. Submitted papers must not substantially overlap papers that have been published or that are simultaneously submitted to a journal or a conference with a proceedings. Papers should be at most 20 pages excluding the bibliography and well-marked appendices (using 11-point font, single column format, and reasonable margins on 8.5"x11" paper), and at most 25 pages total. The page limit will be strictly adhered to. Committee members are not required to read the appendices, and so the paper should be intelligible without them. Proposals for panels should be no longer than five pages in length and should include possible panelists and an indication of which of those panelists have confirmed participation. To submit a paper, send to s.schneider@rhbnc.ac.uk a plain ASCII text email containing the title and abstract of your paper, the authors' names, email and postal addresses, phone and fax numbers, and identification of the contact author. To the same message, attach your submission (as a MIME attachment) in PDF or portable postscript format. Do not send files formatted for word processing packages (e.g., Microsoft Word or WordPerfect files). Submissions received after the submission deadline or failing to conform to the guidelines above risk rejection without consideration of their merits. Where possible all further communications to authors will be via email. If for some reason you cannot conform to these submission guidelines, please contact the program chair at s.schneider@rhbnc.ac.uk. Important Dates --------------- Submission deadline: February 1, 2001 Notification of acceptance: March 16, 2001 Camera-ready papers: April 5, 2001 Program Committee Pierre Bieber, ONERA, France Ed Clarke, Carnegie Mellon University, USA Riccardo Focardi, University of Venice, Italy Dieter Gollmann, Microsoft Research, UK Li Gong, Sun Microsystems, USA Carl Gunter, University of Pennsylvania, USA Joshua Guttman, MITRE, USA Gavin Lowe, Oxford University, UK Teresa Lunt, Xerox PARC, USA Fabio Martinelli, IAT-CNR, Italy John McLean, Naval Research Laboratory, USA Ravi Sandhu, George Mason University, USA Andre Scedrov, University of Pennsylvania, USA Steve Schneider (chair), Royal Holloway, University of London, UK Rebecca Wright, AT&T Labs, USA Workshop Location ----------------- The workshop will be held at the Keltic Lodge in beautiful Cape Breton, Nova Scotia. Located on a narrow peninsula on the Atlantic Ocean, the Lodge's comfortable rooms offer breathtaking views of the rugged shore, vibrant in sunny days and majestic when shrouded in mist. Activities on the premises include tennis, swimming in the heated pool, golf, and mountain biking. The picturesque fishing villages along the scenic Cabot Trail offer opportunities to get acquainted with the local lifestyle and also to embark in such activities as ocean swimming, whale watching, and sea kayaking. Moose, bears and other wildlife are often seen while hiking and camping in the surrounding Cape Breton Highlands National Park. Cape Breton also hosts the final home of Alexander Graham Bell and the station from which Guglielmo Marconi transmitted the first recorded East-bound radio signal across the Atlantic. The Keltic Lodge is 4 hours by car from Halifax International Airport along a magnificent drive. There are direct flights between Halifax and numerous European and American cities. Sydney Regional Airport is 1 1/2 hours by car from the Keltic Lodge and has flights every 2 hours to Halifax. People attending LICS 2001 in Boston may also consider the ferry between Portland, ME and Yarmouth, NS. More travel information can be found from the CSFW website. For further information contact: General Chair Iliano Cervesato ITT Industries, Inc. - AES Division 2560 Huntington Avenue Alexandria, VA 22303-1410 USA +1-202-404-4909 iliano@itd.nrl.navy.mil Program Chair Steve Schneider Department of Computer Science Royal Holloway, University of London Egham, Surrey, TW20 0EX UK +44 1784 443431 s.schneider@rhbnc.ac.uk Publications Chair Jonathan Herzog The MITRE Corporation 202 Burlington Road Bedford, MA 01730-1420 USA +1-781-271-2907 jherzog@mitre.org From rrosebru@mta.ca Tue Oct 10 19:29:34 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9ALo5g18091 for categories-list; Tue, 10 Oct 2000 18:50:05 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 10 Oct 2000 11:52:22 -0400 (EDT) From: Michael MAKKAI To: categories@mta.ca Subject: categories: correction 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: 10 This is a correction to the talk I gave in Toronto on the 24th of September. In the definition of "principal computad" (on page 8 of the slides, for those who have copies of the slides) a clause was omitted. The definition should read as follows (clause (c) was missing): The computad A is *principal* if (a) A is finite, (b) there is a unique indeterminate of maximal dimension in A, say x; and (c) there is no proper subcomputad of A containing x. I add that there was another error in the slides, although it was caught during the talk and corrected on the projected slide (but not on the copies). On page 11 of the slides, "fibration" should be "trivial fibration". Michael Makkai From rrosebru@mta.ca Wed Oct 11 15:44:08 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9BHun122770 for categories-list; Wed, 11 Oct 2000 14:56:49 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 11 Oct 2000 12:33:16 +0300 (EEST) From: Gheorghe Stefanescu X-Sender: ghstef@moisil.cs.unibuc.ro To: categories@mta.ca Subject: categories: Book: "Network Algebra" 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: 11 New book! G. Stefanescu, Network Algebra, Springer-Verlag, London/Berlin/... ISBN: 1-85233-195-X; XVI+402pp; GBP 37.50; softcover; April 2000 See also: http://funinf.cs.unibuc.ro/~ghstef/na/myAdv.html Network Algebra considers the algebraic study of networks and their behaviour. It contains general results on the algebraic theory of networks, recent results on the algebraic theory of models for parallel programs, as well as results on the algebraic theory of classical control structures. The results are presented in a unified framework of the calculus of flownomials, leading to a sound understanding of the algebraic fundamentals of the network theory. Network Algebra will be of interest to anyone interested in network theory or its applications and provides them with the results needed to put their work on a firm basis. Graduate students will also find the material within this book useful for their studies. Contents: An Introduction to Network Algebra: Short Overview on the key results. (http://funinf.cs.unibuc.ro/~ghstef/na/naIntr.ps.gz) Network Algebra and its applications. Relations, Flownomials and Abstract Networks: Networks modulo graph isomorphism. Algebraic models for branching constants. Network behaviour. Elgot theories. Kleene theories. Algebraic Theory of Special Networks: Flowchart schemes. Automata. Process Algebra. Dataflow Networks. Petri Nets. Towards an Algebraic Theory for Software Components: Mixed Network Algebra. Related Calculi, Closing Remarks. Appendices. Bibliography. (http://funinf.cs.unibuc.ro/~ghstef/na/naRef.ps.gz) List of Tables. List of Figures. Index. Stefanescu, G., University of Bucharest, Romania Publication date: April 12, 2000; DM 119,- Recommended List Price Written for: Graduates, practitioners Book category: Graduate Textbook Publication language: English Series: Discrete Mathematics and Theoretical Computer Science. Last update: 08.04.2000 From rrosebru@mta.ca Sun Oct 15 16:32:06 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9FIqt319739 for categories-list; Sun, 15 Oct 2000 15:52:55 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Thu, 12 Oct 2000 10:22:38 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: Preprints: On Mackey topologies ... and On *-autonomous ... 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: 12 I have just posted two papers to ftp.math.mcgill.ca/pub/barr. The first is: mackey M. Barr and H. Kleisli, On Mackey topologies in topological abelian groups. Submitted to TAC. The main result can be described as follows: Let C be a full subcategory of topological abelian groups that includes the circle group T and closed under subobjects and projects. For a group A, let A^ denote the abstract group of all its characters, that is continuous homomorphisms to the circle. If A is an object of C, say that A' has a compatible topology if it has the same elements and the same characters are A and say that A' has a Mackey topology if it has the finest compatible topology. Say that C has Mackey coreflections if the inclusion of the full subcategory of Mackey groups has a right adjoint. Then we show, among other things, that the existence of Mackey coreflections is equivalent to the injectivity of the circle in C and then the Mackey category is equivalent to chu(Ab,T). The second is: tvs On *-autonomous categories of topological vector spaces. To appear in Cahiers de Topologie et Geometrie Differentielle Categorique. The main result here is that the category of Mackey spaces (defined similarly in terms of continuous linear functionals and proved by Mackey to be coreflective) among the locally convex TV spaces is equivalent to chu(Vect,K), where K is the field of scalars (either R or C) and is therefore *-autonomous. Another fact adduced is that--unusually-- chu(Vect,K) is a *-autonomous subcategory of Chu(Vect,K). Sometime in the next week or so, I will be posting derfun Effaceable resolutions and derived functors. Submitted to HHA. It is well known that to define the derived functors, say, of Tor, it is sufficient to use flat resolutions. The usual proofs of this fact use the existence of projective resolutions to do this. For example, to infer functoriality, you use the possibility of lifting resolutions. Suppose, for example, you are in a category of modules over a sheaf of rings in a topos. Generally, there are no projectives (save 0), but the sheaves associated to representable functors are flat. More generally, suppose that T: A --> C is a right exact functor between abelian categories. Call an object E T-effaceable if whenever 0 --> A --> B --> E -->0 is exact, then TA --> TB is monic. Assume as a hypothesis that the kernel of an epimorphism between eeffaceables is effaceable and that every object is the target of an epimorphism from an effaceable. Then derived functors are definable using effaceable resolutions. From rrosebru@mta.ca Sun Oct 15 16:32:07 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9FItkK08201 for categories-list; Sun, 15 Oct 2000 15:55:46 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 13 Oct 2000 13:57:22 +0200 (MET DST) From: Catherine Piliere Message-Id: <200010131157.NAA03239@lorraine.loria.fr> To: categories@mta.ca X-Mailer: Perl Mail::Sender 0.7.01 Jan Krynicky http://jenda.krynicky.cz/ X-Mailer: mailliste Subject: categories: LACL 2001 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 13 ***************************************************************** CALL FOR PAPERS --- Please accept our apologies for multiple copies --- ***************************************************************** LACL 2001 4th International Conference on LOGICAL ASPECTS OF COMPUTATIONAL LINGUISTICS June 27 -- 29, 2001 Le Croisic, France ***************************************************************** HISTORY The LACL series of conferences aims at providing a forum for the presentation and discussion of current research in all the formal and logical aspects of computational linguistics. It started as a workshop held in Nancy (France), in 1995. Due to its success, it was turned, the next year, into a international conference. LACL'96 and'97 have both been held in Nancy (France). LACL'98 has been held in Grenoble (France). Selected papers from LACL'95 appear in a special issue of Journal of Logic Language and Information, 7(4), 1998. The proceedings of LACL'96 and 97 appear as volumes 1328 and 1582 of Lecture Notes in Artificial Intelligence. The proceedings of LACL'98 are in press with the same series. SCOPE Typical topics include, but are not limited to: Categorial grammars, Categorial type logics, Compositionality, Discourse representation theory, Dynamics, Feature Logics, Formal language theory, Game-theoretical semantics, Grammatical inference, Learning theory, Linear logical frameworks, Minimalism, Modal logics, Montague semantics, Parsing as deduction, Proof- theoretic approaches, Situation semantics and situation theory, Type-theoretic approaches. SUBMISSION GUIDELINES Authors are invited to submit a full paper not exceeding 15 standard A4 or US quarto pages. The paper should allow the Programme Committee to assess the merits of the work. In particular, references and comparisons with related work should be included. Submission of material already published or submitted to other conferences with published proceedings is not allowed. Electronic submission is highly recommended. A postscript version of the paper should be sent as an e-mail to: to arrive by January 29, 2001. Authors are strongly encouraged to use LaTeX2e and the Springer llncs class file In addition, a separate e-mail containing the title of the paper, authors' names and addresses, and a short abstract in plain ASCII format should be sent to the same e-mail address. If electronic submission is not possible, authors may submit four hard copies of the paper by post to the following address: LACL 2001 (Attention: G. Morrill) UPC, Departament de LSI Campus Nord - Modul C6 Jordi Girona Salgado, 1-3 E-08034 Barcelona - Espanya IMPORTANT DATES Deadline for Submissions: January 29, 2001 Notification to Authors: March 26, 2001 Final Versions due: April 20, 2001 CONFERENCE PROCEEDINGS The accepted papers will be published as a volume of Springer Lecture Notes in AI. This will be available at the time of the conference. PROGRAM COMMITTEE W. Buszkowski (Poznan) R. Crouch, (Palo Alto) A. Dikovsky (Nantes) M. Dymetman (Grenoble) C. Gardent (Saarbrucken) P. de Groote (Nancy), co-chair M. Kanazawa (Tokyo) G. Morrill (Barcelona), co-chair R. Muskens (Tilburg) F. Pfenning (Pittsburgh) B. Rounds, (Ann Arbor) E. Stabler (Los Angeles) ORGANIZING COMITTEE B. Daille (Nantes) A. Dikovsky (Nantes) A. Foret (Rennes) E. Lebret (Rennes) C. Piliere (Nancy), publicity chair C. Retore (Rennes), chair P. Sebillot (Rennes) URL http://www.irisa.fr/LACL2001 From rrosebru@mta.ca Sun Oct 15 16:32:17 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9FIsu321049 for categories-list; Sun, 15 Oct 2000 15:54:56 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 13 Oct 2000 13:04:43 +0200 (MET DST) From: Furio Honsell X-Sender: honsell@farfarello To: categories@mta.ca Subject: categories: FoSSaCS'01 deadline is Oct, 20 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: 14 [Apologies for multiple copies] FoSSaCS 2001 - Foundations of Software Science and Computation Structures An ETAPS 2001 conference - Genova, Italy, 2 - 6 April, 2001 *** DEADLINE: October 20, 2000 *** Full call for papers and submission page at http://fossacs.dimi.uniud.it/ ETAPS page is at http://www.disi.unige.it/etaps2001/ FoSSaCS seeks papers which offer progress in foundational research with a clear significance to Software Sciences. Central objects of interest are the algebraic, categorical, logical, and geometric theories, models, and methods which support the specification, synthesis, verification, analysis, and transformation of sequential, concurrent, distributed, and mobile programs and software systems. Topics covered are in: Semantic foundations of Computation and Software Sciences: e.g., type theory, domain theory, category theory; Operational and syntactic foundations of Computation and Software Sciences: e.g., - computation processes over discrete and continuous data, - techniques for their manipulation, and analysis of their algorithmic properties; - formal descriptions of general frames for the integration of specification techniques; - automata; - techniques for proving properties of protocols; - transition systems; - models of concurrency interactive and reactive systems, and corresponding calculi, algebras, and logics. From rrosebru@mta.ca Mon Oct 16 11:39:36 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9GEApB29996 for categories-list; Mon, 16 Oct 2000 11:10:51 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Stefan Milius Message-Id: <200010160955.LAA01747@lisa.iti.cs.tu-bs.de> Subject: categories: New mailing list To: categories@mta.ca Date: Mon, 16 Oct 2000 11:55:18 +0200 (MET DST) X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 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: 15 Dear Colleagues, we would like to offer a new mailing list: Algebraic and Coalgebraic Methods in Computer Science the aim of which is to provide background for 1. information on available preprints 2. discussion 3. queries 4. conference announcements in all areas concerned with applications of (co)-algebraic methods in Computer Science. The new coalgebras list will be moderated by one of us to avoid unwanted postings (such as spam) to the list. If you wish to join the mailing list please send an email containing only the word subscribe in the mail's body to coalgebras-request@iti.cs.tu-bs.de Postings to the list should be sent to coalgebras@iti.cs.tu-bs.de We are currently also setting up a web site for the coalgebras list at the URL http://www.iti.cs.tu-bs.de/~coalgebras If you have any questions or comments regarding the list or the web site please do not hesitate to contact the moderator of the list at owner-coalgebras@iti.cs.tu-bs.de Yours sincerely Jiri Adamek & Stefan Milius Technical University of Braunschweig, Germany p.s. Sorry, if you receive multiple copies of this email. From rrosebru@mta.ca Mon Oct 16 11:44:24 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9GDw8N26286 for categories-list; Mon, 16 Oct 2000 10:58:08 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39E74582.BB0A039C@comlab.ox.ac.uk> Date: Fri, 13 Oct 2000 18:25:22 +0100 From: Samson Abramsky Organization: Oxford University Computing Laboratory, UK X-Mailer: Mozilla 4.75 [en] (X11; U; SunOS 5.7 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: TLCA 2001: DEADLINE EXTENSION 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: 16 This is to announce a deadline extension for: Fifth International Conference on Typed Lambda-Calculi and Applications which will be held in Krakow, Poland, May 2nd-5th, 2001. The new extended deadline is: MONDAY OCTOBER 30TH 2000. The scientific scope of TLCA is quite broad, and includes topics from proof theory and semantics to types and logical frameworks, and functional and logic programming. The original call-for-papers follows: (see also the home page at http://www.ii.uj.edu.pl/zpi/tlca2001/) ******************************************************** * * TLCA 2001 * * 5th International Conference on * Typed Lambda Calculi and Applications * May 2 -- 5, 2001 * Krakow, Poland * ******************************************************** * CALL FOR PAPERS ******************************************************** The TLCA series of conferences aims at providing a forum for the presentation and discussion of current research in a field which was originally rather restricted, but has now expanded considerably. Typical areas include, but are not limited to: Proof theory: Natural Deduction and Sequent Calculi, Cut elimination and Normalization, Computational interpretations of Classical Logic, Linear Logic and Proof Nets, Bounded systems capturing complexity classes Semantics: Denotational semantics, Operational semantics, Game semantics, Realizability, Categorical models, Logical Relations, Full Completeness Implementation: Abstract machines, Parallel execution, Optimal Reduction Types: Polymorphism, Dependent types, Intersection types, Subtypes Logical Foundations: Logical Frameworks, Pure Type Systems, Proof checking Programming: Foundational aspects of: Functional programming, Proof search and logic programming, Connections between and combinations of functional and logic programming, Type checking, Higher-order rewriting, Higher-order unification and matching Important Dates =============== Deadline for Submissions: October 9, 2000 Notification to Authors: December 18, 2000 Final Versions due: February 1, 2001 The accepted papers will be published as a volume of the Springer Lecture Notes in Computer Science. Information about LNCS can be found at: http://www.springer.de/comp/lncs/index.html Submission Guidelines ===================== Papers should not exceed 15 standard A4 or US quarto pages, and should allow the Programme Committee to assess the merits of the work: in particular, references and comparisons with related work should be included. Submission of material already published or submitted to other conferences with published proceedings is not allowed. If available, e-mail addresses and fax numbers of the authors should be included. Electronic submissions ====================== Electronic submissions are strongly encouraged. A gzipped Postscript version of the paper should be sent as an e-mail message to: tlca01@comlab.ox.ac.uk In addition, the following information in ASCII format should be sent to this address in a **separate** e-mail: Title; authors; communicating author's name, address, and e-mail address and fax number if available; abstract of paper. Hard-copy submissions ===================== If electronic submission is not possible, authors may submit five (5) hard copies of the paper by post to the following address: TLCA 2001 (Attention: S. Abramsky) Oxford University Computing Laboratory Wolfson Building Parks Road Oxford OX1 3QD United Kingdom Questions concerning submissions ================================ These should be addressed to the Program Chair, Samson Abramsky: samson@comlab.ox.ac.uk Program Committee ================= S. Abramsky (Oxford) (chair) P.-L. Curien (Paris) P. Dybjer (Goteborg) T. Ehrhard (Marseille) M. Hasegawa (Kyoto) F. Honsell (Udine) D. Leivant (Bloomington) S. Ronchi della Rocca (Turin) H. Schwichtenberg (Munich) P. Scott (Ottawa) J. Tiuryn (Warsaw) Organizing Committee ==================== M. Zaionc (chair) TLCA 2001 web page ================== http://www.ii.uj.edu.pl/zpi/tlca2001/ From rrosebru@mta.ca Tue Oct 17 16:11:38 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9HIFC112334 for categories-list; Tue, 17 Oct 2000 15:15:12 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 Message-Id: Date: Tue, 17 Oct 2000 15:17:00 +0100 To: etaps2001@disi.unige.it From: Etaps 2001 Subject: categories: ETAPS 2001: Deadline Approaching Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 17 ETAPS 2001 APRIL 2 - 6, 2001 - GENOVA, ITALY The European Joint Conferences on Theory and Practice of Software (ETAPS) is a loose and open confederation of conferences and other events that has become the primary European forum for academic and industrial researchers working on topics relating to Software Science. http://www.disi.unige.it/etaps2001/ ----------------------------------------------------------------------- 5 Conferences - Tutorials - Tool Demonstrations - 9 Satellite Events ----------------------------------------------------------------------- CONFERENCES ----------------------------------------------------------------------- CC 2001: International Conference on Compiler Construction Chair: Reinhard Wilhelm ESOP 2001, European Symposium On Programming Chair: David Sands FASE 2001, Fundamental Approaches to Software Engineering Chair: Heinrich Hussmann FOSSACS 2001, Foundations of Software Science and Computation Structures Chair: Furio Honsell TACAS 2001, Tools and Algorithms for the Construction and Analysis of Systems Chairs: Tiziana Margaria and Wang Yi Prospective authors are invited to submit, **** BEFORE OCTOBER 20, 2001, **** full papers in English presenting original research. People who cannot submit electronically or who have exceptional conflicts with the submission deadline should contact the relevant PC chair directly. Submitted papers must be unpublished and not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. The proceedings of each main conference will be published as a separate volume in the Springer Verlag Lecture Notes in Computer Science series. TUTORIALS ----------------------------------------------------------------------- Proposals for half-day or full-day tutorials related to ETAPS 2001 are invited. Tutorial proposals will be evaluated on the basis of their assessed benefit for prospective participants to ETAPS 2001. Contact: Bernhard Rumpe (Technische Universitaet Munchen, Germany) TOOL DEMONSTRATIONS ----------------------------------------------------------------------- Demonstrations of tools presenting advances on the state of the art are invited. Submissions in this category should present tools having a clear connection to one of the main ETAPS conferences, possibly complementing a paper submitted separately. These should not be confused with contributions to TACAS, which emphasizes principles of tool design, implementation, and use, rather than focusing on specific domains of application. Contact: Don Sannella (University of Edinburgh) SATELLITE EVENTS ----------------------------------------------------------------------- Besides the five main conferences the following satellite events are planned for ETAPS 2001 CMCS: Co-algebraic Methods in Computer Science Contact: Ugo Montanari (Universita' di Pisa, Italy) ETI Day: Electronic Tool Integration platform Day Contacts: Tiziana Margaria (Universitaet Dortmund, Germany) and Andreas Podelski (MPI Saarbrucken, Germany) JOSES: Java Optimization Strategies for Embedded Systems Contact: Uwe Assmann (Universitat Karlsruhe, Germany) LDTA: Workshop on Language Descriptions, Tools and Applications Contact: Mark van den Brand (CWI Amsterdam, The Netherlands) MMAABS: Models and Methods of Analysis for Agent Based Systems Contact: David Robertson (University of Edinburgh, UK) PFM: Proofs For Mobility Contact: Davide Sangiorgi (INRIA-Sophia Antipolis, France) RelMiS: Relational Methods in Software Contact: Wolfram Kahl (Universitaet der Bundeswehr Munchen, Germany) UNIGRA: Uniform Approaches to Graphical Process Specification Techniques Contact: Julia Padberg (Technische Universitaet Berlin, Germany) WADT: Workshop on Algebraic Development Techniques Contact: Maura Cerioli (DISI-Universita' di Genova, Italy) IMPORTANT DATES: ----------------------------------------------------------------------- October 20, 2000: Submissions Deadline for the Main Conferences, Demos and Tutorials December 15, 2000: Notification of Acceptance/Rejection January 15 2001: Camera-ready Version Due April 2-6, 2001: ETAPS 2001 in Genova March 31 - April 8, 2001: Satellite Events ----------------------------------------------------------------------- [ Sorry for multiple copies. Do not reply to this message. If you believe we have sent this to a list not appropriate, please let us know by mailing to etaps2001@disi.unige.it ] From rrosebru@mta.ca Fri Oct 20 09:04:14 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9KBKic25647 for categories-list; Fri, 20 Oct 2000 08:20:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Reply-To: From: "Michael Mislove" To: "Categories" Subject: categories: MFPS XVII Date: Thu, 19 Oct 2000 09:30:54 -0500 Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 18 Dear Colleagues, Below is the first Announcement and Call for Papers for next spring's conference on the Mathematical Foundations of Programming Semantics. As the announcement indicates, MFPS 17 will take place at Aarhus University in Aarhus, Denmark from May 24 to May 27, 2001. We encourage submissions in areas traditionally represented at MFPS, and in related areas as well. The deadline for submissions is January 5, 2001. Please pass this announcement on to those whom you think would have an interest in participating. An announcement providing registration details and more information about the program will be forthcoming around February 15, 2001, when the list of accepted papers will be posted. General information about MFPS can be found at http://www.math.tulane.edu/mfps.html and information about MFPS 17 at http://www.math.tulane.edu/mfps17.html If you have any questions about the meeting, you can send email to mfps@math.tulane.edu. Best regards, Mike Mislove ====================================================================== Announcement and Call for Papers MFPS XVII Seventeenth Conference on the Mathematical Foundations of Programming Semantics Aarhus University Aarhus, Denmark May 24 - May 27, 2001 Partially Supported by BRICS and the US Office of Naval Research The Seventeenth Conference on the Mathematical Foundations of Programming Semantics will take place on the campus of Aarhus University in Aarhus, Denmark from May 24 to May 27, 2001. The MFPS conferences are devoted to those areas of mathematics, logic and computer science which are related to the semantics of programming languages. The series particularly has stressed providing a forum where both mathematicians and computer scientists can meet and exchange ideas about problems of common interest. We also encourage participation by researchers in neighboring areas, since we strive to maintain breadth in the scope of the series. The invited speakers for MFPS 17 include: Olivier Danvy (Aarhus) Neil Jones (DIKU) Kim Larsen (Aalborg) Prakash Panangaden (McGill) Jan Rutten (CWI) Glynn Winskel (Cambridge) In addition to the invited talks, there will be three special sessions. The first will honor Neil Jones for his contributions to theoretical computer science; it is being organized by Olivier Danvy and David Schmidt (Kansas State). The second will be a special session on model-checking, and it is being organized by Rance Cleaveland (Stony Brook) and Kim Larsen. The final special session will be on security, and it is being organized by Catherine Meadows (NRL). The remainder of the program will consist of papers selected from submissions we receive in response to this Call for Papers. The Organizing Committee for MFPS consists of Stephen Brookes (CMU), Michael Main (Colorado), Austin Melton (Kent State University), Michael Mislove (Tulane) and David Schmidt (Kansas State). The Co-chairs for MFPS XVII are Olivier Danvy, Michael Mislove and David Schmidt. The Program Committee Co-chairs for the meeting are Stephen Brookes and Michael Mislove. The Program Committee also includes: Lars Birkedal (ITU) Rance Cleaveland (Stony Brook) Marcelo Fiore (Sussex) Matthew Hennessy (Sussex) Alan Jeffrey (DePaul) Achim Jung (Birmingham) Gavin Lowe (Oxford) Catherine Meadows (NRL) Peter O'Hearn (Queen Mary and Westfield) Susan Older (Syracuse) Dusko Pavlovic (Kestrel Institute) Uday Reddy (Birmingham) Giuseppe Rosolini (Genoa) Davide Sangiorgi (Inria - Sophia Antipolis) Andre Scedrov (Penn) Submissions must be extended abstracts of 12 pages or less. They should be in the form either of a PostScript file that can print on any PostScript printer, or a pdf file. In particular, submissions should use the US letter size format, as opposed to the European A4 size. Submissions can be sent by email to mfps@math.tulane.edu The Deadline for Submissions is January 5, 2001 Information about decisions will be available by February 15, 2001, at which time a list of accepted papers will be posted. As with MFPS XI, MFPS XIII and MFPS XV, the Proceedings of the conference will be published as a volume of the Electronic Notes in Theoretical Computer Science. For information about this series, access the URL http://www.elsevier.nl/locate/entcs. General inquiries about MFPS XVII can be addressed to mfps@math.tulane.edu. In addition to supporting the conference overall, the support provided by the Office of Naval Research makes funds available to help offset expenses of graduate students. Women and minorities also are encouraged to inquire about possible support to attend the meeting. Registration Information Detailed information about registration and accommodations will be available on February 15, 2001, when the list of papers accepted for the meeting is posted. From rrosebru@mta.ca Fri Oct 20 11:13:08 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9KDbnU25656 for categories-list; Fri, 20 Oct 2000 10:37:49 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Sent: 20 Oct 2000 12:54:08 GMT Message-ID: <003301c03a95$49f73610$448a0dd8@main> Reply-To: "Al Vilcius" From: "Al Vilcius" To: "Categories@Mta. Ca" Subject: categories: coinduction Date: Fri, 20 Oct 2000 08:57:20 -0400 Organization: Al Vilcius & Associates MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 19 can anyone explain coinduction? in what sense it dual to induction? does it relate to the basic picture for a NNO? is there a (meaningful) concept of co-recursion? what would be the appropriate internal language? how is it used to prove theorems? Al Vilcius al.r@vilcius.com From rrosebru@mta.ca Fri Oct 20 18:38:35 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9KL70n12832 for categories-list; Fri, 20 Oct 2000 18:07:00 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 20 Oct 2000 17:35:17 +0200 (MET DST) Message-Id: <200010201535.RAA07760@ithif20.inf.tu-dresden.de> From: Hendrik Tews MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: Subject: categories: Re: coinduction In-Reply-To: <003301c03a95$49f73610$448a0dd8@main> References: <003301c03a95$49f73610$448a0dd8@main> X-Mailer: VM 6.34 under Emacs 19.34.1 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 20 Hi, Al Vilcius writes: From: "Al Vilcius" Date: Fri, 20 Oct 2000 08:57:20 -0400 Subject: categories: coinduction can anyone explain coinduction? Have a look at Bart Jacobs and Jan Rutten A Tutorial on (Co)Algebras and (Co)Induction Bulletin of the EATCS, Vol. 62, pp. 222-259, 1996. it is available on the authors homepages, for instance http://www.cs.kun.nl/~bart/PAPERS/JR.ps.Z Bye, Hendrik From rrosebru@mta.ca Sun Oct 22 17:55:27 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9MKJbn12149 for categories-list; Sun, 22 Oct 2000 17:19:37 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.20001020180219.012fa110@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Fri, 20 Oct 2000 18:19:57 -0700 To: categories@mta.ca From: Charles Wells Subject: categories: Re: coinduction In-Reply-To: <003301c03a95$49f73610$448a0dd8@main> 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: 21 In brief: If a structure has no nontrivial substructures, you can prove a property P is true of everything in the structure by proving that the elements with property P form a nonempty substructure. Take the structure to be N with the unary operation of successor and you get induction. Now say that in the opposite category: If a structure has no nontrivial congruences, you can prove that two objects are equal if they are equivalent under any congruence. (You can define "definition by coinduction" by a similar dualization.) This has found many applications in computer science (where the congruence is bisimulation). See J.J.M.M. Rutten, Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1), 2000, pp. 3-80 and other papers by him on his website: http://www.cwi.nl/~janr/papers/ --Charles Wells >can anyone explain coinduction? >in what sense it dual to induction? >does it relate to the basic picture for a NNO? >is there a (meaningful) concept of co-recursion? >what would be the appropriate internal language? >how is it used to prove theorems? > >Al Vilcius >al.r@vilcius.com > > > Charles Wells, 105 South Cedar St., Oberlin, Ohio 44074, 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 NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm From rrosebru@mta.ca Sun Oct 22 17:55:27 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9MKIKE19544 for categories-list; Sun, 22 Oct 2000 17:18:20 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: phiwumbda.dyndns.org: jesse set sender to jesse@andrew.cmu.edu using -f To: "Categories@Mta. Ca" Subject: categories: Re: coinduction References: <003301c03a95$49f73610$448a0dd8@main> Mail-Copies-To: poster Content-Type: text/plain; charset=US-ASCII From: jesse@andrew.cmu.edu (Jesse F. Hughes) Date: 20 Oct 2000 18:01:59 -0400 In-Reply-To: "Al Vilcius"'s message of "Fri, 20 Oct 2000 08:57:20 -0400" Message-ID: <87og0fnpd4.fsf@phiwumbda.dyndns.org> Lines: 67 User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.1 (Carlsbad Caverns) MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 22 "Al Vilcius" writes: > can anyone explain coinduction? > in what sense it dual to induction? > does it relate to the basic picture for a NNO? > is there a (meaningful) concept of co-recursion? > what would be the appropriate internal language? > how is it used to prove theorems? The principle of induction says that initial algebras have no non-trivial subalgebras. Consider N, the initial successor algebra. A subobject S of N is a subalgebra just in case there is a structure map s: S+1 -> S such that the inclusion S -> N is a homomorphism. This is just the usual condition that 0 is in S and if n is in S, then so is its successor. Induction says that any such subalgebra exhausts the set N. Coinduction says, dually, that the final coalgebra has no non-trivial quotients. (To see that this is "really" a dual principle, we would interpret "subalgebra" above as a regular subobject in the category of algebras.) However, the principle is usually stated in terms of relations on a coalgebra, rather than quotients. In these terms, the principle of coinduction says: Any relation on in the category of coalgebras is a subrelation of equality. Note: I stated the principles of induction/coinduction above for the initial algebra/final coalgebra, resp. However, just as induction holds for any quotient of the initial algebra, coinduction holds for any (regular) subcoalgebra of the final coalgebra. I'm not sure what you're looking for in relation to NNOs. An NNO is the same as an initial algebra for the successor functor (assuming that our category has coproducts). The structure map N + 1 -> N is given by [s,0], where s is the successor. The final coalgebra for successor is easily described (say, in Set): It is the NNO with a point adjoined for "infinity". The structure map pred:F -> F + 1 fixes infinity, takes n+1 to n and takes 0 to * (the element in 1 -- a kind of "error condition"). As far as co-recursion goes, yes, there is a meaningful principle. Namely, given any coalgebra , there is a unique coalgebra homomorphism from to . Thus, for any set S together with a function t:S -> S+1, there is a unique map h:S -> N u {infinity} such that (1) if t(s) = *, then h(s) = 0 (2) else, h(t(s)) = h(s) - 1 (where infinity - 1 = infinity) In other words, h here takes an element s to the least n such that t^n(s) = *, if defined. If, for all n, t^n(s) != *, then h(s) = infinity. I'll defer on the question of what the appropriate internal language is. As far as how coinduction is used to prove theorems: To show two elements of the final coalgebra are equal, it suffices to find a coalgebraic relation relating the elements. Hendrik's suggestion (that you find Jacobs and Rutten's paper) is a good one, but I hope these comments help until then. -- Jesse Hughes "Such behaviour is exclusively confined to functions invented by mathematicians for the sake of causing trouble." -Albert Eagle's _A_Practical_Treatise_on_Fourier's_Theorem_ From rrosebru@mta.ca Mon Oct 23 15:06:08 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9NHD1F31459 for categories-list; Mon, 23 Oct 2000 14:13:01 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 23 Oct 2000 14:00:45 -0300 (ADT) From: Bob Rosebrugh To: categories Subject: categories: new electronic journal: AGT 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: 23 [Note from moderator: while it was not submitted directly to categories, the following announcement will be of interest to many members of the list. The LaTeX/ps is deleted for this mailing, but can be forwarded on request to me.] Date: Sat, 7 Oct 2000 18:28:54 +0100 (BST) Dear GT and AGT Subscribers The attached letter is being widely mailed to topologists. It announces the launching of a new journal (Algebraic and Geometric Topology) published by Geometry and Topology Publications. Please help to publicise this journal by circulating the letter as widely as possible. The letter is given as a text file, as a LaTeX file and as a PostScript file: ****** text file ***** Fellow Topologists: This letter announces the launching of a new international journal, "Algebraic & Geometric Topology" (AGT). It is intended that this new journal cover all of topology, broadly defined. Papers will be fully refereed, in the traditional manner and using standards which are well-known in our field. Immediately after they are accepted for publication, they will be published electronically. At the end of each calendar year, that year's papers will be published in a paper volume, which will be sold to the libraries at cost. AGT is an ``independent journal", i.e. a journal established by and run by mathematicians, with the cooperation of commercial publishers who will handle the printing and distribution of the paper version. The range of interests of AGT is defined by its Editorial Board. It has two Editors-in-Chief, Bob Oliver for Algebraic Topology and Marty Scharlemann for Geometric Topology. The other members of the Editorial Board are Selman Akbulut, Joan Birman, Ruth Charney, Fred Cohen, Alexander Dranishnikov, John Etnyre, Mario Eudave-Mu\~noz, David Fried, John Greenlees, Ian Hambleton, Hans-Werner Henn, Kathryn Hess, Stefan Jackowski, Akio Kawauchi, Goro Nishida, Tomotada Ohtsuki, Fr\'ed\'eric Paulin, Andrew Ranicki, Justin Roberts, Michah Sageev, Peter Scott, Ulrike Tillmann, Vladimir Turaev, Shicheng Wang. The Managing Editors (in charge of publishing) are Colin Rourke and Brian Sanderson. Manuscripts may be submitted to any Editor, including the Editors-in-Chief (but not the Managing Editors). For details about the mathematical interests of the members of the Editorial Board and for instructions on the submission of manuscripts, visit our web site at http://www.maths.warwick.ac.uk/agt/ As most of you probably know, the underlying reason for independent journals is that most of the commercial journals specializing in topology have priced themselves beyond the reach of our libraries. AGT intends to compete directly for the stronger papers in Topology and Its Applications, K-Theory, Geometria Dedicata, Topology and The Journal of Knot Theory and its Ramifications. The 1999 prices for those journals range between $.45 and $.92/page, plus varying supplements (which are difficult to pin down because they depend upon complex arrangements) for the electronic version. On the other hand, we anticipate that AGT will cost about $.10/page for the printed version and zero for the electronic version. The issue of journal prices was the main reason for the founding of GTP, a non-profit making publication enterprise specializing in electronic publications. It is based in the Mathematics Department of the University of Warwick at Coventry, UK, and it will publish the electronic versions of Algebraic & Geometric Topology and its sister journal Geometry & Topology. This raises the immediate question: how is the new journal Algebraic & Geometric Topology} related to the existing journal Geometry & Topology? They are distinct competing journals owned by the same parent organization, just as {\it Springer-Verlag} publishes competing graduate textbooks in topology. Each has its own editorial board. The mathematical interests and tastes of the board members naturally shape the journal. These interests have some overlap, and many areas of non-overlap. Algebraic & Geometric Topology aims to be more inclusive than Geometry & Topology, and it intends to concentrate more specifically on topology. It will set its own standards as it evolves, with those standards determined in part by the competing journals which we named explicitly above. For many years topologists have had a choice of commercial journals. Now they will also have a choice among independent journals. Endorsement by SPARC (the Scholarly Publishing and Academic Resources Coalition) has been requested and is pending. If we receive it, we anticipate that subscriptions to the paper version will come in from a broad selection of research libraries. Negotiations with publishers for printing the paper version are underway. We anticipate that they will be completed well before we have enough papers for our first volume. Archiving will be handled through the arXiv (at either arXiv.org or xxx.lanl.gov), a free service which appears to us to be sound and reliable. Note that we use the arXiv solely as an extra layer of security (in case for some unknown reason the files stored electronically at Warwick University are lost). The papers which are stored in the arXiv will carry the AGT logo and will say, very clearly, ``Published in Algebraic & Geometric Topology". They therefore cannot be confused with preprints. We solicit your submissions, and your assistance in encouraging your library to provide convenient browsing access to AGT. We hope that you will find this new journal as exciting as we do, and will express that feeling by sending us your papers, contributing your expertise as a referee when we call on you, and by telling your students and colleagues about AGT. Sincerely, Bob Oliver, Marty Scharlemann (for the Editorial Board of AGT) and Joan Birman, John Jones, Rob Kirby, Haynes Miller, Colin Rourke, Brian Sanderson (Executive Committee of GTP) From rrosebru@mta.ca Fri Oct 27 14:47:45 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9RH4NT26134 for categories-list; Fri, 27 Oct 2000 14:04:23 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39F8C2F8.3AF5D614@kestrel.edu> Date: Thu, 26 Oct 2000 16:49:12 -0700 From: Dusko Pavlovic X-Mailer: Mozilla 4.5 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: "Categories@Mta. Ca" Subject: categories: Re: coinduction References: <003301c03a95$49f73610$448a0dd8@main> 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: 24 Al Vilcius asks: > > can anyone explain coinduction? > > in what sense it dual to induction? and most people reply along the lines of: > The principle of induction says that initial algebras have no > non-trivial subalgebras. > Coinduction says, dually, that the final coalgebra has no non-trivial > quotients. but wouldn't it be nice to keep the standard definition of induction, which says that the equations f(0) = c f(n+1) = g(f(n)) determine a unique f, given c and g? this is the definition that most first year students study, and many programmers use every day, usually without the slightest idea about subalgebras, or triviality. do we really gain anything by replacing this simple scheme by the higher-order statement about all subalgebras? ok, we do get the appearance of symmetry between induction and coinduction. but is the higher-order statement about quotients really the friendliest form of coinduction, suitable to be taken as the definition? i think barwise and moss somewhere describe coinduction as *induction without the base case*. the coinduction principle says that the equation X = a.X + bc.X determines a unique CCS-process, or a unique {a,b,c}-labelled hyperset. it also guarantees that the integral equation E(x) = 1 + \int_0^x E dt has a unique solution. (note that this is equivalent to the differential equation E(0) = 1 E = E' where the initial condition gives the base case for the power series solution. so the no-base-case slogan is just a matter of form? but note that E' = E, and more generally E' = h(E), for an analytic h, identifies two *infinite* streams, and is not a mere inductive step up the stream.) in any case, i contend that the practice of coinduction primarily consists of solving *guarded equations*, like the two above --- surely if you count the areas where people extensively use coinduction, without calling it by name, viz math analysis. ((it is true that computer scientists became aware of coinduction while working out the bisimulations etc, which is why the quotients came in light. but now it seems that the bisimulations were just the way to construct final coalgebras; whereas the coinduction, in analogy with the induction, should be a practically useful logical principle, available over the *given* final coalgebras.)) anyway, the heart of the matter probably lies in peter aczel's insight that the statement * V ---> PV is a final coalgebra for P = (finite) powerset functor equivalently means that * every accessible pointed graph has a unique decoration in V. presenting the graph definitions as systems of guarded equations (like in barwise and moss' book "vicious circles"), the above equivalence generalizes to the statement that * V --d--> FV is a final coalgebra for F iff * every system of guarded equations over V has a unique solution. where the notion of guarded is determined by F and d. this is, of course, just barwise and moss' solution lemma, lifted to F. or more succinctly : **V is a final fixpoint iff each guarded operation g:V-->V has a unique fixpoint** this, of course, supports the view that ***coinduction is solving guarded equations***... i was hoping to say more, but will have to leave it for later, and post this hoping to motivate discussion. unguardedly yours, -- dusko pavlovic PS i have a great appreciation for jan rutten's work on coinduction, but it seems to me that the title of *universal coalgebra* is a bit exaggerated. universal algebra does not dualize. by design, it is meant to be model theory of algebraic theories. what would be the "coalgebraic theories", leading to coalgebras as their models? what would their functorial semantics look like? (implicitly, these questions are already in manes' book.) and then, moving from coalgebraic theories to comonads, like from algebraic theories to monads, should presumably yield an HSP-like characterization for the categories of (comonad) coalgebras. but coalgebras for a comonad over a topos usually form just another topos. i may be missing something essential here, but then i do stand to be corrected. From rrosebru@mta.ca Fri Oct 27 21:08:17 2000 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9RNBvC11299 for categories-list; Fri, 27 Oct 2000 20:11:57 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: phiwumbda.dyndns.org: jesse set sender to jesse@andrew.cmu.edu using -f To: "Categories@Mta. Ca" Subject: categories: Re: coinduction Content-Type: text/plain; charset=US-ASCII From: jesse@andrew.cmu.edu (Jesse F. Hughes) Date: 27 Oct 2000 16:40:57 -0400 In-Reply-To: Dusko Pavlovic's message of "Thu, 26 Oct 2000 16:49:12 -0700" Message-ID: <87itqexbja.fsf@phiwumbda.dyndns.org> Lines: 110 User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.1 (Carlsbad Caverns) MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 25 I'm afraid that I've never quite understood the notion of guarded equations, so I cannot comment on much of what you wrote below without some more time and more thought. Let me make a few introductory comments and perhaps I can say more later. Dusko Pavlovic writes: > Al Vilcius asks: > > > > can anyone explain coinduction? > > > in what sense it dual to induction? > > and most people reply along the lines of: > > > The principle of induction says that initial algebras have no > > non-trivial subalgebras. > > > Coinduction says, dually, that the final coalgebra has no > non-trivial > > quotients. > > but wouldn't it be nice to keep the standard definition of > induction, which says that the equations > > f(0) = c > f(n+1) = g(f(n)) > > determine a unique f, given c and g? this is the definition that > most first year students study, and many programmers use every > day, usually without the slightest idea about subalgebras, or > triviality. do we really gain anything by replacing this simple > scheme by the higher-order statement about all subalgebras? ok, > we do get the appearance of symmetry between induction and > coinduction. but is the higher-order statement about quotients > really the friendliest form of coinduction, suitable to be taken > as the definition? I have always considered the statement regarding existence of a unique function f to be the principle of recursion. The principle of induction is, in my mind, the weaker principle that says that if a property holds of 0 and is closed under successor, then it holds of N. I identify "properties" with subobjects here. In terms of homomorphisms, this is equivalent to the "uniqueness part" of initiality (assuming that our category has some epi-mono factorization property, I suppose). One may question whether it's appropriate to take the principle of induction to apply to all properties or only those properties which are definable in some sense -- I guess you've done as much when you refer to the "higher-order statement" above. I'm not sure to what extent my use of all subalgebras differs from your quantification over all g and c in the statement of recursion above, however. When we separate the properties of induction and recursion in the way I mention above, by the way, then (conceptually) induction is a property of those algebras A in which each element is picked out by a (not necessarily unique) term of our language. I.e., those A for which there is an epi from the initial algebra to A. Hence, induction in my sense is weaker than recursion (induction in your sense). Regarding whether a statement about quotients is really the "friendliest form" of coinduction, I'll have to agree that it is not, if one's aim is to describe coinduction as it is commonly used. I chose to describe it in the terms above because these terms make clear the "co" in "coinduction". I did gloss over details that ensure the equivalence of the "familiar principle" of coinduction and the principle regarding quotients. If the base category has kernel pairs of coequalizers and G preserves weak pullbacks, then a G-coalgebra A has no non-trivial quotients iff the equality relation is the largest coalgebraic relation on A (I hope I've got that right). Inasmuch as the principle I called coinduction is not always equivalent to the familiar principle, I was being a bit misleading. However, I think it is the right approach if one's goal is to explain the relationship between induction and coinduction. I'm not sure that the principle regarding the equality relation is what you'd call coinduction, however. I think that the principle you have in mind is what I'd call "corecursion". Analogous to the distinction between recursion and induction, I omit the existence part of finality in what I call "coinduction" and I use the uniqueness part. > > and then, moving from coalgebraic theories to comonads, like > from algebraic theories to monads, should presumably yield an > HSP-like characterization for the categories of (comonad) > coalgebras. but coalgebras for a comonad over a topos usually > form just another topos. > But, there *are* such characterizations of categories of coalgebras, if I understand your point. Namely, a full subcategory of coalgebras is closed under coproducts, codomains of epis and domains of regular monos iff it is the class of coalgebras satisfying a "coequation" -- given, here, some boundedness conditions on the functor so that things work out well. For brevity's sake, and because you're likely familiar with this result, I'll omit details on what a coequation is and how it's satisfied. By the way, about that last statement regarding coalgebras "usually" forming a topos: Doesn't one need that the endofunctor preserve pullbacks, or am I missing something? -- Jesse Hughes "The only "intuitive" interface is the nipple. After that, it's all learned." -Bruce Ediger on X interfaces "Nipples are intuitive, my ass!" -Quincy Prescott Hughes From rrosebru@mta.ca Sat Oct 28 17:38:48 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9SKAHF08131 for categories-list; Sat, 28 Oct 2000 17:10:17 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <000901c04116$db094e40$c2036882@ucl.ac.be> From: "Mamuka Jibladze" To: Subject: categories: Re: coinduction Date: Sat, 28 Oct 2000 21:39:57 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 5.00.2919.6600 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 26 Hi all, although I cannot say much on coinduction itself, I would like to mention one possible point of view on "universal coalgebra" commented on by Dusko at the end of his message: > PS i have a great appreciation for jan rutten's work on > coinduction, but it seems to me that the title of *universal > coalgebra* is a bit exaggerated. universal algebra does not > dualize. by design, it is meant to be model theory of algebraic > theories. what would be the "coalgebraic theories", leading to > coalgebras as their models? what would their functorial > semantics look like? (implicitly, these questions are already > in manes' book.) > > and then, moving from coalgebraic theories to comonads, like > from algebraic theories to monads, should presumably yield an > HSP-like characterization for the categories of (comonad) > coalgebras. but coalgebras for a comonad over a topos usually > form just another topos. > > i may be missing something essential here, but then i do stand > to be corrected. I would say that, although there is no straightforward dualization, there might be a "hidden" one. In my opinion, comonads can sometimes play the role of "strengtheners" or "enrichers" for monads, so that while monads can be viewed as a "substrate for structure", comonads are "substrate for semantics". Rather than trying to give sense to this vague phrase, let me give three illustrations. -1- S. Kobayashi, Monad as modality. Theoret. Comput. Sci. 175 (1997), no. 1, 29--74. The starting point in that paper is the monad semantics by Moggi. It seems that for computer-scientific purposes strength of the monad is too restrictive a requirement, and the author modifies the semantics by assuming strength of the monad *only*with* respect*to*a*comonad*. This means that the monad and comonad distribute in such a way that the monad descends to a strong monad on the category of coalgebras over the comonad. Under the Curry-Howard correspondence this yields an interesting intuitionistic version of the modal system S4. A realizability interpretation is also given. -2- Freyd, Yetter, Lawvere, Kock, Reyes and others have studied "atoms", or infinitesimal objects - objects I in a cartesian closed category with the property that the exponentiation functor I->(_) has a right adjoint. This induces a monad, which cannot be strong in a nontrivial way, just as in the previous example. There is a "largest possible" subcategory over which it is strong, namely the category of I-discrete objects, i.e. those objects X for which the adjunction unit from X to I->X is iso. In good cases the inclusion of this subcategory is comonadic. As Bill pointed out, one might view Cantor's idea of set theory as a case of this: the universe of sets is the largest - necessarily "discrete" - part of "analysis" over which the latter can be "enriched" (well, this is awfully inaccurate, sorry -- consider it as a metaphor). -3- In differential homotopical algebra, there was developed a notion of torsor (principal homogeneous object) which works in a non-cartesian monoidal category. This notion requires not just a (right) action of a monoid M on an object P, but also a "cartesianizer" in form of a left coaction of a comonoid C on P which commutes with the action, and is principal in an appropriate sense. It turns out that the monoid and the comonoid enter in an entirely symmetric way. In the monoidal category of differential graded modules over a commutative ring, principal C-M-objects are classified by s.c. twisting cochains from C to M. Moreover in that category, for a monoid M there is a universal choice of P and C given by the Eilenberg-Mac Lane bar construction, and for a comonoid C there is a universal choice of P and M, given by the Adams' cobar construction. I would be grateful for a reference to a version of these for general monads/comonads. Regards, Mamuka From rrosebru@mta.ca Sat Oct 28 17:39:07 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9SK4p703903 for categories-list; Sat, 28 Oct 2000 17:04:51 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200010280923.CAA10190@coraki.Stanford.EDU> To: "Categories@Mta. Ca" Subject: categories: Re: coinduction: definable equationally? In-Reply-To: Message from jesse@andrew.cmu.edu (Jesse F. Hughes) of "27 Oct 2000 16:40:57 EDT." <87itqexbja.fsf@phiwumbda.dyndns.org> Date: Sat, 28 Oct 2000 02:23:02 -0700 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 27 1. Is there a variety embedding coinduction? Jesse Hughes distinguishes induction from recursion in terms of natural numbers. For him induction is Peano's mathematical induction, while recursion is the uniqueness of the map from the (unique up to a unique isomorphism) initial algebra to an arbitrary algebra. To me induction is on the one hand a slightly more general notion, yet on the other sufficiently tractable that it can be axiomatized equationally when suitably expressed, as I'll now describe. In particular there exists a variety embedding induction, meaning one in which an induction principle holds. Whether the additional generality makes induction equal to recursion is another story. The context in which all this arose, namely answers to Al Vilcius' question about coinduction, naturally prompts the question, is there a variety embedding coinduction, to which I'll return at the end. 2. Nature of Induction Suppose, somewhere out there in the universe, a world exists where kicking a nonworking TV set always leaves it in its nonworking state. Then in that world (certainly not ours), it is surely the case that repeated kicking can do no better. The general principle here is that if performing a certain action on a system cannot under any circumstance destroy a certain property of that system, then neither can _repeatedly_ performing that action on that system. I submit that this is the essence of induction, of which mathematical induction is just an instance. This principle may be expressed more logically as PQ |- P ------- (IND) PQ* |- P The premise is that Q preserves P. That is, if first P and then afterwards Q, it follows that P. The conclusion is that Q* preserves P. That is, if first P and then afterwards Q repeatedly, it follows that P. Here we understand Q* as the reflexive transitive closure of Q, in the spirit of Kleene's regular expressions, which we take to denote the performance of Q zero or more times. By itself (IND) serves only to bound Q* from above, which would allow us to satisfy (IND) with Q* = 0 for all Q. We may bound Q* from below by adding that Q* is a closure of Q, namely Q <= Q*, and is transitive --- Q*Q* <= Q* --- and reflexive --- 1 <= Q*. These additional conditions make Q* the least reflexive transitive element greater or equal to Q (proved below), thereby uniquely determining it. 3. Equational Expression of Induction The earliest description to my knowledge of a finitely based variety embedding an induction principle is Tarski and Ng's RAT [1] (1977). (The second is DALG, dynamic algebras, which I described two years later [2] (1979), independently of [1], which I did not learn about until 1989.) The following, based on [3] (1990), generalizes the Boolean setting for RAT to residuated semirings. Others who have worked on finitely based varieties embedding induction include Kozen, Bloom, and Esik, to name just a few. Take as the ambient variety that of semirings with unit. The signature is 2-2-0-0, notated (X, ., +, 0, 1). The equations are: 1. (X,+,0) is a semilattice with unit: + is associative (1), commutative (2), and idempotent (3), with identity 0 (4). 2. (X,.,1) is a monoid: . is associative (5), with identity 1 (6,7). 3. Distributivity: x.(y+z) = x.y + x.y (8) (x+y).z = x.z + y.z (9) (Distributivity could be weakened to monotonicity for our purposes, but since (RR) and (LR) below force it anyway we may as well put it in here to justify calling this a semiring.) We make the following abbreviations. xy for x.y x <= y for x+y = y (inequations are expressible equationally) x |- y for x <= y (i.e. for x+y = y), to look more logical The induction principle IND may then be understood as being about such a semiring expanded with a unary operation *. Thus far the signature has constants 0 and 1, binary operations + and ., and a unary operation *, amounting to Kleene's language of regular expressions. The addition of two further binary operations, suitably axiomatized equationally, permits a purely equational expression of the foregoing. The desired language expansion adds right and left residuation, x\y and x/y (of which just the first suffices for our immediate purposes). PQ <= R iff Q <= P\R (right residuation) (RR) iff P <= R/Q (left residuation) (LR) These axioms, recognizable in this forum of course as making P\ and /P the polarities of a Galois connection or posetal adjunction, serve to define P\Q and Q/P uniquely in terms of the semiring operations. In particular they force P\Q (resp. Q/P) to be the greatest, i.e. weakest, element satisfying P(P\Q) <= Q (resp. (Q/P)P <= Q). If we interpret PQ logically as a noncommutative conjunction P _then_ Q, then P\Q, or P -> Q, may be understood logically as "if previously P, then R". Similarly Q/P, or Q <- P, becomes "Q provided eventually P". One way of looking at this is that we are furnishing the signature with internal conditionals in order to express the external conditionals in (IND), (RR), and (LR) purely equationally. (RR) and (LR) serve not merely to axiomatize residuation but to define it, in the sense that for any given semiring there exists at most one interpretation of right residuation satisfying (RR). Hence (RR) serves (a) to pick out those semirings having exactly one such interpretation, and (b) to enforce that interpretation. Similarly for (LR). The nonequational definition of residuation given by (RR) and (LR) has the following equipollent equational expression (exercise): P\(Q+R) = P\Q + P\R (10) P(P\Q) <= Q <= P\(PQ) (11) (P+Q)/R = P/R + Q/R (12) (Q/P)P <= Q <= (QP)/P (13) (Actually (10) and (12) are overkill, it suffices to state that P\Q and Q/P are monotone in Q, viz. P\Q <= P\(Q+R) and similarly for Q/P. Also left residuation along with (LR), (12), and (13) are redundant for the purposes of the present story.) Three more equations complete the promised variety. 1 + P*P* + P <= P* (14) P* <= (P+Q)* (15) (P\P)* <= P\P (16) (induction, equationally) [1] Equation (14) says that P* is a reflexive transitive element greater or equal to P. Equation (15) merely asserts the monotonicity of *. Equation (16) is the equational expression of induction. It is equivalent to P(P\P)* <= P (16') That is, the repeated action of P\P preserves P. The interest in P\P is first of all that it preserves P, i.e. P(P\P) <= P as an immediate consequence (by (RR)) of P\P <= P\P; and second that it is the weakest (greatest) preserver of P, since if PQ <= P then Q <= P\P (by (RR)). This makes (16') the instance of induction in which the preserver of P happens to be P\P. But since P\P is the _weakest_ preserver of P, we can now obtain the general (nonequational) induction principle, namely from PQ <= P infer PQ* <= P, from this specific equationally expressible instance of it, viz. PQ <= P Q <= P\P by (RR) Q* <= (P\P)* by (15) (monotonicity of *) PQ* <= P(P\P)* by (9) (additivity of P. implies its monotonicity) <= P by (16') That is, the induction principle (IND) holds in the variety axiomatized by (1)-(16). More than this however, the unary operation * is uniquely determined by (14)-(16) by virtue of P* being the least (hence unique) reflexive transitive element of the semiring greater or equal to P. To see this, consider any reflexive transitive X. By transitivity XX <= X so X <= X\X, whence X* <= (X\X)* <= X\X. Hence XX* <= X. Concatenating X* on the right of each side of 1 <= X yields X* <= XX* <= X. Now suppose P <= X. Then P* <= X* <= X, making P* the least reflexive transitive element >= P. The residuals are of course uniquely determined by (10)-(13). So any semiring can be expanded with residuation and star so as to satisfy (10)-(16) in at most one way. That is, those seven equations not only single out those semirings admitting such an expansion but serve to fully define pre- and post-implication as well as reflexive transitive closure, entirely in terms of the given semiring. Given the well-known difficulties of defining the natural numbers using Peano's mathematical induction, or by any other first order means, it is a pleasant change to see an ostensibly intractable operation such as P* pinned down exactly in this way, and even more pleasant that it is all done purely equationally. 4. Back to the question We may now reword the original question in the light of the foregoing. To what variety can one similarly associate suitable operations fully defined equationally so as to include an equationally expressed principal of coinduction? -- Vaughan Pratt [1] @Article( NT77, Author="Ng, K.C. and Tarski, A.", Title="Relation algebras with transitive closure, {A}bstract 742-02-09", Journal="Notices Amer. Math. Soc.", Volume=24, Pages="A29-A30", Year=1977) [2] @InProceedings( Pr79c, Author="Pratt, V.R.", Title="Models of program logics", BookTitle="20th Symposium on foundations of Computer Science", Address="San Juan", Month=Oct, Year=1979) [3] @InProceedings( Pr90b, Author="Pratt, V.R.", Title="Action Logic and Pure Induction", BookTitle="Logics in AI: European Workshop JELIA '90", Series=LNCS, Volume=478, Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120", Address="Amsterdam, NL", Month=Sep, Year=1990) From rrosebru@mta.ca Sun Oct 29 20:04:16 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9TNKwN24211 for categories-list; Sun, 29 Oct 2000 19:20:58 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: phiwumbda.dyndns.org: jesse set sender to jesse@andrew.cmu.edu using -f To: "Categories@Mta. Ca" Subject: categories: Re: coinduction: definable equationally? References: <200010280923.CAA10190@coraki.Stanford.EDU> Mail-Copies-To: poster Content-Type: text/plain; charset=US-ASCII From: jesse@andrew.cmu.edu (Jesse F. Hughes) Date: 28 Oct 2000 16:54:59 -0400 In-Reply-To: Vaughan Pratt's message of "Sat, 28 Oct 2000 02:23:02 -0700" Message-ID: <87bsw4wusc.fsf@phiwumbda.dyndns.org> Lines: 37 User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.1 (Carlsbad Caverns) MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 28 Vaughan Pratt writes: > 1. Is there a variety embedding coinduction? > > Jesse Hughes distinguishes induction from recursion in terms of natural > numbers. For him induction is Peano's mathematical induction, while > recursion is the uniqueness of the map from the (unique up to a unique > isomorphism) initial algebra to an arbitrary algebra. > This doesn't look like what I had in mind, exactly. Peano's mathematical induction was meant as an example of induction, not the whole meaning of induction. I stated induction in terms of natural numbers only to continue Dusko's example. I'm afraid that I was a bit vague in what exactly induction is in my previous post. I say that a G-algebra A satisfies the principle of induction just in case every mono G-homomorphism into A is an isomorphism. If our base category has equalizers, then A satisfies the principle of induction just in case, for every algebra B, there is at most one homomorphism A -> B. So induction is the uniqueness part of initiality. What's recursion, then? As far as I'm concerned, recursion is just initiality. I.e., an algebra A satisfies the principle of definition by recursion just in case it is the initial algebra. (Why not take recursion to be just the existence part? I haven't seen much use for just the existence part and it also doesn't fit well with conventional usage.) Clearly, on this view, the principle of recursion implies the principle of induction, but the converse is not the case. I hope that my idea of induction is a bit clearer. I really must learn to write more precisely. -- Jesse Hughes "Such behaviour is exclusively confined to functions invented by mathematicians for the sake of causing trouble." -Albert Eagle's _A Practical Treatise on Fourier's Theorem_ From rrosebru@mta.ca Mon Oct 30 14:21:11 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9UHaUD03947 for categories-list; Mon, 30 Oct 2000 13:36:30 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 30 Oct 2000 15:55:25 GMT Message-Id: <200010301555.PAA02925@loire.comlab> From: Jeremy Gibbons To: categories@mta.ca In-reply-to: <003301c03a95$49f73610$448a0dd8@main> (al.r@VILCIUS.com) Subject: categories: Re: coinduction References: <003301c03a95$49f73610$448a0dd8@main> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 29 > can anyone explain coinduction? > in what sense it dual to induction? We've heard some very erudite answers to these questions. I don't know the questioner's background, but here is a different answer, in case it helps. In the algebraic approach to functional programming, an initial datatype of a functor F is a datatype T and an operation in : F T -> T for which the equation in h h . in = f . F h has a unique solution for given f. We write "fold_F f" for that unique solution, so h = fold_F f <=> h . in = f . F h This is an inductive definition of fold, and the above equivalence (the "universal property for fold") encapsulates proof by structural induction. (For example, when F X = 1+X, then T is N, the naturals. The injection in : 1+N->N is the coproduct morphism [0,1+]. Folds on naturals are functions of the form fold_{1+} [z,s] 0 = z fold_{1+} [z,s] (1+n) = s (fold_{1+} [z,s] n) To prove that a predicate p holds for every natural n is equivalent to proving that the function p : N -> Bool is equal to the function alwaystrue : N -> Bool that always returns true. Now alwaystrue is a fold, alwaystrue = fold_{1+} [true,step] where step true = true Therefore, to prove that p holds for every natural, we can use the universal property: predicate p holds of every natural <=> p = alwaystrue <=> p = fold_{1+} [true,step] <=> p . [0,1+] = [true,step] . id+p <=> p(0) = true and p(1+n) = step(p(n)) <=> p(0) = true and (p(1+n) = true when p(n) = true) which is the usual principle of mathematical induction.) Dually, a final datatype of a functor F is a datatype T and an operation out : T -> F T for which the equation in h out . h = F h . f has a unique solution for given f. We write "unfold_F f" for that unique solution, so h = unfold_F f <=> out . h = F h . f This is a coinductive definition of unfold, and the above equivalence (the "universal property for unfold") encapsulates proof by structural coinduction. > how is it used to prove theorems? Exactly the same way. For example, the datatype Stream A of streams of A's is the final datatype of the functor taking X to A x X. An example of an unfold for this type is the function iterate, for which iterate f x = [ x, f x, f (f x), f (f (f x)), ... ] defined by iterate f = unfold_{A x} One might expect that iterate f . f = Stream f . iterate f and the proof of this fact is a straightforward application of the universal property of unfold (that is, a proof by coinduction). Jeremy -- Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html From rrosebru@mta.ca Mon Oct 30 14:23:33 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9UHmMR07543 for categories-list; Mon, 30 Oct 2000 13:48:22 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: laurie.rem.cmu.edu: andrej set sender to Andrej.Bauer@cs.cmu.edu using -f To: "Categories@Mta. Ca" Subject: categories: Re: coinduction: definable equationally? References: <200010280923.CAA10190@coraki.Stanford.EDU> <87bsw4wusc.fsf@phiwumbda.dyndns.org> Reply-To: Andrej.Bauer@CS.cmu.edu From: Andrej Bauer Date: 29 Oct 2000 19:32:19 -0500 In-Reply-To: jesse@andrew.cmu.edu's message of "28 Oct 2000 16:54:59 -0400" Message-ID: Lines: 81 User-Agent: Gnus/5.0803 (Gnus v5.8.3) XEmacs/20.4 (Emerald) 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: 30 I believe the original post asked what coalgebras might be good for. Dusko Pavlovic already talked about examples of coinduction in analysis. Let me mention two examples from constructive mathematics. They are both examples of final coalgebras for polynomial functors. A polynomial functor P_f with signature f: B --> A is a functor of the form P_f(X) = \sum_{a \in A} X^{f^{*} a} where \sum is a dependent sum, and f^{*} is the inverse image of f. For the purposes of this post you can think of a polynomial functor as one of the form P(X) = C_0 + C_1 x X^{N_1} + ... + C_k x X^{N_k} where C_0, ..., C_k and N_0, ..., N_k are (constant) objects. Suppose we are in a constructive setting (a variant of Martin-Lof type theory, effective topos, a PER model, ...) in which every polynomial functor has a final coalgebra. Example 1: In constructive mathematics _spreads_ and _fans_ play an important role. They are examples of final coalgebras. For example, a fan is a finitely branching tree (can be infinite!) in which the nodes are labeled with natural numbers. The space of all fans FAN satisfies the identity FAN = N + N x FAN + N x FAN^2 + N x FAN^3 + ... = sum_{k \in N} N x FAN^k it is the final coalgebra for the polynomial functor P(X) = \sum_{k \in N} N x FAN^k I find this presentation conceptually cleaner than the usual encoding of spreads as sets of Goedel codes of finite sequences of natural numbers (of course, this presentation requires a richer type theory). Also, this definition is easily adapted to fans and spreads labeled by elements of any set A (just replace N x FAN^k with A x FAN^k), and of any branching type. By the way, FAN is isomorphic to N^N, and N^N is the final coalgebra for the functor P(X) = N x X. Example 2: The initial algebra for P(X) = 1 + X is the set of natural numbers. The final coalgebra N^+ for this functor is best thought of as the one-point compactification of the natural numbers, as it consists of the natural numbers together with one extra point "at infinity". In classical set theory, this is no different from natural numbers, but in a constructive setting the point at infinity is not isolated. If one wants to prove anything interesting about N^+, just about the only way to do it is to use coinduction and corecursion. It's a good exercise. This is neat because we get a one-point compactification of N without any reference to topology. If we compute N^+ in PER(D), where D is some topological model of the untyped lambda calculus, such as P(omega) or the universal Scott domain, we get _precisely_ the one-point compactification of natural numbers. In the effective topos N^+ can be described as an equivalence relation on partial recursive functions, where two such functions are equivalent if, and only if, they terminate in the same number of steps (when applied to some fixed input) or they diverge. The divergent functions represent the point at infinity, and those terminating in exactly k steps represent the number k. Andrej From rrosebru@mta.ca Mon Oct 30 14:26:39 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9UHljU03310 for categories-list; Mon, 30 Oct 2000 13:47:45 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39FCED20.9EC15DBD@kestrel.edu> Date: Sun, 29 Oct 2000 19:38:08 -0800 From: Dusko Pavlovic X-Mailer: Mozilla 4.5 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: "Categories@Mta. Ca" Subject: categories: Re: coinduction References: <87itqexbja.fsf@phiwumbda.dyndns.org> 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: 31 > > but wouldn't it be nice to keep the standard definition of > > induction, which says that the equations > > > > f(0) = c > > f(n+1) = g(f(n)) > > > > determine a unique f, given c and g? this is the definition that most > first year > I have always considered the statement regarding existence of a unique > function f to be the principle of recursion. the recursion schema, as defined by godel in 1930, is a bit stronger: g is allowed to depend on n, not only on f(n). > The principle of > induction is, in my mind, the weaker principle that says that if a > property holds of 0 and is closed under successor, then it holds of N. in a topos, this principle is equivalent with the above schema. and the schema itself, of course, just means that [0,s] : 1+N --> N is initial: any algebra [c,g] : 1+X --> X induces a unique homomorphism f : N-->X. using the exponents, we do recursion. as i said last time, induction and recursion have been in heavy use for so long, that they really don't leave much space for redefining, even for the sake of symmetry with coinduction and corecursion. -- dusko From rrosebru@mta.ca Mon Oct 30 20:13:35 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9UNVqR30225 for categories-list; Mon, 30 Oct 2000 19:31:52 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: Preprint: The co-Birkhoff theorem Mail-Copies-To: poster Content-Type: text/plain; charset=US-ASCII From: jesse@andrew.cmu.edu (Jesse F. Hughes) Date: 30 Oct 2000 16:56:30 -0500 Message-ID: <8766ma8035.fsf@phiwumbda.dyndns.org> Lines: 26 User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.1 (Carlsbad Caverns) MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 32 This is to announce that a pre-print is available at http://www.contrib.andrew.cmu.edu/user/jesse/papers/CoBirkhoff.ps.gz. Dusko's recent post regarding coinduction raises a question that is answered in this paper. Namely, what is the dual to Birkhoff's HSP theorem? Title: The Coalgebraic Dual of Birkhoff's Variety Theorem Authors: Steve Awodey and Jesse Hughes Abstract: We prove an abstract dual of Birkhoff's variety theorem for categories $\E_\Gamma$ of coalgebras, given suitable assumptions on the underlying category $\E$ and suitable $\map\Gamma\E\E$. We also discuss covarieties closed under bisimulations and show that they are definable by a trivial kind of coequation -- namely, over one ``color''. We end with an example of a covariety which is \emph{not} closed under bisimulations. This research is part of the Logic of Types and Computation project (http://www.cs.cmu.edu/Groups/LTC/) at Carnegie Mellon University under the direction of Dana Scott. -- Jesse Hughes From rrosebru@mta.ca Mon Oct 30 20:13:46 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9UNZIq00795 for categories-list; Mon, 30 Oct 2000 19:35:18 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: "Categories@Mta. Ca" Subject: categories: Re: coinduction Mail-Copies-To: poster Content-Type: text/plain; charset=US-ASCII From: jesse@andrew.cmu.edu (Jesse F. Hughes) Date: 30 Oct 2000 18:09:53 -0500 In-Reply-To: Dusko Pavlovic's message of "Sun, 29 Oct 2000 19:38:08 -0800" Message-ID: <87wveqsz7i.fsf@phiwumbda.dyndns.org> Lines: 84 User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.1 (Carlsbad Caverns) MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 33 Dusko Pavlovic writes: > > > I have always considered the statement regarding existence of a > > unique function f to be the principle of recursion. > > the recursion schema, as defined by godel in 1930, is a bit > stronger: g is allowed to depend on n, not only on f(n). Yes, I overlooked that point. But, is that principle any stronger than the principle you called induction? I think it isn't, given products in our category. Let N be the initial successor algebra. Let c be in X and g:N x X -> X. To define a function f such that f(0) = c f(n+1) = g(n,f(n)), I just have to cook up the appropriate structure map for N x X. I think that + <0,c>: (N x X) + 1 -> N x X does it (p_1 is the projection map). Let : N -> N x X be the unique function guaranteed by initiality. One can show that f satisfies the equations above. (Along the way, one shows that k is the identity.) (To add other parameters, one needs exponentials. For instance, given h:A -> X g:A x N x X -> X to show that there is a unique f such that f(a,0) = h(a) f(a,n+1) = g(a,n,f(a,n)) requires a structure map for (X x N)^A, if I'm not mistaken.) This shows that Godel's principle of recursion is equivalent to the statement "N is an initial algebra". I.e., it is equivalent to the statement that there is a unique f such that f(0) = c f(n+1) = g(f(n)). > > The principle of > > induction is, in my mind, the weaker principle that says that if a > > property holds of 0 and is closed under successor, then it holds of N. > > in a topos, this principle is equivalent with the above schema. and > the schema itself, of course, just means that [0,s] : 1+N --> N is > initial: any algebra [c,g] : 1+X --> X induces a unique homomorphism > f : N-->X. using the exponents, we do recursion. I am confused by this statement. My principle of induction for successor algebras [0_X,s_X]:1+X -> X is this: For all subsets P of X, if 0_X is in P and P is closed under s_X, then P = X. (Categorically, an algebra satisfies the principle of induction if it contains no proper subalgebras.) Consider the successor algebra X={x}, with the evident structure map [0_X,s_X]:1+X -> X. Surely, for every subset P of X, if 0_X is in P and P is closed under s_X, then P = X. In other words, the algebra X satisfies the principle of induction in the sense that I gave. This seems to contradict the equivalence you mention. What am I overlooking? > as i said last time, induction and recursion have been in heavy use > for so long, that they really don't leave much space for redefining, > even for the sake of symmetry with coinduction and corecursion. I quite agree, but I didn't redefine induction, as far as I am concerned. I learned that induction was the proof principle as I stated it and that recursion is the principle regarding the definition of functions many years ago. I think that our disagreement in definitions is a disagreement that one will find elsewhere in the literature. I also suppose that the term coinduction (as I use it) arose from the definition of induction that I offered. Are others unfamiliar with the distinction between induction and recursion as I drew it? I assumed it was a more or less conventional distinction. If my use is really idiosyncratic, then I'd be happy to drop it. -- Jesse Hughes "Such behaviour is exclusively confined to functions invented by mathematicians for the sake of causing trouble." -Albert Eagle's _A Practical Treatise on Fourier's Theorem_ From rrosebru@mta.ca Wed Nov 1 09:00:34 2000 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id eA1CF4Y12480 for categories-list; Wed, 1 Nov 2000 08:15:04 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39FF8058.2F30557@kestrel.edu> Date: Tue, 31 Oct 2000 18:30:48 -0800 From: Dusko Pavlovic X-Mailer: Mozilla 4.5 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: CATEGORIES mailing list Subject: categories: on algebra of coreals 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: 34 hi. almost a year after peter freyd posted his version of the coalgebra of real numbers (henceforth coreals), i finally tried to cash in on my initial excitement with it, and spec out the coinductive programs for addition and multiplication. however, i must report that i am a bit stuck. since i am also guilty of not having tried to work this out in time, i'll try to refresh things (at least for myself) by reporting in some detail. the reason why i was excited, as i think i explained at the time, was that peter seemed to be able to define the algebraic operations on his coreals by a relatively simple *stream* coinduction. for the coreals vaughan pratt and i had previously constructed, i only knew how to do this using the *conway games*, ie cuts, which appeared to be the most inefficient way imaginable. let me clarify the context a little, and why any of this matters. first of all, why another presentation of reals, when there are already so many deep and beautiful presentations, left behind the centuries of analysis? well, in spite of all that math, the CS students still learn that real numbers must be truncated, because they are infinite, whereas the computers are finite. as if computers are more finite than our heads, or smaller than our calculus textbooks. so the task is to find a presentation of the "real reals" suitable for computers. and the hypothesis is that coinduction allows such presentations. and indeed, we have several different coinductive implementations of the datatype of reals, and it has also been shown that a lot of what people do in differential calculus yields to coinduction. but the problem is that coalgebraically implemented reals offer some resistance to algebra: adding and multiplying computable reals may not be computable. if each real number is represented irredundantly, say by a unique stream of digits, then there will be numbers for which the entire infinite streams of digits will need to be consumed before the first digit of their sum, or product, can be determined. this observation is due to brouwer, and has been mentioned in this thread several times, in one form or another. in any case, in order to implement coreal algebra, besides a real coalgebra R, we also need a *redundant numeration system*, a surjection D^N --->> R mapping to each number the streams of D-digits representing it (plus some structure saying this). the coalgebras vaughan and i had constructed represent each number by a unique stream, and didn't seem to have good numeration systems. (now i think at least two of them have decent *generalized* numerations --- later more.) in contrast, peter's coalgebra represented reals as equivalence classes of streams, and thus came equipped with natural numerations! true, they were never mentioned explicitly, probably because XvX was viewed as a subobject of XxX, in order to allow splitting X--->XvX as a pair . but viewing XvX as the quotient of X+X = 2xX displays the final coalgebra I of XvX as the quotient of the final coalgebra 2^N of 2xX. hence the numeration 2^N --->> I corresponding to the standard binary expansion. of course, this system is not fully redundant (i think andrej bauer pointed this out), but the transition to the signed binary expansion 3^N --->> I where 3 = {-1,0,1}, is almost as well known... (ok, i only learned of it from martin escardo's thesis, but the real aritmeticists surely know all about it.) in any case, it seemed reasonable to expect that freyd's elegant derivations lift to the redundant numerations, viz the streams lurking at the intuitive background of all constructions. and indeed, the midpoint operation lifts to a coinductive definition on 3^N. but nothing beyond that point works for me. in particular, i don't know how to construct from the closed interval *with a numeration system* a *coalgebra* of all reals, *with the corresponding numeration*. neither of the reflection of midpoint algebras in abelian groups, nor the extension of the "yoneda" embedding of the interval in its endomorphism monoid extends to the numeration systems. how do you enrich the structure of abelian group by a numeration system? what should the midpoint algebra homomorphisms lift on the attached numerations? the alternative that i keep pushing are the conway coreals. the finite and infinite lists of 1 and -1 yield an irredundant representation of the real line, extended with the infinity on both ends. to get the real number corresponding to a list, sum up the initial 1s or -1s, until the sign changes. this is the integer part of the number. after that point, sum up the entries of the list divided by increasing powers of 2. this is, of course, gonshor's version of surreal numbers. it is a retract of the conway's version. but conway's games can be viewed as {L,R}-labelled hypersets. so they form a final coalgebra. the addition, and the multiplication arise as *eminently* coinductive operations. the addition happens to be defined by a coalgebra similar to the one defining the product of analytic functions, and the asynchronous product of processes. conway's definitions of all algebraic operations are very nice examples of coinductive programming. the idea is now to use gonshor's version as the real coalgebra, and conway's version as a generalized numeration system: instead of streams of digits, use {L,R}-labelled graphs, viz hypersets. gonshor's numbers correspond to the minimal representatives of conway's numbers, so they embed canonically; whereas conway's *simplicity theorem* yields the retraction. in practice, given two real numbers, say to add, and the desired precision of the result, you replace them by sufficiently small binary intervals, ie the simplest binary numbers contained. these lift to finite conway games, and easily add. finding the simplest form is trivial. i am not sure whether i am missing something, but with this approximation part, the algorithm does not seem inefficient at all any more. originally, this story was invented for the coalgebra of alternating dyadics, which has appeared in my paper with vaughan pratt. but alternating dyadics are easily seen to be just a version of gonshor's representation. and just like alternating dyadics/gonshor reals embed in conway's games, our coalgebra of continued fractions embeds in contorted fractions, mentioned by peter johnstone... one would expect that that numeration system might be still a bit more efficient, or less inefficient, though i didn't look at the details at all... happy halloween, -- dusko