January 2003 - Categories - categories.org.au

Chair of Theoretical Computer Science
by Gordon Plotkin 01 Feb '03

01 Feb '03

Chair of Theoretical Computer Science, LFCS, School of Informatics, Edinburgh University The above chair is currently open; we seek outstanding candidates in any area of theoretical computer science. For details, see http://www.informatics.ed.ac.uk/events/vacancies/ Gordon Plotkin

1 0

Fields Institute Summer School in Logic & Theoretical CS
by P. Scott 31 Jan '03

31 Jan '03

Dear Colleagues: This is an update of the last announcement. June will be theoretical computer science month at U. Ottawa! The Field's Institute will sponsor a summer school in Logic and Foundations of Computation at the University of Ottawa this summer, June 2-20, 2003. This program will be hosted by the logic group in the Department of Mathematics and Statistics at the University of Ottawa (consisting of Philip Scott, Richard Blute, and Peter Selinger). The program will consist of 2 weeks of courses for graduate students, then a week of workshops in several areas of theoretical computer science. This program is particularly aimed at graduate students in mathematics, logic, theoretical computer science, mathematical linguistics and related areas. The program culminates in the 18th annual IEEE Logic in Computer Science (LICS2003) meeting at U. Ottawa June 21-27. For the latter, see http://www.dcs.ed.ac.uk/home/als/lics/. Weeks 1,2: Each week will consist of two courses (one in the morning, the other in the afternoon), taught by experts in the area. We are also expecting visiting experts, who may give informal seminars as well. We are planning topics that include: Week 1: (a) Categorical Logic and type theory and (b) Linear Logic. Lectures will be given by our logic group, as well as visiting scholars. Among the visitors we are pleased to have Thomas Ehrhard (Marseille), Robert Seely (McGill), and Robin Cockett (Calgary). Week 2: (a) Game Semantics and (b) Concurrency. We are honoured to announce that Samson Abramsky (Oxford) and Glynn Winskel (Cambridge), resp., will be lecturing on the two topics above. We hope to have other distinguished visitors who will give additional lectures. Week 3: Fields Institute Workshops. These include, among other topics, June 15-16: Quantum Programming Languages (Org: Peter Selinger), June 17: Game Semantics (In preparation) June 18-19: Mathematical Linguistics (Org: J. Lambek) June 19-20: Mobility Workshop (In preparation) Further details on these workshops will be forthcoming. Some limited funding scholarships will be made available to graduate students for attending the summer school. To apply for this money, we ask that you contact us and include the following information: 1) A one-page email letter stating your background as well as why you are interested in attending. 2) The letter should also state whether you have access to any other funding to attend. 3) An email letter of reference from your supervisor or an appropriate other person. Preference will be given to students working in the areas covered by the Fields Summer School. Applications should be received by February 28. Non-students are of course welcome to attend the summer school and/or workshops; there will be a nominal registration fee for attendance. For further information to apply, please contact any of us: Philip Scott (phil(a)site.uottawa.ca) Richard Blute (rblute(a)mathstat.uottawa.ca) Peter Selinger (selinger(a)mathstat.uottawa.ca) The Webpage of the Fields Institute Summer School in Logic and Theoretical Computer Science is: http://www.mathstat.uottawa.ca/lfc/fields2003/

1 0

Proof Theory List
by Alessio Guglielmi 31 Jan '03

31 Jan '03

Hello, there is a new list dedicated to proof theory: please find more info and a list of subscribers at <http://www.ki.inf.tu-dresden.de/~guglielm/Research/list.html>. -Alessio -- Alessio Guglielmi, PhD Department of Computer Science - Technische Universitaet Dresden Dresden - Germany <http://www.ki.inf.tu-dresden.de/~guglielm/>

1 0

CFP: FICS 03
by Igor Walukiewicz 30 Jan '03

30 Jan '03

Fixed Points in Computer Science FICS'03 A Satellite Workshop to ETAPS'2003 12-13 April, 2003, Warsaw, Poland CALL FOR PAPERS Aim. Fixed points play a fundamental role in several areas of computer science and logic by justifying induction and recursive definitions. The construction and properties of fixed points have been investigated in many different frameworks such as: design and implementation of programming languages, program logics, databases. The aim of the workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points. Previous workshops where held in Brno (1998, MFCS workshop), Paris (2000, LC2000 workshop), Florence (2001, PLI workshop). Copenhagen (2002, LICS workshop). Topics include, but are not restricted to: Construction and reasoning about properties of fixed points, categorical, metric and ordered fixed point models, continuous algebras, relation algebras, regular algebras of finitary and infinitary languages, formal power series, word and tree automata, the mu-calculus and other programming logics, fixed points in process algebras and process calculi, fixed points and the lambda calculus, fixed points in relation to dataflow and circuits, fixed points in logic programming, databases and complexity theory. Programme Committee: J. Adamek (Braunschweig) R. Amadio (Marseille) R. Backhouse (Nottingham) S. Bloom (Hoboken NJ) J. Bradfield (Edinburgh) A. Dawar (Cambridge) R. De Nicola (Florence) Z. Esik (cochair, Szeged) I. Guessarian (Paris) M. Mislove (Tulane) I. Walukiewicz (cochair, Bordeaux) Invited speakers: Martin Grohe (Edinburgh) Erich Gradel (Aachen) Damian Niwinski (Warsaw) Leszek Pacholski (Wroclaw) Contact person: Igor Walukiewicz LaBRI Domaine Universitaire, bat. A30 351, cours de la Liberation 33405 Talence Cedex FRANCE igw(a)labri.fr phone: +33 5 56.84.69.00 fax: +33 5 56.84.66.69 Paper submission: Authors are invited to send three copies of an abstract not exceeding three pages to Igor Walukiewicz. Electronic submissions in the form of uuencoded postscript files are encouraged and can be sent to igw(a)labri.fr. Submissions are to be received before February 14, 2003. Authors will be notified of acceptance by March 10, 2003. Proceedings: Preliminary proceedings containing the abstracts of the talks will be available at the meeting. Final proceedings will be published after the meeting as a special issue of Theoretical Informatics and Application (http://www.edpsciences.org/docinfos/ITA/) The meeting will be organized in affiliation to ETAPS'03: http://www.mimuw.edu.pl/etaps03 Important Dates: Submission: February 14, 2003 Notification: March 10, 2003 Final version of the abstract: March 17, 2003 More information is available at the web site http://www.labri.fr/~igw/fics

1 0

Re: Cauchy completeness of Cauchy reals
by Andrej Bauer 29 Jan '03

29 Jan '03

Alex Simpson <als(a)inf.ed.ac.uk> writes: > > > The map e : 2^N --> [0,1] defined by > > > > e x = x_0/2 + x_1/4 + x_2/8 + ... > > > > is epi in the effective topos, but it is not regular epi. > > This is clearly wrong. Every epi is regular, in a topos. > > My original statement was correct. In the effective topos, > the map from binary representations to Cauchy (= Dedekind) > reals is not epi. I stand corrected. I am confusing the effective topos with assemblies (or modest sets) over the first Kleene algebra. Andrej

4 3

Two questions on the real numbers
by Alex Simpson 28 Jan '03

28 Jan '03

While the topic is still hot, I'd like to post two more questions concerning the various real number objects. Just to recap, in any elementary topos with nno N we have the Cauchy reals R_C, the Dedekind reals R_D, and also the "Cauchy-completion (w.r.t. sequences) of R_C in R_D", as discussed thoroughly in previous postings. Let's call this latter object R_E. All three objects are logically defined, and hence preserved by logical functors between toposes. Martin Escardo and I proved that R_E is also preserved by inverse image functors of essential geometric morphisms. (Actually, we proved this for the closed unit interval I_E in R_E. The result for R_E follows by exibiting R_E as a coequalizer of two well-chosen maps from N x I_E to itself.) QUESTION 1. What preservation results are available for R_C and R_D? Surely something is known about this. I can't, at the moment, see any reason for them to be preserved by inverse image functors of arbitrary essential geometric morphisms. Interesting mathematical differences between the objects arise when one considers algebraic closure properties of the complex numbers C_C, C_D and C_E associated with R_C, R_D and R_E respectively. In Fourman and Hyland, "Sheaf models for analysis" (Springer LNM 753, 1979) it is shown that the Dedekind complex numbers C_D are not in general algebraically closed. This fails in the strong sense that, in certain toposes, one can actually exhibit a polynomial that has no root. Thus the fundamental theorem of algebra does not hold in general for C_D. On the other hand, in Ruitenberg, "Constructing roots of polynomials over the complex numbers" (in "Computational aspects of Lie group representations and related topics", CWI Tract 84, Amsterdam, 1990), it is shown that the fundamental theorem of algebra does hold for C_C in any topos. (I first heard about this paper from Fred Richman. I have never seen it. I have only read its math review, no.92g:03085.) The conflicting picture above, leads naturally to: QUESTION 2. Does the fundamental theorem of algebra hold for C_E? I would be interested to hear any ideas at all related to these questions. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson(a)ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209

1 0

Re: Cauchy completeness of Cauchy reals
by Andrej Bauer 28 Jan '03

28 Jan '03

Alex Simpson <als(a)inf.ed.ac.uk> writes: > In fact not. Markov's principle holds in the effective topos, and > there, unless I'm much mistaken, it is not even true that the map from > binary representations to Cauchy (= Dedekind) reals in [0,1] is epi, > let alone split epi. The map e : 2^N --> [0,1] defined by e x = x_0/2 + x_1/4 + x_2/8 + ... is epi in the effective topos, but it is not regular epi. In terms of logic, this means that forall a : [0,1]. (not not (exists x : 2^n. (e x = a))) is valid in the effective topos, but forall a : [0,1]. (exists x : 2^n. (e x = a)) is not valid. Andrej

2 1

What does it take to identify the field and the continuum of reals?
by Vaughan Pratt 27 Jan '03

27 Jan '03

By way of motivating the question posed in the subject line I'll pick up in the middle of this thread on Dedekind vs. Cauchy reals, which I can't help much with I'm afraid but which provides a nice jumping off point for my real topic nonetheless. >From: Martin Escardo > >From: Dusko Pavlovic > > >From: Martin Escardo > > >NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex > > >Simpson and I characterized "the Cauchy completion of the rationals > > >within the Dedekind reals" as a free algebra > > > > > and vaughan pratt and i characterized the cauchy reals as a final > > coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. > >I forgot to mention this --- I apologize. In your paper, you work in >Set. Do you think your construction works in any topos? If so, what >would "Cauchy reals" mean precisely in this general context? Thanks. I would bounce this question back to Martin: what did he mean by "the Dedekind reals" in his attribution to Freyd? Both the Pavlovic-Pratt and Freyd constructions of the continuum as a final coalgebra characterize the continuum only up to its order type (and hence up to homeomorphism if we take the usual order topology generated by the open intervals). Cuts in the *field* Q of rationals inherit Q's metric, but cuts in the *poset* Q acquire only topology. Only with Q qua poset would it be fair to say that either Peter's or our coalgebraic construction of the continuum "characterized the Dedekind reals." The Cauchy completion of the rationals on the other hand requires Q to be at minimum a metric space and surely a field if you want to bring in 1/n. This distinction constitutes a disconnect between Martin's first two sentences that subsequent emails are at risk of propagating. I have not to date seen any really convincing marriage of the algebraic and coalgebraic approaches to defining real numbers. The very fact that algebra produces the field of reals while coalgebra produces the continuum as understood by descriptive set theorists draws a sharp line right there between the two approaches. The only marriage I'm aware of that even works at all is Conway's elegant construction of his surreal numbers. It is a marriage because (loosely speaking) the numbers entering on the ends create algebra while those interpolating their predecessors in the Conway ordering create coalgebra. A great virtue of this construction is its complete lack of any distinction between, or even reference to, algebra and coalgebra, the implicit presence of both notwithstanding. Unfortunately it produces neither the field of reals nor a continuum. Conway doesn't get the former because just before day omega he has only produced the ring of binary fractions, those rationals of the form m/2^n. Day omega itself however witnesses the birth not only of all the remaining reals but the first few infinities and infinitesimals, in particular ±w and their reciprocals. This doesn't even form an additive monoid let alone a ring since w+w for example is not due to arrive for another w days! Negation is the only arithmetic operation surviving the day-to-day evolution of Conway's surreal universe, from its little bang to its apocalyptic Field. Seeking closure, Conway slogs gamely on through *all* the ordinals to produce a Field of reals. (Or rather The Field, the maximal such having been shown elsewhere to be unique, if I've understood that correctly.) This being a proper class, not only does it not have the cardinality of the continuum, it doesn't have a cardinality at all! Now I conjecture that stopping just before day \epsilon_0, for the sake of getting a set, produces a field closed under all functions whose n-th bit is computable in time f(n) where f is definable in Peano arithmetic. And it may well be that Conway already has a field just before day \omega^\omega, I haven't checked but surely someone has by now (I'm very bad at keeping up with these things, sorry). But all this is for naught here, since even the smallest Conway field whatever it might turn out to be is cannot be Archimedean, for the reason above. And although it has the power of the continuum it lacks its order type: with the usual order topology, the Conway continuum becomes totally disconnected as soon as ±1 appear, and remains that way thenceforth. Total disconnectedness is not anything a continuum can be proud of. It seems to me that topos theory, or logic, or something in between if that makes sense, should have something to say about a gap between the algebra and coalgebra of the reals. Algebraically the reals form a field, coalgebraically they form a continuum. What is the logical strength of the weakest framework identifying these dual views of the reals? Vaughan Pratt

3 2

Re: Generalization of Browder's F.P. Theorem?
by Andrej Bauer 27 Jan '03

27 Jan '03

Michael Barr <barr(a)barrs.org> writes: > For Bishop, a real number is an equivalence class of pairs of > RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n - > a_m/b_m| < 1/m + 1/n ... Actually, Bishop purposely avoids taking a real to be an equivalence class of sequences, presumably because he does not want to assume the axiom of countable choice. A sequence as described above is sometimes called a "fundamental sequence". Two such sequences x = (a_n/b_n) and y = (c_n/b_n) are said to "coincide", written x ~ y iff |a_n/b_n - c_m/d_m| < 2/n + 2/m, where I might have gotten the right-hand side slightly wrong. Now there are two possibilities: (1) we say that a real is an equivalence class of fundamental sequences under the relation ~, or (2) we say that a real _is_ a fundamental sequence, where two reals are claimed "equal" if they coincide (the approach taken by Bishop). The first alternative gives us what is usually called "Cauchy reals". The difference between the two is apparent when we attempt to show that every Cauchy sequence of reals has a limit. In the first case we are given a sequence of equivalence classes of fundamental sequences. In order to construct a fundamental sequence representing the limit we need to _choose_ a representative from each equivalence class. In the second case a Cauchy sequence of reals is a sequence of fundamental sequences, so no choice is required. There seems to be an open question in regard to this, advertised by Alex Simpson and Martin Escardo: find a topos in which Cauchy reals are not Cauchy complete (i.e., not every Cauchy sequence of reals has a limit). For extra credit, make it so that the Cauchy completion of Cauchy reals is strictly smaller than the Dedekind reals. Has this been advertised on this list already? Or was it the FOM list? [If anyone replies to this, I suggest you start a new discussion thread.] Andrej Bauer

7 10

(pre-)Sheaves
by Galchin Vasili 26 Jan '03

26 Jan '03

Hello, I am trying to get my mind around (pre-)sheaves. I have studied point set topology in the past, but I didn't run into the notion of local homeomorphism. It seems to me that every local homeomorphism is a homeomorphism (because in a topological space (X, T), X is always a neighorhood of any point in X). Am I correct? Regards, Bill Halchin

2 1