October 2000 - Categories - categories.org.au

Re: coinduction: definable equationally?
by Andrej Bauer 03 Nov '00

03 Nov '00

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

2 1

FST TCS 2000 Call for Participation
by Sanjiva Prasad 31 Oct '00

31 Oct '00

******************************************************************* * * * Call for Participation * * * * Foundations of Software Technology * * and * * Theoretical Computer Science * * (FST TCS 2000) * * * * India International Centre * * New Delhi, India * * 13--15 December July, 2000 * * * * REGISTER AT http://www.cse.iitd.ernet.in~/fsttcs20 * * EARLY REGISTRATION DEADLINE IS November 15 * * * ******************************************************************* Invited Speakers: Peter Buneman (U Penn) Bernard Chazelle (Princeton) E. Allen Emerson (U Texas, Austin) Martin Groetschel (ZIB, Berlin) Jose Meseguer (SRI) Philip Wadler (Avaya Labs Satellite Events: Tutorial Workshop on Recent Advances in Programming Languages December 11-12, 2000 at IIT Delhi, Hauz Khas Workshop on Geometry December 16-17, 2000 at IIT Delhi, Hauz Khas FST TCS 2000 Preliminary Programme 13 December 2000 9:00-9:30 Opening 9:30-10:30 Invited Talk: E Allen Emerson Model Checking: Theory into Practice 10:30-11:00 Tea 11:00-12:30 40. Fast On-line/Off-line 100. Model checking CTL Algorithms for Optimal Properties of Pushdown Systems Reinforcement of a Network Igor Walukiewicz and its Connections with Principal Partition H. Narayanan, Sachin B. Patkar 59. On-Line Edge-Coloring 125. A Decidable Dense with a Fixed Number of Colors Branching-time Temporal Logic Lene Monrad Favrholdt, Salvatore La Torre and Morten Nyhave Nielsen Margherita Napoli 15. On Approximability of the 126. Fair Equivalence Relations Independent/Connected Edge Orna Kupferman, Nir Piterman, Dominating Set Problems Moshe Vardi Toshihiro Fujito 12:30-14:00 Lunch 14:00-15:00 Invited Talk: Philip Wadler An Algebra for XML Query 15:00-15:30 Tea 15:30-17:00 8. Arithmetic Circuits and 113. Combining Semantics with Polynomial Replacement Systems Non-Standard Interpreter Pierre McKenzie, Heribert Hierarchies Vollmer, Klaus W. Wagner Sergei Abramov, Robert Glueck 70. Depth-3 Arithmetic Circuits 112. Using Modes to Ensure for S(2,n)(X) and Extensions of Subject Reduction for Typed the Graham-Pollack Theorem Logic Programs with Subtyping Jaikumar Radhakrishnan, Pranab Jan-Georg Smaus, Francois Sen, Sundar Vishwanathan Fages, Pierre Deransart 130. The Weak Monadic Quantifier 23. Dynamically Ordered Alternation Hierarchy of Probabilistic Choice Logic Equational Graphs is Infinite Programming Ly Olivier Marina De Vos, Dirk Vermeir 14 December 2000 9:00-10:00 Invited Talk: Bernard Chazelle Irregularities of Distribution, Derandomization, and Complexity Theory 10:10-11:10 147. Coordinatized Kernels and Catalytic Reductions: Improved 12. A Complete Fragment of FPT Algorithms for Max Leaf Higher-Order Duration Spanning Tree and Other Problems $\mu$-Calculus Michael R. Fellows, Catherine Dimitar P. Guelev McCartin, Ulrike Stege, Frances A. Rosamond 53. Planar Graph Blocking for 39. A Complete Axiomatisation External Searching for Timed Automata Surender Baswana, Sandeep Sen Huimin Lin and Wang Yi 11:10-11:30 Tea 11:30-12:30 124. Text Sparsification via 120. Semantic Theory for Local Maxima Heterogeneous System Design Pierluigi Cresceznzi, Alberto Rance Cleaveland, Gerald Del Lungo, Roberto Grossi, Luettgen Elena Lodi, Linda Palgi, Gianluca Rossi 38. Approximate Swapped Matching 133. Formal Verification of the A Amir, M Lewenstein, E. Porat Ricart-Agrawala Algorithm Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari 12:30-14:00 Lunch 14:00-15:00 Invited Talk: Jose Meseguer Rewriting Logic as a Metalogical Framework 15:00-15:30 Tea 15:30-17:00 96. On distribution-specific 117. A General Framework for learning with membership queries Types in Graph Rewriting versus pseudorandom generation Barbara Koenig Johannes K�bler, Wolfang Lindner 69. $\Theta_2^p$-completeness: 146. The Ground Congruence for A classical approach for new Chi Calculus results Yuxi Fu, Zhenrong Yang Joel Vogel, Holger Spakowski 110. Is the Standard Proof System 122. Inheritance in the Join for SAT P-optimal? Calculus Johannes K�bler, Jochen Messner Cedric Fournet, Cosimo Laneve, Luc Maranget Didier Remy 15 December 2000 9:00-10:00 Invited Talk: Martin Gr�tschel Frequency Assignment in Mobile Phone Systems 10:10-11:10 65. Approximation Algorithms 118. The Fine Structure of for Bandwidth and Storage Game Lambda Models Allocation Problems under Real Pietro Di Gianantonio, Time Constraints Gianluca Franco Stefano Leonardi, Alberto Marchetti-Spaccamela, Andrea Vitaletti 37. Dynamic Spectrum Allocation: 127. Strong Normalisation of The Impotency of Duration Second Order Symmetric Notification Lambda-calculus Bala Kalyanasundaram, Kirk Pruhs Michel Parigot 11:10-11:30 Tea 11:30-12:30 94. Scheduling to minimize the 49. Keeping Track of the Latest average completion time of Gossip in Shared Memory Systems dedicated tasks Bharat Adsul, Aranyak Mehta, Foto Afrati, Eviripidis Bampis, Milind Sohoni Aleksei V. Fishin, Klaus Jansen Claire Keyon 73. Hunting for Functionally 123. On Concurrent Knowledge Analogous Genes and Logical Clock Abstractions M. T. Hallett, J. Lagergren Ajay Kshemkalyani 12:30-14:00 Lunch 14:00-15:00 Invited Talk: Peter Buneman Data Provenance: Some Basic Issues 15:00-15:30 Tea 15:30-16:30 20. Decidable Hierarchies of Starfree Languages Christian Glasser, Heinz Schmitz 58. Prefix languages of Church-Rosser Languages Jens R. Woinowski 16:30-17:00 Closing Organization: FST TCS 2000 is being organized by the Indian Institute of Technology, Delhi under the aegis of the Indian Association for Research in Computer Science (IARCS). -- Sanjiva Prasad Associate Professor Department of Computer Science and Engineering sanjiva(a)cse.iitd.ernet.in Indian Institute of Technology, Delhi (Off) +91 11 659 1294 Hauz Khas, New Delhi 110016 (Res) +91 11 659 1684 INDIA (Fax) +91 11 686 8765 http://www.cse.iitd.ernet.in/~sanjiva

1 0

Re: coinduction
by jesse＠andrew.cmu.edu 31 Oct '00

31 Oct '00

Dusko Pavlovic <dusko(a)kestrel.edu> 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 <s o p_1,g> + <0,c>: (N x X) + 1 -> N x X does it (p_1 is the projection map). Let <k,f>: 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_

1 0

Preprint: The co-Birkhoff theorem
by jesse＠andrew.cmu.edu 31 Oct '00

31 Oct '00

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

1 0

Conference on Algebraic Topological Methods in Computer Science
by Rick Jardine 31 Oct '00

31 Oct '00

First Announcement: Conference on Algebraic Topological Methods in Computer Science Department of Mathematics Stanford University July 30 - August 3, 2001 The application of algebraic topological methods in areas related to Computer Science is an emerging field that is of interest to both pure and applied mathematical scientists. The aim of this conference is to describe recent advances, and define the fundamental open problems in the field through a mixture of expository and technical lectures. There will be twenty lectures, on a variety of topics in the area. The following is a preliminary list of invited speakers: John Baez (Math, UC Riverside) Marshall Bern (Xerox PARC) Tamal Dey (CS, Ohio State) Herbert Edelsbrunner (CS, Duke) David Eppstein (CS, UC Irvine) Michael Freedman (Microsoft) Philippe Gaucher (CNRS, Strasbourg) Eric Goubault (Commissariat a l'Energie Atomique, France) Jean Goubault-Larrecq (ENS Cachan) Marco Grandis (Dip. di Mat., Genova) Jeremy Gunawardena (HP BRIMS) Joel Hass (Math Dept, UC Davis) Maurice Herlihy (CS, Brown) Reinhard Laubenbacher (NMSU) Laszlo Lovasz (Microsoft) Vaughan Pratt (CS, Stanford) Christian Reidys (Los Alamos National Lab) Bernd Sturmfels (Math Dept, UC Berkeley) Noson Yanofsky (CS, Brooklyn College) All conference announcements and information will be available at the web site: http://www.math.uwo.ca/~jardine/at-cs.html The organizers for this meeting are: Gunnar Carlsson: gunnar(a)math.stanford.edu Rick Jardine: jardine(a)uwo.ca

1 0

coinduction
by Al Vilcius 31 Oct '00

31 Oct '00

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(a)vilcius.com

5 4

Re: coinduction
by jesse＠andrew.cmu.edu 30 Oct '00

30 Oct '00

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 <dusko(a)kestrel.edu> 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

4 3

Re: coinduction: definable equationally?
by jesse＠andrew.cmu.edu 29 Oct '00

29 Oct '00

Vaughan Pratt <pratt(a)cs.stanford.edu> 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_

1 0

new electronic journal: AGT
by Bob Rosebrugh 24 Oct '00

24 Oct '00

[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)

1 0

Re: coinduction
by jesse＠andrew.cmu.edu 21 Oct '00

21 Oct '00

"Al Vilcius" <al.r(a)VILCIUS.com> 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 <F,f> 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 <A,a>, there is a unique coalgebra homomorphism from <A,a> to <F,f>. 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_

1 0