From MAILER-DAEMON Sun Mar 30 15:41:27 2003 Date: 30 Mar 2003 15:41:27 -0400 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1049053287@mta.ca> X-IMAP: 1044293014 0000000066 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From rrosebru@mta.ca Mon Feb 3 11:41:21 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 03 Feb 2003 11:41:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18fiWo-0004rg-00 for categories-list@mta.ca; Mon, 03 Feb 2003 11:28:58 -0400 X-Authentication-Warning: spurv.itu.dk: birkedal set sender to birkedal@itu.dk using -f To: categories@mta.ca Subject: categories: Ph.D. scholarships at the IT University of Copenhagen Reply-To: birkedal@itu.dk From: Lars Birkedal Date: 03 Feb 2003 09:45:25 +0100 Message-ID: Lines: 25 User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 1 A number of Ph.D. scholarships are now advertised at the IT University of Copenhagen, Denmark. There are openings in several areas, including the research areas of the Theory Department: algorithms and complexity theory, semantics of logics and programming languages, category theory, categorical logic and type theory, models of concurrency, verification, mobile computation. The official announcement of the Ph.D. scholarships can be found at http://www.it-c.dk/Internet/jobs/puuAlA/ Application deadline is noon March 19, 2003. More information about the Theory Deparment can be found at http://www.it-c.dk/English/research/theory/ Best regards, Lars Birkedal ---------------------------------------------------------------------- Lars Birkedal (birkedal@it-c.dk) Associate Professor, Ph.d. Head of Theory Department The IT University of Copenhagen From rrosebru@mta.ca Wed Feb 5 10:49:48 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 10:49:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gQko-0005Fp-00 for categories-list@mta.ca; Wed, 05 Feb 2003 10:42:22 -0400 Message-Id: <200302040047.QAA03714@coraki.Stanford.EDU> X-Mailer: exmh version 2.1.1 10/15/1999 To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals In-Reply-To: Message from Vaughan Pratt of "Wed, 22 Jan 2003 22:29:51 PST." Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Mon, 03 Feb 2003 16:47:58 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 2 While I'm comfortable with coalgebraic presentations of the continuum, as well as such algebraic presentations as the field P/I (P being a ring of certain polynomials, I the ideal of P generated by 1-2x) that I mentioned a week or so ago, I'm afraid I'm no judge of constructive approaches to formulating Dedekind cuts. Would a toposopher (or a constructivist of any other stripe) view the following variants as all more or less equally constructive, for example? 1. Define a (closed) interval in the reals as a disjoint pair (L,R) consisting of an order ideal L and an order filter R, both in the rationals standardly ordered, both lacking endpoints. Order intervals by pairwise inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'. Define the reals to be the maximal elements in this order. Define an irrational to be a real for which (L,R) partitions Q. 2. Ditto but with the reals defined instead to be intervals for which Q - (L U R) is a finite set. ("Finite set" rather than just "finite" to avoid the other meaning of "finite interval." The order plays no role in this definition, maximality of reals in the order being instead a theorem.) 3. As for 2 but with "finite" replaced by "cardinality at most 1". The predicate "rational" is identified with the cardinality of Q - (L U R). Vaughan From rrosebru@mta.ca Wed Feb 5 10:49:48 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 10:49:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gQjU-00056k-00 for categories-list@mta.ca; Wed, 05 Feb 2003 10:41:00 -0400 Message-ID: <20030203204959.52730.qmail@web12207.mail.yahoo.com> Date: Mon, 3 Feb 2003 12:49:59 -0800 (PST) From: Galchin Vasili Subject: categories: "Vicious Circles" by Barwise and Moss To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 3 Hello, I just started reading "Vicious Circles", which is discussion of non-wellfounded or hypersets. It seems like this book could be rewritten from a category theoretic viewpoint at the very least and perhaps even a topos viewpoint. I say topos because I have an intuition that a category with non-wellfounded sets as objects and total functions as morphims is a topos. I am just scratching the surface of this book so it is just an intuition. Or perhaps morphisms should be some other kind of function that preserves structure. Any guidance? Regards, Bill Halchin From rrosebru@mta.ca Wed Feb 5 15:35:06 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 15:35:06 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gVI7-0007O9-00 for categories-list@mta.ca; Wed, 05 Feb 2003 15:33:03 -0400 Date: Wed, 5 Feb 2003 16:06:02 +0000 (GMT) From: "Prof. Peter Johnstone" To: CATEGORIES LIST Subject: categories: Re: Cauchy completeness of Cauchy reals In-Reply-To: <200302040047.QAA03714@coraki.Stanford.EDU> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18gS3m-00001q-00*TL.8jifFciY* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 On Mon, 3 Feb 2003, Vaughan Pratt wrote: > > While I'm comfortable with coalgebraic presentations of the continuum, as > well as such algebraic presentations as the field P/I (P being a ring of > certain polynomials, I the ideal of P generated by 1-2x) that I mentioned > a week or so ago, I'm afraid I'm no judge of constructive approaches to > formulating Dedekind cuts. Would a toposopher (or a constructivist of > any other stripe) view the following variants as all more or less equally > constructive, for example? > > 1. Define a (closed) interval in the reals as a disjoint pair (L,R) > consisting of an order ideal L and an order filter R, both in the rationals > standardly ordered, both lacking endpoints. Order intervals by pairwise > inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'. > Define the reals to be the maximal elements in this order. Define an > irrational to be a real for which (L,R) partitions Q. > > 2. Ditto but with the reals defined instead to be intervals for which > Q - (L U R) is a finite set. ("Finite set" rather than just "finite" to > avoid the other meaning of "finite interval." The order plays no role > in this definition, maximality of reals in the order being instead a > theorem.) > > 3. As for 2 but with "finite" replaced by "cardinality at most 1". > The predicate "rational" is identified with the cardinality of Q - (L U R). > No constructivist (of whatever stripe) would be happy talking about Q - (L U R), as in your second and third definitions, since he wouldn't want to assume that L and R were complemented as subsets of Q. Your first definition, if I understand it correctly, is equivalent to what most toposophers would call the MacNeille reals -- that is, the (Dedekind-MacNeille) order-completion of Q. If you "positivize" the second and third (which would appear to be equivalent, for any sensible notion of finiteness) by saying "Whenever p and q are rationals with p < q, then either p \in L or q \in R", you get the Dedekind reals, which are a proper subset of the MacNeille reals (though they coincide iff De Morgan's law holds) but have rather better algebraic properties. Peter Johnstone From rrosebru@mta.ca Thu Feb 6 16:43:49 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 06 Feb 2003 16:43:49 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gsnO-0002dk-00 for categories-list@mta.ca; Thu, 06 Feb 2003 16:38:54 -0400 Date: Wed, 5 Feb 2003 12:56:33 -0800 From: Toby Bartels To: CATEGORIES mailing list Subject: categories: Re: Cauchy completeness of Cauchy reals Message-ID: <20030205205632.GC26302@math-rs-n01.ucr.edu> References: <3E36ED4F.4070807@kestrel> <1043829334.3e37925619e77@mail.inf.ed.ac.uk> <3E3F849F.5080704@kestrel.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <3E3F849F.5080704@kestrel.edu> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 Dusko Pavlovic wrote: >Alex Simpson wrote: >>Somebody wrote: >>>that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k >>>s.t. 1/2^k < e. this is *equivalent* to markov's principle. >>The property quoted is in fact a trivial consequence of intuitionistic >>arithmetic alone. It has nothing to do with Markov's principle. >for a real number e, i am pretty sure that the above is equivalent with >markov's principle. it must be in books, but i think you can't miss the >proof if you try. I don't remember the original context, so I don't know who's right, but the answer depends on what sort of real number e could be. It can't be 0, for example, so what can it be? * If e > 0, then work with 1/e and use the Archimedean property; Bishop would recognise and accept this proof. * But if you only know that e <= 0 is false, then you need Markov's principle to deduce e > 0. -- Toby From rrosebru@mta.ca Thu Feb 6 16:43:49 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 06 Feb 2003 16:43:49 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gsnr-0002fM-00 for categories-list@mta.ca; Thu, 06 Feb 2003 16:39:23 -0400 Date: Thu, 6 Feb 2003 10:44:33 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras In-Reply-To: <20030204022954.98645.qmail@web12202.mail.yahoo.com> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18gjWE-0004Or-00*kYnPgBf/7Og* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 On Mon, 3 Feb 2003, Galchin Vasili wrote: > > Hello, > > I understand (to some degree) full combinatory algebra, but I don't > understand the motivation behind the definition of a partial combinatory > algebra. E.g. why do we have Sxy converges/is defined? I'd like to know the answer to this too. Why does *everyone*, in writing down the definition of a PCA, include the assumption that Sxy is always defined? As far as I can see, the only answer is "because everyone else does so"; the condition is never used in the construction of realizability toposes, or in establishing any of their properties. In every case where you need to know that a particular term Sab is defined, it's easy to find a particular c such that Sabc is provably defined. Peter Johnstone From rrosebru@mta.ca Thu Feb 6 16:43:49 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 06 Feb 2003 16:43:49 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gsmy-0002bI-00 for categories-list@mta.ca; Thu, 06 Feb 2003 16:38:28 -0400 From: John Longley X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to jrl@localhost using -f To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras Message-ID: <1044469182.3e4155bed0abd@mail.inf.ed.ac.uk> Date: Wed, 05 Feb 2003 18:19:42 +0000 (GMT) References: <20030204022954.98645.qmail@web12202.mail.yahoo.com> In-Reply-To: <20030204022954.98645.qmail@web12202.mail.yahoo.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 129.215.58.96 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 7 Bill Halchin writes: > I understand (to some degree) full combinatory algebra, but I > don't > understand the motivation behind the definition of a partial > combinatory > algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x? The somewhat mysterious definition of (partial or full) combinatory algebras is really motivated by the fact that it is equivalent to a "combinatory completeness" property, which is a bit less mysterious but more cumbersome to state. Informally, combinatory completeness says that all functions definable in the language of A are themselves representable by elements of A. More precisely: A is a PCA iff for every formal expression e (built up from variables x,y_1,...,y_n and constants from A via juxtaposition), there is a formal expression called (\lambda x.e), whose variables are just y_1,...,y_n, such that (\lambda x.e)[b_1/y_1,...,b_n/y_n] is defined for all b_1,...,b_n \in A, (\lambda x.e) a [b_1/y_1,...,b_n/y_n] ~ e[a/x,b_1/y_1,...,b_n/y_n] (This is easiest to understand in the case n=0.) A similar statement holds for full combinatory algebras where everything is always defined. The term (\lambda x.e) can be constructed via the Curry translation from lambda calculus to combinatory logic. The condition "Sxy is defined" is needed for this to work. Also, I should say the whole theory of realizability models goes through much more smoothly with this condition, otherwise one has to keep making tiresome exemptions for the case of the object 0. I imagine the condition becomes strictly necessary at some point, e.g. in the proof that PER is an internal category. As for Kxy ~ x, that's the same as saying Kxy=x, because all elements x of A are of course defined. Cheers, John From rrosebru@mta.ca Fri Feb 7 11:15:01 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 07 Feb 2003 11:15:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18hABK-0000PY-00 for categories-list@mta.ca; Fri, 07 Feb 2003 11:12:46 -0400 Date: Fri, 7 Feb 2003 10:57:42 +0100 (CET) From: Message-Id: <200302070957.KAA10380@kodder.math.uu.nl> To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras X-Sun-Charset: US-ASCII X-Virus-Scanned: by AMaViS snapshot-20020300 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 8 > Date: Thu, 6 Feb 2003 10:44:33 +0000 (GMT) > From: "Prof. Peter Johnstone" > Subject: categories: Re: Realizibility and Partial Combinatory Algebras > > On Mon, 3 Feb 2003, Galchin Vasili wrote: > > > > > Hello, > > > > I understand (to some degree) full combinatory algebra, but I don't > > understand the motivation behind the definition of a partial combinatory > > algebra. E.g. why do we have Sxy converges/is defined? > > I'd like to know the answer to this too. Why does *everyone*, in writing > down the definition of a PCA, include the assumption that Sxy is always > defined? As far as I can see, the only answer is "because everyone else > does so"; the condition is never used in the construction of > realizability toposes, or in establishing any of their properties. > In every case where you need to know that a particular term Sab is > defined, it's easy to find a particular c such that Sabc is provably > defined. > > Peter Johnstone Dear Peter, I think the relevance of this condition (Sxy defined) is explained in the Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they have a definition of "c-pca" which is just omitting this requirement. They show that the standard P(A)-indexed preordered set, for a c-pca A, can fail to be a tripos. So the condition IS used. Another condition which is often imposed is really redundant: it is the requirement that, if sxyz defined, then xz(yz) defined and equal to sxyz. There are important constructions of realizability toposes where this fails to hold. Jaap van Oosten From rrosebru@mta.ca Fri Feb 7 11:15:01 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 07 Feb 2003 11:15:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18hACG-0000Xb-00 for categories-list@mta.ca; Fri, 07 Feb 2003 11:13:44 -0400 Date: Fri, 7 Feb 2003 13:57:05 +0100 (CET) From: Peter Lietz To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras In-Reply-To: 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: 9 Hello, On Thu, 6 Feb 2003, Prof. Peter Johnstone wrote: > I'd like to know the answer to this too. Why does *everyone*, in writing > down the definition of a PCA, include the assumption that Sxy is always > defined? As far as I can see, the only answer is "because everyone else > does so"; the condition is never used in the construction of > realizability toposes, or in establishing any of their properties. > In every case where you need to know that a particular term Sab is > defined, it's easy to find a particular c such that Sabc is provably > defined. I'd like to vehemently contradict the claim that the condition "sab is always defined" is never used in the construction of realizability toposes. In the paper "Modified Realizability Toposes and Strong Normalization Proofs (Extended Abstract)" by Martin Hyland and Luke Ong, a weaker notion of combinatory algebra, called "conditionally partial combinatory algebra c-pca)", in which the requirement in question is actually dropped, is thoroughly examined. The axioms for a c-pca are that (K) kxy = y (S) sxyz ~= xz(yz) where by "~=" I mean Kleene-equality (i.e. the r.h.s. is defined iff the l.h.s. is defined in which case they are equal). It is not required for a c-pca that "sxy" exists, but if z exists such that xz(yz) exists then sxyz and hence sxy exists by the axiom (S). The motivation for introducing the notion of a c-pca in the paper is that there is a very relevant c-pca which is not a pca. It consists of strongly normalizing lambda terms modulo closed beta equivalence and can be used for providing a categorical point of view on the "candidates of reducibility" method for strong normalization proof. It is shown in the paper that the standard realizability tripos construction will fail to actually deliver a tripos: The set of subsets of the c-pca taken as the set of truth-values won't even model minimal logic, which is why a "modified realizability topos" construction is used in the paper. So there is a strong reason for stipulating the existence of sxy. One relaxation of the notion of pca which won't break the usual constructions but is nevertheless rarely employed (exception is e.g. Longley's work) is the following: instead of sxyx ~= xz(yz) one might merely require sxyz ~> xz(yz), i.e., sxyz is allowed to be more defined than xz(yz). However, I don't know of any interesting models which do not satisfy (S) with Kleene equality anyway. Respectfully yours, Peter Lietz From rrosebru@mta.ca Sat Feb 8 10:48:23 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 08 Feb 2003 10:48:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18hW9s-0004Eh-00 for categories-list@mta.ca; Sat, 08 Feb 2003 10:40:44 -0400 From: John Longley To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras Message-ID: <1044631562.3e43d00ae7e2c@mail.inf.ed.ac.uk> Date: Fri, 07 Feb 2003 15:26:02 +0000 (GMT) References: <20030204022954.98645.qmail@web12202.mail.yahoo.com> In-Reply-To: <20030204022954.98645.qmail@web12202.mail.yahoo.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Originating-IP: 129.215.58.96 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 10 > I understand (to some degree) full combinatory algebra, but I don't > understand the motivation behind the definition of a partial combinatory > algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x? Here's another way to motivate the definition of PCAs, which I believe also shows (in response to Peter Johnstone's message) where the definedness condition is used in the standard realizability construction. Let A be any set with a partial binary operation (thought of as "application"). Let PA be the powerset of A. The idea is that we want to use PA as a little model for minimal implicational logic. We think of sets X \in PA as "propositions", and elements a \in X as "proofs" or "witnesses" for X. We think of the empty set as "false" since it has no witnesses. We next define an operation => on PA, corresponding to "implication", as follows: X => Y = { a \in A | for all b \in X. ab defined and ab \in Y } [Idea: a proof of X=>Y should map any proof of X to a proof of Y.] The basic idea here is often attributed to Dana Scott. Now, given any formula \phi built up from propositional variables p_1,...,p_n using implication, and any valuation v assigning elements of PA to these variables, we can interpret \phi in PA to get an element [[\phi]]_v \in PA. Let us say \phi holds in our model ( A |= \phi ) if there's some a \in A such that for all valuations v we have a \in [[\phi]]_v. [In other words, there's a uniform proof that all instances of \phi are true.] We'd like this model to be sound for the (intuitionistic) logic of pure implication. As is well known, the two axioms p -> q -> p (p -> q -> r) -> (p -> q) -> (p -> r) and the modus ponens rule suffice for deriving all theorems of this logic. Since modus ponens is clearly sound for the above interpretation, we just need to assume we have "uniform proofs" in A of the above two formulae. Now suppose A contains elements k,s satisfying the axioms of a PCA. Then it is simple to show that k,s respectively provide realizers for the above two formulae, and hence A soundly models minimal implicational logic. The condition "sxy defined" is important here, as can be seen by interpreting p as \emptyset, and q and r as A. The question of the converse is quite interesting. I have occasionally suggested that the definition of PCA should be weakened to allow sxyz >~ (xz)(yz), where >~ means "if the RHS is defined then so is the LHS and they are equal". Some support for this proposal could perhaps be drawn from the following result, which I had not noticed before: Let A be any partial applicative structure. Then (PA,=>) as above soundly models minimal implicational logic iff there exist k,s \in A satisfying kxy = x, sxy defined, sxyz >~ (xz)(yz) (I do have examples of structures that are PCAs in this weaker sense but not in the standard sense, but they are a little obscure.) Anyhow, the "PA construction" above is an important part of the tripos-theoretic construction of realizability models, so I think this shows that "sxy defined" is needed even to ensure the realizability model is a model for implicational logic. (My suggestion regarding internal categories in my previous message was overkill!) Incidentally, a few years ago, Hyland and Ong considered structures called "conditionally partial combinatory algebras", where one assumes sx defined but not sxy defined. They observed that the standard realizability construction does not in general work for CPCAs, but (in certain interesting cases) a modified realizability construction does. Cheers, John From rrosebru@mta.ca Sat Feb 8 10:51:18 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 08 Feb 2003 10:51:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18hWG2-0004QV-00 for categories-list@mta.ca; Sat, 08 Feb 2003 10:47:06 -0400 Date: Fri, 7 Feb 2003 23:43:45 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras In-Reply-To: <200302070957.KAA10380@kodder.math.uu.nl> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18hI9q-0000Ou-00*BU.7iwWPGow* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 11 On Fri, 7 Feb 2003 jvoosten@math.uu.nl wrote: > > I think the relevance of this condition (Sxy defined) is explained in the > Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization > Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they > have a definition of "c-pca" which is just omitting this requirement. > They show that the standard P(A)-indexed preordered set, for a c-pca A, > can fail to be a tripos. So the condition IS used. > I hope Jaap and Peter will forgive me for saying that I think they missed the point of my message. (Perhaps it's my fault -- with hindsight, I wasn't as clear as I should have been. I really ought to stop trying to reply to things like this late at night -- although, as you'll see from the header of this message, I'm doing it again.) Of course I know about the Hyland--Ong paper: indeed, I reviewed it for Zentralblatt. However, the point I was trying to make was that the construction of the quasitopos of A-valued assemblies, and the proof that its effectivization is a topos, make no use whatever of the condition that Sxy is always defined. The fact that the tautology ((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to be realized by S when p is empty has no effect on this construction, because one never has to deal with "propositions" having an empty set of realizers. So, whilst a tripos-theorist (if such a creature exists) may indeed have cause to worry about whether Sxy might be undefined, there seems to be no reason why a topos-theorist should do so. [Yes, yes, I know that I was responsible for inventing the term "tripos", and therefore that if anyone can legitimately be called a tripos-theorist then I can. But I don't believe that I am a tripos-theorist (which implies that no-one is).] Peter Johnstone From rrosebru@mta.ca Sun Feb 9 15:50:14 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 09 Feb 2003 15:50:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18hxOX-0000XN-00 for categories-list@mta.ca; Sun, 09 Feb 2003 15:45:41 -0400 Date: Sun, 9 Feb 2003 20:09:26 +0100 (CET) From: Peter Lietz To: categories@mta.ca Subject: categories: Re: Realizibility and Partial Combinatory Algebras In-Reply-To: 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 On Fri, 7 Feb 2003, Prof. Peter Johnstone wrote: > Of course I know about the Hyland--Ong paper: indeed, I reviewed it for > Zentralblatt. However, the point I was trying to make was that the > construction of the quasitopos of A-valued assemblies, and the proof > that its effectivization is a topos, make no use whatever of the > condition that Sxy is always defined. The fact that the tautology > ((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to > be realized by S when p is empty has no effect on this construction, > because one never has to deal with "propositions" having an empty > set of realizers. Dear Professor Johnstone, I obviously assumed strongly that you know the Hyland-Ong paper and was hence rather puzzled by what I mistakenly took for your question. As to the question regarding A-valued assemblies when A is a c-pca, I think I can give a justification for the axiom "Sab exists" as well. I claim that if the axiom "Sab exists" is absent, then the resulting category of A-valued assemblies is not a quasi-topos. One can form the category of A-valued assemblies and it is regular and cartesian closed. However, the realizers for the evaluation maps and also the construction of a realizer for the transpose of a map may exist, but one has to make a case analysis as to whether the source object is inhabited or not. Therefore it seems unlikely that the category is locally cartesian closed, as these operations cannot be carried out in a uniform manner. If this is the case then the category's exact completion is not a topos. I am aware that this argument is pretty vague. For a rigorous proof I would try to show that IF the subobjects of the threefold product of Nabla(P(A)) do form a Heyting-algebra, which if I am right is one of the requirements for a quasi-topos, THEN "Sab always exists". I would go about it as follows. 1. Show that the exponent subobject of two subobjects of an object is - if it exists - constructed as in the "unconditional" pca case. 2. Define the subobject m:S->Nabla(P(A)) with S = {M\subseteq A | M inhabited} and the set of realizers of M w.r.t. S being M (and m being the obvious map). 3. Interpret the S-tautology of intuitionistic propositional logic taking u,v and w as the pullbacks of m along the 1st, 2nd and 3rd projection of Nabla(P(A)) x Nabla(P(A)) x Nabla(P(A)), respectively. 4. Observe that it is the full subobject and use the reasoning of the Hyland-Ong paper to show that "Sab always exists". Should I be wrong, this would also be good news in a way, because it would imply that the standard construction of A-valued assemblies could be used for semantic strong normalization proofs instead of the more complicated construction of modified assemblies. Best regards, Peter Lietz From rrosebru@mta.ca Mon Feb 10 10:46:13 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 10 Feb 2003 10:46:13 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18iF7q-0000VG-00 for categories-list@mta.ca; Mon, 10 Feb 2003 10:41:38 -0400 From: Alex Simpson X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to als@localhost using -f To: CATEGORIES mailing list Subject: categories: Weak choice principles Message-ID: <1044845117.3e47123d29d65@mail.inf.ed.ac.uk> Date: Mon, 10 Feb 2003 02:45:17 +0000 (GMT) MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 130.54.16.90 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 13 The recent discussion about real numbers in toposes has reminded me of some questions I've previously wondered about concerning choice principles in toposes. As is well known, all that is needed to get the Cauchy reals and Dedekind reals to coincide (and hence the Cauchy completeness of the Cauchy reals) is N-N-choice (N being the natural numbers): (AC-NN) (\forall n:N. \exists m:N. A(n,m)) \implies \exists f:N->N. \forall n:N. A(n,f(n)) This is a very weak choice principle. Under classical logic it is simply true (by the least number principle). Although not provable intuitionistically, it is accepted by the Bishop school of constructivism (in fact they accept full dependent choice). What I want to remark upon is that the coincidence of the Cauchy and Dedekind reals also follows from the, apparently weaker, principle of bounded choice: (AC-Nb) (\forall n:N. \exists m \leq n. A(n,m)) \implies \exists f:N->N. \forall n:N. (f(n) \leq n) \and A(n,f(n)) from which one can derive, for any g:N->N (\forall n:N. \exists m \leq g(n). A(n,m)) \implies \exists f:N->N. \forall n:N. (f(n) \leq g(n)) \and A(n,f(n)). Alongside this it is natural to consider a principle of boolean choice: (AC-N2) (\forall n:N. \exists m \leq 1. A(n,m)) \implies \exists f:N->N. \forall n:N. (f(n) \leq 1) \and A(n,f(n)). (I am assuming 0 is a natural number). From (AC-N2) one can derive for any k:N, (\forall n:N. \exists m \leq k. A(n,m)) \implies \exists f:N->N. \forall n:N. (f(n) \leq k) \and A(n,f(n)). One obviously has implications (AC-NN) ==> (AC-Nb) ==> (AC-N2) QUESTION 1 Can either of the above implications be reversed? My conjecture is that they can't. Regarding the relationship to the real numbers, as remarked above we have: (AC-Nb) ==> R_C = R_D where R_C and R_D are the Cauchy and Dedekind reals respectively. In fact this implication cannot be reversed. More strongly: R_C = R_D =/=> (AC-N2) QUESTION 2 Does (AC-N2) imply R_C = R_D? Again, my conjecture is that it doesn't. Any counterexample here would of course simultaneously show that (AC-N2) does not imply (AC-Nb). I'd be interested to hear if anyone has ideas on these questions, or knows of references in which the above choice principles (other than AC-NN) are discussed. Thanks, Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209 From rrosebru@mta.ca Wed Feb 5 11:37:25 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 11:37:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gRao-000385-00 for categories-list@mta.ca; Wed, 05 Feb 2003 11:36:06 -0400 Message-ID: <20030204022954.98645.qmail@web12202.mail.yahoo.com> Date: Mon, 3 Feb 2003 18:29:54 -0800 (PST) From: Galchin Vasili Subject: categories: Realizibility and Partial Combinatory Algebras To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 14 Hello, I understand (to some degree) full combinatory algebra, but I don't understand the motivation behind the definition of a partial combinatory algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x? Regards, Bill Halchin From rrosebru@mta.ca Wed Feb 5 11:37:52 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 11:37:52 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gRc5-0003EK-00 for categories-list@mta.ca; Wed, 05 Feb 2003 11:37:25 -0400 Message-ID: <3E3F849F.5080704@kestrel.edu> Date: Tue, 04 Feb 2003 01:15:11 -0800 From: Dusko Pavlovic X-Accept-Language: en-us, en MIME-Version: 1.0 To: CATEGORIES mailing list Subject: categories: Re: Cauchy completeness of Cauchy reals References: <3E36ED4F.4070807@kestrel> <1043829334.3e37925619e77@mail.inf.ed.ac.uk> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 15 (not sure whether i shouldn't let this thread die, since i didn't read mail for a week, and we all have things to do. but it's not like this list is filling anyone's mailbox with megabytes of usolicited research problems, and it seems a couple more dekabytes on cauchy reals might be useful.) Alex Simpson wrote: >> |cb(x)i - cb(y)i| <= [... calculation omitted ...] >> <= 1/2^i >> >>means that cb(x)i and cb(y)i have the first i digits equal. >> >I don't see that cb(x)i and cb(y)i have the first i digits equal. > i stand corrected (as they say). >>now, as everyone has been pointing out, the dyadic representation >>depends on markov's principle. >> > >This is *not* what has been pointed out (whatever you mean >by dyadic representation). > >What I previously pointed out was that the existence of >ordinary binary representations may fail even in the presence >of Markov's principle. > dyadic numbers are rationals in the form p/2^n. (google helps with such things.) the intuition that dyadic approximation has to do with markov's principle is supported by the fact that markov's principle is equivalent with the statement >>that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k >>s.t. 1/2^k < e. this is *equivalent* to markov's principle. >> > >The property quoted is in fact a trivial consequence of intuitionistic >arithmetic alone. It has nothing to do with Markov's principle. > for a real number e, i am pretty sure that the above is equivalent with markov's principle. it must be in books, but i think you can't miss the proof if you try. *however* you are right that in my "construction", it is used in a wrong place, for a rational number, and k exists trivially. >Such an f is tantamount to giving a splitting to the epi > > r: {x: Q^N | x a Cauchy sequence} --> I_C > >where I_C is the Cauchy interval. There are many toposes >in which Q^N is basically Baire space and I_C is basically >the closed unit interval in Euclidean space >Furthermore, >in many such toposes (e.g. Johnstone's), countable >choice and Markov's principle both hold. > splitting r is only the strongest sense of finding the canonical representatives, not the only one. r may not split by a topos morphism, but the canonical representatives can be found externally, and suffice for a completeness proof. after all, if i remember correctly, such is the situation with markov's principle itself: for a decidable P, * heyting arithmetic does not validate |- ~forall x. P(x) -> exists x.~ P(x) * but if |-~foral x. P(x) can be derived, then |- exists x.~P(x) can be derived. in particular, if i can prove that not all numbers in a binary stream are 0, then i can extract the first 1 from that proof, although that proof transformation cannot be internalized as a recursive function, to realize the implication. all this is, of course, just more intuitive support for the idea that i have been trying out, that *dyadic approximations might yield representatives of cauchy sequences, and since they are a coalgebra, help with their completeness*. i know that it is probably a wrong idea, but it also feels wrong to me to settle with incomplete cauchy reals. i'd like to understand why in the world would toposes deviate from cantor's idea of continuum, so pervasive in everyday math? -- dusko From rrosebru@mta.ca Wed Feb 5 11:38:37 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 11:38:37 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gRcl-0003II-00 for categories-list@mta.ca; Wed, 05 Feb 2003 11:38:07 -0400 Message-Id: <5.2.0.9.2.20030204143821.009e1b20@mail.netropolis.net> X-Sender: xtalv1@mail.netropolis.net X-Mailer: QUALCOMM Windows Eudora Version 5.2.0.9 Date: Tue, 04 Feb 2003 14:48:30 -0500 To: categories@mta.ca From: "Ellis D. Cooper, Ph.D." Subject: categories: Mentamatics: Books and Stories, a movie book by Ellis D. Cooper Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 16 Dear category theorists - In one sense my movie book pays homage to the patient categoristes who tolerated my limitations as a student of mathematics. I sure would like to know if I am on to something with my category of abstract computers and translators as a context for explaining virtual machinery. Below is the formal announcement. Ellis D. Cooper ---------------------------- I will not send more e-mails to you unless specifically authorized to do so via the e-mail link on the web site announced below. Just place the word YES in the Subject line of your e-mail. From the outside, The FORM of Mentamatics: Books and Stories at http://www.mentamatics.com is like a book of short movies. From the inside, The CONTENT centers on my interests in mathematics, engineering, and philosophy. It is an autobiographical video tutorial and report on research. The audience for this FORM is the set of all Educators. Philosophers, Mathematicians, Computer Scientists, and Engineers may value the CONTENT. There is a set of stories and tutorials about Stephen Wolfram's "new kind of science," allocating it a niche in a new structure called Virtuality. Timing machines populate this vast space. These encompass both the discrete and continuous realms of machinery, that is, hybrid systems. Towers of virtual machines grounded in physical systems implement higher level machines. From the inside, the purpose is to entertain, to report on my scientific research, and to raise money for continuing it. However, from the outside, the main purpose of the web site is to demonstrate one way Educators may do more for students.* So, please contact me at XTALV1@NETROPOLIS.NET on how I can help teachers and educational institutions use this FORM to deliver personalized tutorial CONTENT over the Web or on CD or DVD. *Technology demonstrated includes the following. Quicktime: panorama with hotspots, video with timed events, audio-only, screen-capture video, image slideshow; mathematical animation, animated GIF; digital conversion of analog video; HTML popup windows and frames. , From rrosebru@mta.ca Mon Feb 10 14:21:06 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 10 Feb 2003 14:21:06 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18iIUv-0000oR-00 for categories-list@mta.ca; Mon, 10 Feb 2003 14:17:41 -0400 Date: Mon, 10 Feb 2003 10:14:25 -0800 From: Vaughan Pratt Message-Id: <200302101814.KAA16416@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Topological spaces are ? frames Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 17 I'm looking for a better adjective than "eclectic" to use in the equation, "Topological spaces are ?eclectic? frames." "Lax" would be good but for its extant 2-cell connotations. "Relaxed", "mellow" (suggested at an FMCS in Calgary some years ago for tensor products not required to have a right adjoint in either argument), and "laid-back" come to mind. (These tension types were to my generation as snow types are rumored to be to Eskimos.) If someone has already coined an adjective for this purpose, I'll go with that. Otherwise I'll take all recommendations and justifications into consideration. Context: Since comonoids in chu_2 are to biCPOs much as topological spaces are to frames, I'd like to use the same adjective in the analogous equation "Comonoids in chu_2 are ?eclectic? biCPOs." (A biCPO is a CPO whose order dual is also a CPO---does that have a better name btw? The category chu_2 consists of the biextensional (left-separable and right-separable) dyadic (over {0,1}) Chu spaces.) Fran=E7ois Lamarche's casuistries, about which he spoke at the Barrfest, be= ar on this. Any recent news on casuistries? Fran=E7ois? Anyone else working on comonoids in chu_2? That is, besides the team at theory-edge that has spent the last 10 days attacking "Is every T1 comonoid in chu_2 discrete?" for $500, raised to $1000 on Friday, see correspondence starting at http://groups.yahoo.com/group/theory-edge/messages/6957 The puzzle home itself is on Dominic Hughes' machine Thue as http://thue.stanford.edu/puzzle.html I'll settle on the adjective on Feb. 26 (CMCS submission deadline). Vaughan Pratt From rrosebru@mta.ca Tue Feb 11 12:25:01 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Feb 2003 12:25:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18id9d-0004pg-00 for categories-list@mta.ca; Tue, 11 Feb 2003 12:21:05 -0400 X-Sender: grandis@pop4.dima.unige.it Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Tue, 11 Feb 2003 16:54:04 +0100 To: categories@mta.ca From: grandis@dima.unige.it (Marco Grandis) Subject: categories: Preprint: JORDAN-HOLDER, MODULARITY AND DISTRIBUTIVITY IN NON-COMMUTATIVE ALGEBRA X-OriginalArrivalTime: 11 Feb 2003 15:49:07.0718 (UTC) FILETIME=[1C972A60:01C2D1E5] Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 18 The following preprint is available: F. Borceux - M. Grandis JORDAN-HOLDER, MODULARITY AND DISTRIBUTIVITY IN NON-COMMUTATIVE ALGEBRA Dip. Mat. Univ. Genova, Preprint 474 (Feb 2003), 34 p. Abstract. A study of lattices of subgroups or subrings adequate for non-commutative homological algebra can be pursued in a setting of *weakly exact* categories. These extend the Puppe-exact ones and the semiabelian ones, and are essentially based on a notion of *gamma-category* introduced by Burgin. In this context, subobjects form *w-modular w-lattices*, equipped with a normality relation. The free w-modular w-lattice generated by two chains with normality conditions is determined and proved to be *weakly distributive*, by a construction inspired by the well-known Birkoff theorem for free modular lattices. We show that this theorem is relevant for the study of double filtrations, much in the same way as the Birkoff theorem in the commutative case; similarly, it should be of use in the study of spectral sequences. Available in dvi and ps: http://www.dima.unige.it/~grandis/BGwe.dvi http://www.dima.unige.it/~grandis/BGwe.ps ________ The interested reader can also download the following preprint on w-exact categories: M. Grandis Weakly exact categories and their relations, December 2002. [Slightly revised version of: Weakly exact categories and their relations, Dip. Mat. Univ. Genova 20 (1987)]. Available in ps: http://www.dima.unige.it/~grandis/wEx.ps ________ Marco Grandis Dipartimento di Matematica Universita' di Genova via Dodecaneso 35 16146 GENOVA, Italy e-mail: grandis@dima.unige.it tel: +39.010.353 6805 fax: +39.010.353 6752 http://www.dima.unige.it/~grandis/ From rrosebru@mta.ca Tue Feb 11 12:25:01 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Feb 2003 12:25:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18id8G-0004gL-00 for categories-list@mta.ca; Tue, 11 Feb 2003 12:19:40 -0400 Message-ID: <001401c2d1c2$fc3c3520$50c2bc93@acws0090> From: "Steve vickers" To: References: <200302101814.KAA16416@coraki.Stanford.EDU> Subject: categories: Re: Topological spaces are ? frames Date: Tue, 11 Feb 2003 11:44:49 -0000 MIME-Version: 1.0 Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 6.00.2600.0000 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2600.0000 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 19 > I'm looking for a better adjective than "eclectic" to use in the equation, > "Topological spaces are ?eclectic? frames." "Lax" would be good but for > its extant 2-cell connotations. "Relaxed", "mellow" (suggested at an FMCS > in Calgary some years ago for tensor products not required to have a right > adjoint in either argument), and "laid-back" come to mind. (These tension > types were to my generation as snow types are rumored to be to Eskimos.) The spaces closest to frames are sober, and the wayward ones are drunkard frames. Though in practice one might euphemistically call them "relaxed" or "mellow" out of kindness. Steve Vickers From rrosebru@mta.ca Tue Feb 11 15:46:20 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 11 Feb 2003 15:46:20 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18igKE-0006WR-00 for categories-list@mta.ca; Tue, 11 Feb 2003 15:44:14 -0400 Date: Tue, 11 Feb 2003 17:19:39 +0100 Message-Id: <200302111619.RAA27727@ns.lami.univ-evry.fr> To: categories@mta.ca From: "RULE'03 workshop" Reply-To: giavitto@lami.univ-evry.fr Subject: categories: CFP for RULE 2003 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 20 ********************************************************** *** RULE 2003: RPD workshop *** *** JUNE, 9, 2003 *** *** Valencia, Spain *** *** *** *** http://www.dsic.upv.es/~rdp03/rule/ *** ********************************************************** Scope: ------ The rule-based programming paradigm is characterized by the repeated, localized transformation of a shared data object such as a term, graph, proof, or constraint store. The transformations are described by rules which separate the description of the sub-object to be replaced (the pattern) from the calculation of the replacement. Optionally, rules can have further conditions that restrict their applicability. The transformations are controlled by explicit or implicit strategies. The basic concepts of rule-based programming appear throughout computer science, from theoretical foundations to practical implementations. Term rewriting is used in semantics in order to describe the meaning of programming languages, as well as in the implementation of program transformation systems. It is used implicitly or explicitly to perform computations, e.g., in Mathematica, OBJ, or ELAN, or to perform deductions, e.g., by using inference rules to describe or implement a logic, theorem prover or constraint solver. Extreme examples of rule-based programming include the mail system in Unix which uses rules in order to rewrite mail addresses to canonical forms, or the transition rules used in model checkers. Rule-based programming is currently experiencing a renewed period of growth with the emergence of new concepts and systems that allow a better understanding and better usability. On the theoretical side, after the in-depth study of rewriting concepts during the eighties, the nineties saw the emergence of the general concepts of rewriting logic and of the rewriting calculus. On the practical side, new languages such as ASM, ASF+SDF, BURG, Claire, ELAN, Maude, and Stratego, new systems such as LRR and commercial products such as Ilog Rules and Eclipse have shown that rules are a useful programming tool. The practical application of rule-based programming prompts research into the algorithmic complexity and optimization of rule-based programs as well as into the expressivity, semantics and implementation of rules-based languages. The purpose of this workshop is to bring together researchers from the various communities working on rule-based programming to foster fertilisation between theory and practice, as well as to favour the growth of this programming paradigm. We solicit original papers on all topics of rule-based programming, including but not restricted to * Languages for rule-based programming o Expressivity o Semantics o Implementation techniques * Applications of rule-based programming o Analysis of rule-based programs o Programming methods * Environments for rule-based programming o (Partial) Evaluation o Abstract machines for rewriting * Combination of rule-based programming with other paradigms * System descriptions Submission procedure and publication: ------------------------------------- Submission process will be open in April 2003. Papers (of at most 15 pages) should be submitted electronically as PostScript or PDF files to one of the program committee chairs: Jean-Louis Giavitto (giavitto@lami.univ-evry.fr) or Pierre-Etienne Moreau (Pierre-Etienne.Moreau@loria.fr). The message should also contain a text-only abstract and author information. Accepted papers will be published and available during the workshop. After revision, final copies of the accepted papers will be published in Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier Science. This will be confirmed in the second call for papers. Program committee co-chairs: ---------------------------- Jean-Louis Giavitto, Evry Val d'Essone University, France Pierre-Etienne Moreau, LORIA-INRIA Nancy, France Program Committee members: -------------------------- James Cordy, Queen's University at Kingston, Canada Olivier Danvy, BRICS, Denmark Steven Eker, SRI International, USA Thom Fruehwirth, Ulm University, Germany Berthold Hoffmann, Bremen University, Germany Herbert Kuchen, Muenster University, Germany Oege de Moor, Oxford University Computing Laboratory, England Przemek Prusinkiewicz, Calgary University, Canada Patrick Viry, ILOG, France ----------------------------------------------------------------------- IMPORTANT DATES ----------------------------------------------------------------------- April 6th 2003 Submission of full paper May 5th 2003 Notification May 14th 2003 Final version due June 9th 2003 RULE 2003 From rrosebru@mta.ca Wed Feb 12 11:25:26 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Feb 2003 11:25:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18iyev-0002VV-00 for categories-list@mta.ca; Wed, 12 Feb 2003 11:18:49 -0400 Message-Id: <200302112134.h1BLYiMQ026698@imgw1.cpsc.ucalgary.ca> Date: Tue, 11 Feb 2003 14:34:44 -0700 (MST) From: Robin Cockett Reply-To: robin@cpsc.ucalgary.ca Subject: categories: FMCS 2003: preliminary announcement (call for abstracts and participation) To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii X-Virus-Scanned: by amavis-milter (http://amavis.org/) X-Spam-Status: No, hits=3.7 required=7.3 X-Spam-Level: *** Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 21 A preliminary announcement for FMCS 2003: __________________________________________________________ FFFFFFF M M CCC SSS F MM MM C S FFFFF M MM M C SSS F M M C S F M M CCC SSS 2003 (OTTAWA) _________________________________________________________ CHANGE OF VENUE: Please note that this year's meeting on Foundational Methods in Computer Science (FMCS 2003) will be hosted by the Logic Group at the University of Ottawa, May 30th -- June 1st. The change in venue is to allow participants to take advantage of the "Theoretical Computer Science Month" supported by the Field's institute leading up to the LICS meeting in Ottawa. It is planned to hold next years meeting in the Kananaskis (Alberta) .. __________________________________________________________ FOUNDATIONAL METHODS IN COMPUTER SCIENCE The workshop is an informal meeting to bring together researchers in mathematics and computer science with a focus on the applications of category theory in computer science. It is a three day meeting, which starts with a day of tutorials (Friday 30th May) aimed at students and newcomers to category theory, followed by a days and a half of research talks (Saturday, 1st June and Sunday, 2nd June). There will be a series of invited presentations (TBA). The remaining research talks are solicited from the participants. If you wish to give a talk please let us know by sending an abstract and title to Robin Cockett or Richard Blute (see e-mail address below) before the beginning of May. Student participation at FMCS is particularly encouraged. There are limited funds to provide support for students who wish to attend the workshop (see below). __________________________________________________________ Support for graduate students: __________________________________________________________ We particularly encourage graduate students to attend FMCS and to present their work. If you wish to give a presentation at FMCS you should send a title and a brief abstract to Robin Cockett (robin@cpsc.ucalgary.ca). We would like to receive these abstracts before beginning of May so that we can arrange the schedule before the meeting itself. Some limited funding is available to support graduate students who wish to attend the summer school and/or FMCS. To apply for this money, you should contact Richard Blute (rblute@mathstat.uottawa.ca) 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 who wish to attend FMCS and intend to stay to attend the Fields Summer School. Applications should be made as soon as possible before the beginning of March. __________________________________________________________ Organizer: Robin Cockett (robin@cpsc.ucalgary.ca) Local organizer: Richard Blute (rblute@cpsc.ucalgary.ca) From rrosebru@mta.ca Wed Feb 12 11:25:26 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Feb 2003 11:25:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18iyfd-0002Yp-00 for categories-list@mta.ca; Wed, 12 Feb 2003 11:19:33 -0400 Message-ID: <20030211214817.55877.qmail@web12203.mail.yahoo.com> Date: Tue, 11 Feb 2003 13:48:17 -0800 (PST) From: Galchin Vasili Subject: categories: Category of Heyting Algebras To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 22 Hello, I have some questions about the category whose objects are Heyting algebras and whose arrows are Heyting algebra homomorphims. 1) Does this category possess a subobject classifier? 2) Is this category a CCC? 3) Is this category a topos? It would really be neat if 3) was true because of all kinds of self-reference or infinite regression, e.g. it's Omega would be an internal Heyting algebra, but my guess is "no" to all three. Regards, Bill Halchin From rrosebru@mta.ca Wed Feb 12 11:30:57 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Feb 2003 11:30:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18iyou-0003O7-00 for categories-list@mta.ca; Wed, 12 Feb 2003 11:29:08 -0400 From: John Longley To: categories@mta.ca Subject: categories: Re: Realizability and Partial Combinatory Algebras Message-ID: <1045047509.3e4a28d50d86b@mail.inf.ed.ac.uk> Date: Wed, 12 Feb 2003 10:58:29 +0000 (GMT) References: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 129.215.32.128 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 23 Peter Johnstone wrote: > However, the point I was trying to make was that the > construction of the quasitopos of A-valued assemblies, and the proof > that its effectivization is a topos, make no use whatever of the > condition that Sxy is always defined. As far as I can see, Peter Johnstone is essentially correct. Even without the condition "sxy is defined", Asm(A) is locally cartesian closed (though the correct construction of local exponentials is not quite the "obvious" one), and its exact/regular completion is a topos. Peter Lietz's argument (which is the one that occurred to me too) seems to fail at his point 1: to get a realizer for the mediating morphism from the true local exponential to the object he constructs, one actually needs the condition "sxy is defined". For the record, in Peter L's example, the true exponential m^m in the slice over Nabla(P(A)), for instance, may be described as follows: |T| = P(A) [|X \in T|] = {a | for all b \in X. akb \in X} (where k plays the role of an arbitrary element which forces the "thunked" operation X -> X to manifest itself.) I think I can now appreciate Peter Johnstone's point of view, though it seems to me that to follow it through consistently would require some substantial changes to the way one develops the whole theory. For instance, in defining the category Asm(A), one really ought to say e.g. that an element r \in A *tracks* f : X -> Y iff for all x \in X, a \in A. a \in [|x \in X|] => rka \in [|f(x) \in Y|] so as not to get mired down in case splits on whether X is inhabited, which (I humbly submit) are here an abomination and totally out of keeping with the spirit of realizability and topos theory in general. [Classically, of course, the above definition leads to exactly the same category as the usual one.] One can then do everything else in the same way, and it all works out - e.g. there is a perfectly respectable tripos over A (with Heyting implication defined as in the object T above), and the theory of internal categories such as PER also works fine. I don't think one can really call this "standard realizability" any more, in the sense of being derived from (a simple abstraction of) Kleene's realizability interpretation. Of course, one might say that doesn't matter much, but for my part, I feel one loses something of the directness of standard realizability, where application in the PCA corresponds immediately to function application in Asm(A) and also to Modus Ponens in the logic. There is also of course the evident analogy with the Brouwer-Heyting- Kolmogorov interpretation of intuitionistic logic. If one adopts the above alternative, there is less of a clear intuition about what the significance of application in the PCA is. However, no sooner has one reached this point, than one notices that doing realizability of the above kind over A is just tantamount to doing standard realizability over the "derived PCA" a la Freyd [?], where application is defined by a.b ~ akb. Indeed, one has the following easy proposition: For any PCA A (where we don't assume "sxy defined"), there is an applicatively equivalent PCA B (in the sense of my thesis) in which sxy is always defined. In particular, the realizability topos on A (constructed as outlined above) is equivalent to the (usual) standard realizability topos on B. Proof: Let B have the same set as A, and define application in B by a.b ~ akb. It's easy to construct K,S \in B such that K.a.b = a, S.a.b.c ~ a.c.(b.c), and with a little additional care one can arrange that S.a.b is always defined. Now, application in B is realized in A by \lambda ab. akb (constructed as normal); and application in A is realized in B by i=skk, since i.a.b = ikakb = kakb = ab. The equivalence of toposes can now most easily be seen by noticing that the categories Asm(A), Asm(B) are equal on the nose. So, it seems it's largely just a question of taste whether one adopts the definedness condition. For my money, I would rather adopt this condition, retain the directness of standard realizability and all the familiar constructions, do all the proofs in an "effective" spirit, and know that I'm not sacrificing any generality. Who could ask for anything more? (Quite a lot of the above was new to me, and was all good fun!) Finally, I'd like to remark briefly on the other issue in the definition of PCA, which Jaap, Peter L and myself have now all mentioned: whether one should require sxyz ~ xz(yz) or just sxyz >~ xz(yz). I know of no reason not to adopt the latter, more general condition, and it seems to me much more in the spirit of realizability: e.g. one never cares if a realizer for a morphism assemblies is defined on more elements than required. On the other hand, I do not have any particular use yet for any of the extra examples admitted by this definition. An interesting case in point is Kleene's second model, K_2. It is a PCA in the sense of the axiom with ~, but the "natural" construction of an element s gives one that only satisfies the axiom with >~. Some artificial hackery is needed to produce an element s satisfying the stronger axiom - and of course, my attitude would be: why bother? Best wishes, John From rrosebru@mta.ca Wed Feb 12 15:10:14 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Feb 2003 15:10:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18j2AR-00076n-00 for categories-list@mta.ca; Wed, 12 Feb 2003 15:03:35 -0400 Date: Wed, 12 Feb 2003 17:03:26 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Category of Heyting Algebras In-Reply-To: <20030211214817.55877.qmail@web12203.mail.yahoo.com> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18j0IB-0003ei-00*Vu274ehEKDo* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 24 On Tue, 11 Feb 2003, Galchin Vasili wrote: > > Hello, > > I have some questions about the category whose objects are Heyting > algebras and whose arrows are Heyting algebra homomorphims. > > 1) Does this category possess a subobject classifier? > > 2) Is this category a CCC? > > 3) Is this category a topos? > The category of Heyting algebras has no hope of being cartesian closed because its initial object (the free HA on one generator) is not strict initial. It doesn't have a subobject classifier either, because the theory of Heyting algebras doesn't have enough unary operations to satisfy the conditions of Theorem 1.3 in my paper "Collapsed Toposes and Cartesian Closed Varieties" (J. Algebra 129, 1990). On the other hand, the terminal object in the category of Heyting algebras is strict, which suggests that the dual of the category might come rather closer to being a topos (although, by an observation which I posted a couple of months ago, it can't have a subobject classifier). Indeed, the dual of (finitely-presented Heyting algebras) is remarkably well-behaved, as shown by Silvio Ghilardi and Marek Zawadowski ("A Sheaf Representation and Duality for Finitely Presented Heyting Algebras", J.Symbolic Logic 60, 1995): they identified a particular topos in which it embeds (non-fully, but conservatively) as a subcategory closed under finite limits, images and universal quantification. Peter Johnstone From rrosebru@mta.ca Wed Feb 12 15:10:14 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Feb 2003 15:10:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18j2Bo-0007D8-00 for categories-list@mta.ca; Wed, 12 Feb 2003 15:05:00 -0400 From: Robert McGrail To: categories@mta.ca Subject: categories: Re: Category of Heyting Algebras Date: Wed, 12 Feb 2003 12:20:09 -0500 User-Agent: KMail/1.4.1 References: <20030211214817.55877.qmail@web12203.mail.yahoo.com> In-Reply-To: <20030211214817.55877.qmail@web12203.mail.yahoo.com> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Message-Id: <200302121220.09792.mcgrail@bard.edu> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 25 On Tuesday 11 February 2003 16:48, you wrote: > Hello, > > I have some questions about the category whose objects are Heyting > algebras and whose arrows are Heyting algebra homomorphims. > > 1) Does this category possess a subobject classifier? > > 2) Is this category a CCC? Unless my definition of Heyting algebra is a bit off, I am sure that this (and hence 3) is false. I assume that in a Heyting algebra T does not equal F. This follows the intuitive introduction of Heyting algebras by Moerdijk/MacLane as capturing the algebraic structure of topologies. If that is not the case then disregard the rest of my message. Anyway, under these assumptions, the trivial HA {T,F} is both initial and final. Hence 0 = 1 (= means is iso to). Any CCC with 0 = 1 is trivial. I will leave the diagram chase to you but it can be summarized as follows. Let A be any HA. Then A = A^1 = A^0 = 1. Hope this helps, Bob McGrail > > 3) Is this category a topos? > > It would really be neat if 3) was true because of all kinds of > self-reference or infinite regression, e.g. it's Omega would be an > internal Heyting algebra, but my guess is "no" to all three. > > Regards, Bill Halchin From rrosebru@mta.ca Wed Feb 12 15:10:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 12 Feb 2003 15:10:15 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18j29T-00072e-00 for categories-list@mta.ca; Wed, 12 Feb 2003 15:02:35 -0400 Date: Wed, 12 Feb 2003 08:06:33 -0800 From: Vaughan Pratt Message-Id: <200302121606.IAA05541@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Slightly cheaper elephants? Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 26 Normally I click the "No thanks, just place my order" button at Amazon when asked whether I want to "Share the Love". This feature lets you supply a list of friends ahead of time whom you can email after your purchase of a book with the happy news that you've secured them a 10% discount on that book. I ignore this feature because it casts you in the role of Amazon salesperson and turns your friends into your clientele for as long as they remain on your euphemistically named "Amazon Friends list." At 10% I find this role downright embarrassing. Now if I could get my friends 100% discounts, or maybe even 50%, I'd have to reconsider this. I was just about to click the "No thanks" button on my preorder of Peter's "Sketches of an Elephant" when it occurred to me that a 10% discount on enough money to buy a house (ok a doll-house) was the monetary equivalent of a 50% or even 100% discount on a lesser tome. So this raises two questions. First, are other sources of "Elephant" at 17% or better off Amazon's $295.00 price available to us eager students of toposophy? (See below for why 17%, $245.50 to be precise, and not 10%.) And if not, is there anyone who'd been contemplating the purchase within the next week (Amazon's time limit) who'd like to be on my list, even if just temporarily for the sake of this one book, in order to be able to get it for the amazingly low price of $245.50? (Oh, that's the one I would have chosen, sir, just sign right here, and here, and here.) OUP presumably does the best off this deal, with Amazon next and me third if I end up with at least two "friends." (With only one "friend" the friend relationship may as well have been symmetric since each side gets 10% off, but that's still a 10% discount for each of two purchasers of the book. The only advantage of no "friends" is you get to keep all your real friends, but then no one gets a 10% discount that way.) One thing about this system that I find truly evil is that if 2n purchasers form n pairs in this way so that every purchaser winds up with a 10% discount on the book in question, this seemingly fairest of all arrangements turns out to be suboptimal for the purpose of extracting discounts from Amazon. The optimum is to elect a single salesperson, who buys the book at no discount, after which every purchase of that book within that week extracts 20% per book, half of which goes to the latest purchaser and the other half to the elected salesperson. With enough "friends" the salesperson who took the original risk makes out like a bandit! I propose to reverse this as follows. I'll buy my copy at $295.00. Anyone wanting to be my "Amazon friend for a week" can then get it at $265.50. To spare me the embarrassment of becoming a salesman I'll send you an Amazon gift certificate for $20 which further gets your price down to $245.50. I still clear $9.50 (if I haven't lost a decimal point somewhere like those Anderson guys did), which means that if three people join this cockamamie scheme (my gamble I guess) then I end up with close to the discount I'd have gotten with only one friend, but my friends then become real friends because I'm offering them $49.50 (16.7%) discounts on a book from Amazon. Or two such if they buy two copies. So, if anyone who was planning to postpone their doll-house purchase in favour of buying two copies, or even just one copy, of Peter's book on huge arches (ele arch, phant huge), please let me know and I'll add your name to my list. I will hold off on the actual purchase however until it is clear that everyone who wants to be in on this in anything like a reasonable time frame has joined, since the opportunity cost of splitting this arrangement into multiple weeks is $59.00 per split (proof by induction, with the base case being one purchaser, who gets no discount, whereas a second purchaser brings the total discount to $59.00). If you spot anything I've misinterpreted about Amazon's Share the Love scheme in the above, *please* let me know soon before this hole is dug too deep. Vaughan From rrosebru@mta.ca Thu Feb 13 14:52:31 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:52:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jOOy-0006bI-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:48:04 -0400 Date: Wed, 12 Feb 2003 21:22:45 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: Slightly cheaper elephants? In-Reply-To: <200302121606.IAA05541@coraki.Stanford.EDU> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18j4L8-0004vH-00*gtrAOA/LCro* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 27 Vaughan's message prompts me to pass on the information, received today, that the U.S. end of OUP has already sold out of copies of (at least) the second volume of the "Elephant", due to higher than expected sales. The U.K. end still has some copies, but they are just about to reprint, six months before they expected to do so. What implication (if any) this has for the availability of the book from Amazon, I have no idea. Peter Johnstone -------------- On Wed, 12 Feb 2003, Vaughan Pratt wrote: > Normally I click the "No thanks, just place my order" button at Amazon when > asked whether I want to "Share the Love". This feature lets you supply > a list of friends ahead of time whom you can email after your purchase > of a book with the happy news that you've secured them a 10% discount > on that book. I ignore this feature because it casts you in the role of > Amazon salesperson and turns your friends into your clientele for as long > as they remain on your euphemistically named "Amazon Friends list." At 10% > I find this role downright embarrassing. > > Now if I could get my friends 100% discounts, or maybe even 50%, I'd have > to reconsider this. I was just about to click the "No thanks" button on > my preorder of Peter's "Sketches of an Elephant" when it occurred to me > that a 10% discount on enough money to buy a house (ok a doll-house) was > the monetary equivalent of a 50% or even 100% discount on a lesser tome. > > So this raises two questions. First, are other sources of "Elephant" at > 17% or better off Amazon's $295.00 price available to us eager students > of toposophy? (See below for why 17%, $245.50 to be precise, and not 10%.) > And if not, is there anyone who'd been contemplating the purchase within > the next week (Amazon's time limit) who'd like to be on my list, even if > just temporarily for the sake of this one book, in order to be able to get > it for the amazingly low price of $245.50? (Oh, that's the one I would > have chosen, sir, just sign right here, and here, and here.) > > OUP presumably does the best off this deal, with Amazon next and me third if > I end up with at least two "friends." (With only one "friend" the friend > relationship may as well have been symmetric since each side gets 10% off, > but that's still a 10% discount for each of two purchasers of the book. > The only advantage of no "friends" is you get to keep all your real friends, > but then no one gets a 10% discount that way.) > > One thing about this system that I find truly evil is that if 2n purchasers > form n pairs in this way so that every purchaser winds up with a 10% discount > on the book in question, this seemingly fairest of all arrangements turns > out to be suboptimal for the purpose of extracting discounts from Amazon. > The optimum is to elect a single salesperson, who buys the book at no > discount, after which every purchase of that book within that week extracts > 20% per book, half of which goes to the latest purchaser and the other half > to the elected salesperson. With enough "friends" the salesperson who > took the original risk makes out like a bandit! > > I propose to reverse this as follows. I'll buy my copy at $295.00. Anyone > wanting to be my "Amazon friend for a week" can then get it at $265.50. > To spare me the embarrassment of becoming a salesman I'll send you an Amazon > gift certificate for $20 which further gets your price down to $245.50. > I still clear $9.50 (if I haven't lost a decimal point somewhere like those > Anderson guys did), which means that if three people join this cockamamie > scheme (my gamble I guess) then I end up with close to the discount I'd > have gotten with only one friend, but my friends then become real friends > because I'm offering them $49.50 (16.7%) discounts on a book from Amazon. > Or two such if they buy two copies. > > So, if anyone who was planning to postpone their doll-house purchase in > favour of buying two copies, or even just one copy, of Peter's book on huge > arches (ele arch, phant huge), please let me know and I'll add your name to > my list. I will hold off on the actual purchase however until it is clear > that everyone who wants to be in on this in anything like a reasonable time > frame has joined, since the opportunity cost of splitting this arrangement > into multiple weeks is $59.00 per split (proof by induction, with the base > case being one purchaser, who gets no discount, whereas a second purchaser > brings the total discount to $59.00). > > If you spot anything I've misinterpreted about Amazon's Share the Love scheme > in the above, *please* let me know soon before this hole is dug too deep. > > Vaughan > > > > From rrosebru@mta.ca Thu Feb 13 14:52:31 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:52:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jONN-0006Su-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:46:25 -0400 From: Thomas Streicher Message-Id: <200302121928.UAA01552@fb04209.mathematik.tu-darmstadt.de> Subject: categories: Re: Realizibility and Partial Combinatory Algebras In-Reply-To: <1044469182.3e4155bed0abd@mail.inf.ed.ac.uk> from John Longley at "Feb 5, 2003 06:19:42 pm" To: categories@mta.ca Date: Wed, 12 Feb 2003 20:28:14 +0100 (CET) X-Mailer: ELM [version 2.4ME+ PL66 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 28 John L. has recalled that the traditional definition of pca is motivated by functional completeness. > The somewhat mysterious definition of (partial or full) > combinatory algebras is really motivated by the fact that it > is equivalent to a "combinatory completeness" property, which is > a bit less mysterious but more cumbersome to state. Informally, > combinatory completeness says that all functions definable in the > language of A are themselves representable by elements of A. > More precisely: > > A is a PCA iff for every formal expression e (built up from > variables x,y_1,...,y_n and constants from A via juxtaposition), > there is a formal expression called (\lambda x.e), whose variables > are just y_1,...,y_n, such that > (\lambda x.e)[b_1/y_1,...,b_n/y_n] is defined for all b_1,...,b_n \in A, > (\lambda x.e) a [b_1/y_1,...,b_n/y_n] ~ e[a/x,b_1/y_1,...,b_n/y_n] He also has pointed out that in realizability one always may replace a realizer by one which is defined for more arguments. Thus, it appears as natural to weaken the notion of functional completeness to the following "asymmetric" variant: for every formal expression e (built up from variables x,y_1,...,y_n and constants from A via juxtaposition), there is a formal expression called (\lambda x.e), whose variables are just y_1,...,y_n, such that for all a, b_1,...,b_n in A (\lambda x.e) a [b_1/y_1,...,b_n/y_n] = e[a/x,b_1/y_1,...,b_n/y_n] whenever the right hand side is defined Certainly, this assymmetric version of functional completeness ensures the existence of a k (with the usual properties) and an s in A with the property that (*) sabc = ac(bc) whenever ac(bc) is defined Obviously, from a k and an s satisfying (*) one can prove the assymmetric version of functional completeness. Axiom (*) doesn't even exclude undefinedness of sa (if a.x undefined for all x in A). Probably, such very weak pca's are also equivalent to an ordinary one? In any case the notion of pca is somewhat intensional in character. As we know Asm(A) and Asm(A') are equivalent iff their categories of modest projectives are equivalent. Concretely, for a pca A the category MP(A) of modest projectives is nothing but the category of subsets of A and maps f : P -> Q such that for some r in A we have ra = f(a) for all a in P. Of course, we know from John L.'s work that MP(A) and MP(A') are equivalent iff A and A' are applicatively equivalent. What, alas, is not known is an intrinsic categorical characterisation of those categories equivalent to MP(A) for some pca A. If we had such a characterisation we would have arrived at a categorical characterisation of categories of assemblies and, this, also of realizability toposes. Thomas From rrosebru@mta.ca Thu Feb 13 14:52:31 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:52:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jONv-0006WD-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:46:59 -0400 Date: Wed, 12 Feb 2003 11:31:57 -0800 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: Category of Heyting Algebras Message-ID: <20030212193157.GB19717@math-rs-n01.ucr.edu> References: <20030211214817.55877.qmail@web12203.mail.yahoo.com> <200302121220.09792.mcgrail@bard.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <200302121220.09792.mcgrail@bard.edu> User-Agent: Mutt/1.4i Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 29 Robert McGrail wrote: >I assume that in a Heyting algebra T does not equal F. >This follows the intuitive introduction of Heyting algebras by >Moerdijk/MacLane as capturing the algebraic structure of topologies. Probably there are people that put this in the definition -- the same people that require 0 != 1 in any ring, or that a topological space not be empty, or (for that matter) that a CCC not be trivial. But if you're not one of those people, then the Heyting algebra {*} captures the algebraic structure of the (unique topology on the) empty space. >Anyway, under these assumptions, the trivial HA {T,F} is both initial and >final. So with my definition, {T,F} is initial but {*} is final. But even with yours, I don't believe that {T,F} becomes final. There are 2 homomorphisms to it from the power set of {T,F} (as a Boolean algebra, which is a special kind of Heyting algebra). I don't think that your category has a final object (any more than the category of nontrivial rings does, nor the category of nonempty spaces has an initial object). -- Toby From rrosebru@mta.ca Thu Feb 13 14:52:31 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:52:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jOOP-0006Ym-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:47:29 -0400 From: Robert McGrail Organization: \sBard College To: categories@mta.ca Subject: categories: Oops Date: Wed, 12 Feb 2003 14:49:05 -0500 User-Agent: KMail/1.4.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Message-Id: <200302121449.05496.mcgrail@bard.edu> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 30 Though my conclusion is consistent with Peter Johnstone's, I am now convinced that my chain of proof is nonsense. Of course, you should be paying attention to Peter's response, rather than mine, anyway so shame on anyone who noticed :-) Bob McGrail From rrosebru@mta.ca Thu Feb 13 14:55:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:55:15 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jOTp-00071L-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:53:05 -0400 Date: Thu, 13 Feb 2003 18:34:40 +0100 (CET) From: Peter Lietz To: categories Subject: categories: Re: Realizability and Partial Combinatory Algebras In-Reply-To: <1045047509.3e4a28d50d86b@mail.inf.ed.ac.uk> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 31 Dear John, would you please fill me in on either (or better yet, both) of the following points, as I failed to figure them out by myself: 1.) Let A be a c-pca. If I understand correctly, you say that the indexed poset that maps a set I to the set of maps from I to P(A), endowed with the usual entailment relation [ for phi,psi: I -> P(A), phi |- psi iff there is an r in A such that for all i in I and for all a in phi(i), ra exists and ra is in psi(i) ] is indeed an indexed Heyting-Algebra and that the implication of phi,psi : I -> P(A) is given by (phi=>psi)(i) = {r in A | forall a in phi(i). rka in psi(i)}. My question is: given phi, psi and theta such that theta /\ phi |- psi over I via some realizer r, what would be a realizer witnessing theta |- phi => psi with => defined in the way you indicated? 2.) Given a c-pca A, you say that A equipped with the application function a.b := akb is a (proper) pca. What exactly would be a good S combinator for the new algebra ? (You wrote that some additional care is needed to construct S) Many thanks in advance, Peter ps: in an attempt to give the shortest possible of the many reasons, why Heyting algebras do not form a CCC I suggest: The one-element poset is the terminal Heyting algebra. Therefore, every object has at most one global section. Hence, there can only be one morphism between each two Heyting algebras, as the global sections of the exponent correspond to the morphisms (which is absurd). pps: The one-element poset *is* a Heyting-algebra, in fact all topologies are. On Wed, 12 Feb 2003, John Longley wrote: > As far as I can see, Peter Johnstone is essentially correct. > Even without the condition "sxy is defined", Asm(A) is locally cartesian > closed (though the correct construction of local exponentials is not quite > the "obvious" one), and its exact/regular completion is a topos. Peter > Lietz's argument (which is the one that occurred to me too) seems to fail > at his point 1: to get a realizer for the mediating morphism from the > true local exponential to the object he constructs, one actually needs > the condition "sxy is defined". For the record, in Peter L's example, > the true exponential m^m in the slice over Nabla(P(A)), for instance, .... From rrosebru@mta.ca Fri Feb 14 10:12:57 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 14 Feb 2003 10:12:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jgU9-00024i-00 for categories-list@mta.ca; Fri, 14 Feb 2003 10:06:37 -0400 Message-Id: <200302131312.h1DDCxv12769@mendieta.science.uva.nl> Date: Thu, 13 Feb 2003 14:12:59 +0100 X-Organisation: Faculty of Science, University of Amsterdam, The Netherlands X-URL: http://www.science.uva.nl/ From: info@folli.org To: categories@mta.ca Subject: categories: Beth Dissertation Prize 2003: Call for Nominations Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 32 [ We apologise if you receive this message more than once ] The European Association for Logic, Language and Information http://www.folli.org E. W. BETH DISSERTATION PRIZE 2003: CALL FOR NOMINATIONS Nominations are invited for the E. W. Beth Dissertation Prize awarded by the European Association for Logic, Language and Information to outstanding dissertations in the fields of Logic, Language and Information. The prize will be awarded to the best dissertation which resulted in a PhD in the year 2002. The dissertations will be judged on the impact they made in their respective fields, breadth and originality of the work, and also on the interdisciplinarity of the work. Ideally the winning dissertation will be of interest to researchers in all three fields. -- Who qualifies? -- Those who were awarded the PhD degree in the area of Logic, Language and Information between the 1st of January, 2002 and the 31st of December, 2002. There is no restriction on the nationality of the candidate or the university where the PhD was granted. However, after a careful consideration, FoLLI has decided to accept only dissertations written in English. -- How to submit? -- We only accept electronic submissions. The following documents are required: 1. the thesis in pdf or ps format (doc/rtf not accepted). 2. a ten page abstract of the dissertation in ascii format. 3. a letter of nomination from the thesis supervisor. Self-nominations are not possible; each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was awarded. 4. Two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree. All documents must be submitted electronically to beth_award@cs.nott.ac.uk . Hard copy submissions are not possible. If you experience any problems with the email submission or do not receive a notification from us within two working days, please write to beth_award@cs.nott.ac.uk or nza@cs.nott.ac.uk . -- Important dates: -- Deadline for Submissions: 28 February 2003 Notification of Decision: 1 June 2003 The prize will be handed to the winners at the European Summer School in Logic, Language and Information in Vienna (Austria), 18 - 29 August 2003. Prize winners will be expected to attend the ceremony; funding to make this possible is currently being secured. From rrosebru@mta.ca Fri Feb 14 12:28:03 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 14 Feb 2003 12:28:03 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jieZ-0005KB-00 for categories-list@mta.ca; Fri, 14 Feb 2003 12:25:31 -0400 Message-Id: <200302141548.h1EFmPn07526@famaf.unc.edu.ar> Date: Fri, 14 Feb 2003 18:48:25 +0300 (GMT) From: WAIT 2003 Reply-To: WAIT 2003 Subject: categories: CFP: WAIT 2003 To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii Content-MD5: xVbLJLpVrFhvpuAyuHMdiA== X-Mailer: dtmail 1.3.0 @(#)CDE Version 1.3.5 SunOS 5.7 sun4u sparc Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 33 ---------------------------------------------------------------------- CALL FOR PAPERS 32 JAIIO - WAIT 2003 Argentinian Workshop on Theoretical Computer Science Buenos Aires - Argentina September 1-5, 2003 ---------------------------------------------------------------------- The Argentinian Workshop on Theoretical Computer Science (WAIT) has become an important Latin American forum for the exchange of ideas and the presentation of research in theoretical computer science and its applications. The workshop aims are to build a bridge between academic and applied research and to stimulate the exchange of ideas and experience between theory and practise in computer science. The meeting includes contributed and invited talks, and tutorials. Further, we are very pleased to announce that there will be a special issue of ENTCS (http://www.elsevier.nl/locate/entcs) dedicated to WAIT 2003 publishing a selection of outstanding contributions. WAIT 2003 (http://wait2003.famaf.unc.edu.ar), the 7-th workshop in the series, will be held in Buenos Aires during September 1-5 (2003) as part of the 32-nd Argentinian Conference on Informatics and Operations Research (32 JAIIO, http://www.jaiio2003.uade.edu.ar). Buenos Aires (http://www.buenosaires.gov.ar/areas/turismo/en/) is a cosmopolitan and modern urban centre easily accessible by plane from most mayor cities in the world. The city is characterised by the multiplicity of its artistic expressions, ranging from the great assortment of sculptures and monuments to streets and corners that surprise with their allegorical reliefs and murals. The climate of Buenos Aires ---oceanic and warm--- is mild all year round, allowing visitors to discover the city on foot in any season. The city offers all categories of accommodation, and food ---which is something of a cult--- is of high quality. TOPICS Submissions are welcome in all fields of Theoretical Computer Science. Specific topics of WAIT 2003 include (but are not limited to): * Logical and algebraic foundations of computer science (logics for computation, category theory, relation algebras, type theory); * Formal methods (formal specification of sequential and concurrent programs, analysis, verification and transformation of programs, model checking); * Algorithms and data structures (sequential, parallel, distributed and on-line computing, probabilistic algorithms); * Automata theory and computational complexity; * Symbolic and algebraic computation; * Quantum Computing; * Bioinformatics. Submissions are expected to contain original research and will be refereed by international experts. Research papers must contain previously unpublished results. They will be judged on the base of originality and importance of their contributions and clarity of presentation. Papers should not exceed 12 pages, including figures and references. PROGRAM COMMITTEE: Martin Abadi (University of California at Santa Cruz) Gilles Barthe (INRIA Sophia-Antipolis) Gabriel Baum (Universidad de La Plata) Veronica Becher (Universidad de Buenos Aires) Vincent Danos (CNRS, Paris VII) Peter Dybjer (University of Gothenburg) Roberto Di Cosmo (PPS, Paris VII) Esteban Feuerstein (Universidad de Buenos Aires) Marcelo Fiore (Cambridge University) (co-chair) Daniel Fridlender (Universidad de Cordoba) (co-chair) Joos Heintz (Universidad de Buenos Aires) Gonzalo Navarro (Universidad de Chile) Peter O'Hearn (QMW, University of London) Alfredo Viola (Universidad de la Republica) IMPORTANT DATES: Deadline for reception of papers.................................May 4 Notification of acceptance.....................................June 27 Deadline for reception of the final version....................July 18 INSTRUCTIONS FOR AUTHORS: To facilitate the dissemination of papers and results, authors are invited to submit their papers in English. However, papers in Spanish or Portuguese are also welcome. Accepted contributions will be published in the Proceedings of the 32 JAIIO. Further, a selection of outstanding contributions will be invited to be published (in English) in a special issue of ENTCS dedicated to WAIT 2003. Papers should respond to ENTCS format (obtainable from http://math.tulane.edu/~entcs/) or similar, and must be submitted electronically in PostScript format (ghostview-readable) or PDF to the following e-mail address: wait2003@famaf.unc.edu.ar. Authors should communicate in a separate e-mail (in ASCII format) the title of the paper together with a short abstract, name and affiliation of all co-authors and their e-mail addresses, phone and FAX numbers. The message should also contain a list of keywords describing the area of the paper. ---------------------------------------------------------------------- From rrosebru@mta.ca Fri Feb 14 12:32:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 14 Feb 2003 12:32:15 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jijd-0005o4-00 for categories-list@mta.ca; Fri, 14 Feb 2003 12:30:45 -0400 Message-Id: <200302140332.h1E3WAMQ026782@imgw1.cpsc.ucalgary.ca> Date: Thu, 13 Feb 2003 20:32:10 -0700 (MST) From: Robin Cockett Subject: categories: Re: Category of Heyting Algebras To: categories@mta.ca In-Reply-To: MIME-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii X-Virus-Scanned: by amavis-milter (http://amavis.org/) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 34 Further to Peter's remark that the opposite of the category finitely presented Heyting algebras is rather nice ... one particular sense in which it is nice is that it is a lextensive category! So -- to seemingly contradict Peter :-) -- it does have a partial map classifier (but of course not for all monics)! The fact that it is a lextensive category can be obtained, by checking some Heyting algebra identities, from "Conditional Control is not quite Categorical Control" IV Higher Order Workshop, Banff 1990, Workshops in Computing (Springer-Verlag) 190-217 (1991) where the general question of when the opposite of an algebraic theory is extensive is answered. Any extensive category can be fully and faithfully embedded in a topos so as to preserve sums and limits ... so the ability to embed the opposite of Heyting algebra "nicely" into a topos can also be read from these results. -robin P.S.Whether this embedding has the other logical properties mentioned is, of course, another question ... On 12 Feb, Prof. Peter Johnstone wrote: > On Tue, 11 Feb 2003, Galchin Vasili wrote: > >> I have some questions about the category whose objects are Heyting >> algebras and whose arrows are Heyting algebra homomorphims. >> > > The category of Heyting algebras has no hope of being cartesian closed > because its initial object (the free HA on one generator) is not > strict initial. It doesn't have a subobject classifier either, because > the theory of Heyting algebras doesn't have enough unary operations > to satisfy the conditions of Theorem 1.3 in my paper "Collapsed > Toposes and Cartesian Closed Varieties" (J. Algebra 129, 1990). > > On the other hand, the terminal object in the category of Heyting > algebras is strict, which suggests that the dual of the category > might come rather closer to being a topos (although, by an observation > which I posted a couple of months ago, it can't have a subobject > classifier). Indeed, the dual of (finitely-presented Heyting > algebras) is remarkably well-behaved, as shown by Silvio Ghilardi > and Marek Zawadowski ("A Sheaf Representation and Duality for > Finitely Presented Heyting Algebras", J.Symbolic Logic 60, 1995): > they identified a particular topos in which it embeds (non-fully, > but conservatively) as a subcategory closed under finite limits, > images and universal quantification. > > Peter Johnstone > > > > From rrosebru@mta.ca Sat Feb 15 09:31:47 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 15 Feb 2003 09:31:47 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18k2Mg-00030Z-00 for categories-list@mta.ca; Sat, 15 Feb 2003 09:28:22 -0400 Message-ID: <20030215013412.22156.qmail@web12208.mail.yahoo.com> Date: Fri, 14 Feb 2003 17:34:12 -0800 (PST) From: Galchin Vasili Subject: categories: Topos ... working through a concrete example ... irreflexive graphs To: categories@mta.ca 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: 35 Hello, I am taking as my concrete topos the category of irreflexive graphs. >From William Lawvere's book (and many other sources), I know what the subobject classifier looks like, i.e. what graph is the subobject classifier. I haven't worked out the internal Heyting algebra Omega yet, but Hom[1, Omega] consists of three arrows, yes? (Sorry I know the question is a little basic, but I need a sanity check). Thanks and regards, Bill Halchin From rrosebru@mta.ca Sat Feb 15 09:31:47 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 15 Feb 2003 09:31:47 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18k2LX-0002y9-00 for categories-list@mta.ca; Sat, 15 Feb 2003 09:27:11 -0400 Date: Sat, 15 Feb 2003 06:52:25 +0100 From: Giuseppe Scollo Message-Id: <200302150552.h1F5qPO07228@amarena.sci.univr.it> To: categories@mta.ca Subject: categories: AMiLP-3: 1st Announcement and Call for Papers Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 36 AMiLP-3 Third AMAST Workshop on Algebraic Methods in Language Processing Verona, Italy, 25-27 August 2003 http://www.di.univr.it/amilp3 http://www.sci.univr.it/amilp3 First Announcement and Call for Papers AIMS AND SCOPE. The Third AMAST Workshop on Algebraic Methods in Language Processing, AMiLP-3, is aimed at collecting state-of-art approaches and results in formal language theory, programming language theory and natural language theory. Like its predecessors, held in 1995 at the University of Twente, Enschede, the Netherlands, and in 2000 at the University of Iowa, Iowa City, USA, the workshop is organized jointly within the Twente Workshop in Language Processing (TWLT) series. TOPICS. Research contributions are sought in all aforementioned areas of language theory, as well as other areas of language theory and language processing, including, but not limited to: formal specification and analysis, relational and higher-order languages and calculi, man-machine interaction languages, graphic and visual languages, dialogue modeling, language translation, languages for concurrent and mobile computing, new and emerging specification and programming paradigms. A common feature of work relevant to the workshop is the use of mathematical concepts, in particular the use of an algebraic approach. Due to this, traditional boundaries between the areas may disappear, allowing researchers to learn from areas that were uncommon to them before. SUBMISSIONS. Papers are sought describing original research work, even if in progress or under tentative approaches. Initially we ask you to submit a max. 4-page extended abstract. These contributions will be evaluated by the Program Committee and selected on basis of originality, significance, and relevance to the workshop aims. Authors of accepted contributions will have the opportunity to expand them to a max. 15-page full paper, for inclusion in the proceedings of the workshop. Contributions are to be submitted electronically, in PDF or printable PostScript format, either through the workshop website or by e-mail (to either PC Chair or to the PC Secretary, see below). IMPORTANT DATES. Abstract submission: 14 March, 2003 Notification: 14 April, 2003 Full version: 11 July, 2003 Early registration: 25 July, 2003 AMiLP-3 workshop: 25-27 August, 2003 PROCEEDINGS. There will be a participants' proceedings volume in the TWLT series published by the University of Twente, containing the full papers, which will be made available at the workshop. For previous volumes in the series see URL: http://parlevink.cs.utwente.nl/Conferences/twltseries.html If there will be enough contributions of sufficiently high quality, a selection of the presented papers will be considered for publication in a journal special issue, as it happened with the previous editions of the workshop. PROGRAM COMMITTEE Anton Nijholt (Chair, Enschede) Giuseppe Scollo (Chair, Verona) Domenico Cantone (Catania) Roberto Giacobazzi (Verona) Dirk Heylen (Enschede) Aravind Joshi (Philadelphia) Geert-Jan Kruijff (Saarbruecken) Vincenzo Manca (Verona) Uwe Moennich (Tuebingen) Till Mossakowski (Bremen) Mark-Jan Nederhof (Groningen) Maurice Nivat (Paris) Teodor Rus (Iowa City) Fausto Spoto (Verona) Martin Wirsing (Muenchen) LOCAL ORGANIZING COMMITTEE (University of Verona) Fausto Spoto (Chair) Giuditta Franco Roberto Giacobazzi Isabella Mastroeni Nicola Piccinini Giuseppe Scollo FURTHER INFORMATION. The AMiLP-3 website gives up-to-date information about the workshop, at URL: http://www.di.univr.it/amilp3 Furthermore you may contact: o for information relating to local organization and facilities: Dr. Fausto Spoto Universit=E0 di Verona, Dipartimento di Informatica Strada Le Grazie, 15, I-37134 Verona, Italy fax: +39 045 8027068, e-mail: fausto.spoto@univr.it o for information relating to submission of contributions: - Mw. Charlotte Bijron (AMiLP-3 Program Committee Secretary) University of Twente, Faculty of Computer Science e-mail: bijron@cs.utwente.nl - Prof. Anton Nijholt University of Twente, Faculty of Computer Science e-mail: anijholt@cs.utwente.nl - Dr. Giuseppe Scollo Universit=E0 di Verona, Dipartimento di Informatica e-mail: giuseppe.scollo@univr.it From rrosebru@mta.ca Sat Feb 15 01:38:52 2003 -0400 Return-path: Envelope-to: rrosebrugh@mta.ca Delivery-date: Sat, 15 Feb 2003 01:38:52 -0400 Received: from zent.mta.ca ([138.73.1.15]) by mailserv.mta.ca with smtp (Exim 4.10) id 18jv2K-0005tI-00 for rrosebrugh@mta.ca; Sat, 15 Feb 2003 01:38:52 -0400 Received: FROM amarena.sci.univr.it BY zent.mta.ca ; Sat Feb 15 01:39:19 2003 -0400 Received: (from scollo@localhost) by amarena.sci.univr.it (8.11.6/8.11.6) id h1F5qPO07228 for rrosebrugh@mta.ca; Sat, 15 Feb 2003 06:52:25 +0100 Date: Sat, 15 Feb 2003 06:52:25 +0100 From: Giuseppe Scollo Message-Id: <200302150552.h1F5qPO07228@amarena.sci.univr.it> To: rrosebrugh@mta.ca Subject: AMiLP-3: 1st Announcement and Call for Papers Status: RO X-Status: X-Keywords: X-UID: 37 Dear Bob, Please accept my apologies if you receive multiple copies of this announcement. I would be grateful if you could make it available to potentially interested contributors. Best regards, Giuseppe Scollo ____________________________________________________________________ AMiLP-3 Third AMAST Workshop on Algebraic Methods in Language Processing Verona, Italy, 25-27 August 2003 http://www.di.univr.it/amilp3 http://www.sci.univr.it/amilp3 First Announcement and Call for Papers AIMS AND SCOPE. The Third AMAST Workshop on Algebraic Methods in Language Processing, AMiLP-3, is aimed at collecting state-of-art approaches and results in formal language theory, programming language theory and natural language theory. Like its predecessors, held in 1995 at the University of Twente, Enschede, the Netherlands, and in 2000 at the University of Iowa, Iowa City, USA, the workshop is organized jointly within the Twente Workshop in Language Processing (TWLT) series. TOPICS. Research contributions are sought in all aforementioned areas of language theory, as well as other areas of language theory and language processing, including, but not limited to: formal specification and analysis, relational and higher-order languages and calculi, man-machine interaction languages, graphic and visual languages, dialogue modeling, language translation, languages for concurrent and mobile computing, new and emerging specification and programming paradigms. A common feature of work relevant to the workshop is the use of mathematical concepts, in particular the use of an algebraic approach. Due to this, traditional boundaries between the areas may disappear, allowing researchers to learn from areas that were uncommon to them before. SUBMISSIONS. Papers are sought describing original research work, even if in progress or under tentative approaches. Initially we ask you to submit a max. 4-page extended abstract. These contributions will be evaluated by the Program Committee and selected on basis of originality, significance, and relevance to the workshop aims. Authors of accepted contributions will have the opportunity to expand them to a max. 15-page full paper, for inclusion in the proceedings of the workshop. Contributions are to be submitted electronically, in PDF or printable PostScript format, either through the workshop website or by e-mail (to either PC Chair or to the PC Secretary, see below). IMPORTANT DATES. Abstract submission: 14 March, 2003 Notification: 14 April, 2003 Full version: 11 July, 2003 Early registration: 25 July, 2003 AMiLP-3 workshop: 25-27 August, 2003 PROCEEDINGS. There will be a participants' proceedings volume in the TWLT series published by the University of Twente, containing the full papers, which will be made available at the workshop. For previous volumes in the series see URL: http://parlevink.cs.utwente.nl/Conferences/twltseries.html If there will be enough contributions of sufficiently high quality, a selection of the presented papers will be considered for publication in a journal special issue, as it happened with the previous editions of the workshop. PROGRAM COMMITTEE Anton Nijholt (Chair, Enschede) Giuseppe Scollo (Chair, Verona) Domenico Cantone (Catania) Roberto Giacobazzi (Verona) Dirk Heylen (Enschede) Aravind Joshi (Philadelphia) Geert-Jan Kruijff (Saarbruecken) Vincenzo Manca (Verona) Uwe Moennich (Tuebingen) Till Mossakowski (Bremen) Mark-Jan Nederhof (Groningen) Maurice Nivat (Paris) Teodor Rus (Iowa City) Fausto Spoto (Verona) Martin Wirsing (Muenchen) LOCAL ORGANIZING COMMITTEE (University of Verona) Fausto Spoto (Chair) Giuditta Franco Roberto Giacobazzi Isabella Mastroeni Nicola Piccinini Giuseppe Scollo FURTHER INFORMATION. The AMiLP-3 website gives up-to-date information about the workshop, at URL: http://www.di.univr.it/amilp3 Furthermore you may contact: o for information relating to local organization and facilities: Dr. Fausto Spoto Università di Verona, Dipartimento di Informatica Strada Le Grazie, 15, I-37134 Verona, Italy fax: +39 045 8027068, e-mail: fausto.spoto@univr.it o for information relating to submission of contributions: - Mw. Charlotte Bijron (AMiLP-3 Program Committee Secretary) University of Twente, Faculty of Computer Science e-mail: bijron@cs.utwente.nl - Prof. Anton Nijholt University of Twente, Faculty of Computer Science e-mail: anijholt@cs.utwente.nl - Dr. Giuseppe Scollo Università di Verona, Dipartimento di Informatica e-mail: giuseppe.scollo@univr.it From rrosebru@mta.ca Mon Feb 17 22:22:58 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 17 Feb 2003 22:22:58 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18kxLE-0001D7-00 for categories-list@mta.ca; Mon, 17 Feb 2003 22:18:40 -0400 Message-Id: <200302160616.WAA10219@coraki.Stanford.EDU> X-Mailer: exmh version 2.1.1 10/15/1999 To: categories@mta.ca Subject: categories: Re: Slightly cheaper elephants? Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Sat, 15 Feb 2003 22:16:36 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 38 In my previous post under this subject line I asked two questions. >First, are other sources of "Elephant" at 17% or better off Amazon's $295.00 >price available to us eager students of toposophy? As it turns out, OUP is happy to offer 20% off this book for AMS, SIAM, and LMS members. As an AMS member I have suddenly forgotten what the second question was. I hereby bequeath to nonmembers of the aforesaid societies my little theorem about Amazon discounts, that for any bulk purchase accomplished within a week, with Amazon handling both billing and distribution (separate shipping addresses for each book), purchase of n+1 copies of the same book nets a total discount of 20n% (n/5) for the n+1 purchasers, that is, n/(5*(n+1)) per purchaser. Amazon distributes n/10 of this to the first purchaser and 1/10 to each of the remaining n purchasers. With Amazon's system, the first purchaser breaks even at the second purchase (each purchaser nets 10%) and draws ahead with the third (the first purchaser gets 20% and the other two 10%). A group organizing for this purpose may prefer a completely equitable system, in which each of the n+1 parties receives a discount of n/(5*(n+1)) (20% of n/(n+1)). Complete parity should therefore be achieved when the first purchaser distributes n/(5*(n+1)) - 1/10 = (n-1)/(10*(n+1)) to each of the other purchasers, but read Amazon's "Share the Love" rules in full before ordering the first book. Bear in mind that Amazon offers free shipping to those not in a tearing hurry for knowledge. A first purchaser with a taste for simplicity and a gambling spirit may wish to offer a flat 1/6 discount to each of the other purchasers, keeping n/30 of the remainder. Breakeven in this scheme is at n=5 (a total of 6 purchasers). I was close to that point when OUP's Alison Jones (Jonesal@oup.co.uk) answered my first question in the affirmative, whom members of the aforementioned societies should contact with their orders (if I have correctly interpreted her emails to me on the subject, which seemed clear enough). While all this may seem a bit hard on nonmembers of these societies, for whom n could be advantageously larger if the members joined in this plan, rest assured that the patiently supportive members of these worthy and worthwhile academic societies do not feel your pain. One other disadvantage of ordering from Amazon is that they appear to know only about the 2-volume set of 1600 pages at $295, and not the higher-priced individual volumes, for which one would expect Amazon to ask perhaps $170 each were they to offer them. If you aren't Superman planning to read and absorb the whole 1600 pages in one speed-reading pass, and didn't need something more substantial than the phone directory to stand on when rescuing the cat off the top china shelf, you might wish to consider the ergonomic and durability benefits of two separate volumes, the higher cost notwithstanding. I do hope Peter J. does reasonably well off all this, heaven knows he's worked hard enough and insightfully enough for it. Vaughan From rrosebru@mta.ca Mon Feb 17 22:29:39 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 17 Feb 2003 22:29:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18kxVT-0001pB-00 for categories-list@mta.ca; Mon, 17 Feb 2003 22:29:15 -0400 From: =?iso-8859-1?Q?Diane_B=E9langer?= To: Subject: categories: announcement: conference for Andre Joyal Date: Mon, 17 Feb 2003 14:52:37 -0500 Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" X-Priority: 3 (Normal) X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook IMO, Build 9.0.2416 (9.0.2911.0) Importance: Normal X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4522.1200 Content-Transfer-Encoding: quoted-printable X-MIME-Autoconverted: from 8bit to quoted-printable by jason.MAGELLAN.UMontreal.CA id h1HJowj53898939 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 39 Please join us to honour Andr=E9 Joyal, in celebration of his 60th birthday, at the conference "Journ=E9es Joyal" April 11, 12 and 13th 2003 Universit=E9 du Qu=E9bec =E0 Montr=E9al (UQ=C0M), Montreal, Canada Invited Speakers : Terrence Bisson (Canisius College), Pierre Cartier (IH=C9S), Ezra Getzler (Northwestern), Peter Johnstone (Cambridge), Christian Kassel (Strasbourg), William Lawvere (Buffalo), Ieke Moerdijk (Utrecht University), Ross Street (Macquarie), Myles Tierney (Rutgers) and Doron Zeilberger (Rutgers) To registrate : www.crm.umontreal.ca/Joyal For additional information (schedule; hotel information, transportation, etc) : see the web site www.crm.umontreal.ca/Joyal or contact Lise Tourigny (LaCIM), at (1) 514-987-7902 or lacim@lacim.uqam.ca Organising committee : Steven Boyer (UQAM), Fran=E7ois Lalonde (Montr=E9al) and Christophe Reutenauer (UQAM) with the participation of Jacques Hurtubise (CRM) and Pierre Leroux (UQAM) Sponsors : CIRGET (Centre interuniversitaire de recherches en g=E9om=E9trie et topologie), CRM (Centre de recherche math=E9matiques), L= ACIM (Laboratoire de combinatoire et d'informatique math=E9matique ) Thank you Diane B=E9langer Adjointe administrative Chaires de recherche en math=E9matiques D=E9partement de math=E9matiques et statistique Universit=E9 de Montr=E9al CP 6128 succ Centre-Ville Montr=E9al QC H3C 3J7 Canada T=E9l=E9phone : (514) 343-6111 poste 2710 T=E9l=E9copieur : (514) 343-5700 From rrosebru@mta.ca Sat Feb 15 11:10:29 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 15 Feb 2003 11:10:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18k3pL-0007K2-00 for categories-list@mta.ca; Sat, 15 Feb 2003 11:02:03 -0400 From: Peter Selinger Message-Id: <200302141704.h1EH48V01318@quasar.mathstat.uottawa.ca> Subject: categories: 2 Research Fellow/Postdoc positions, Ottawa To: categories@mta.ca (Categories List) Date: Fri, 14 Feb 2003 12:04:08 -0500 (EST) X-Mailer: ELM [version 2.5 PL3] 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: 40 2 Research Fellow/Postdoc positions in Logic and Computation, University of Ottawa The Logic Group in the Department of Mathematics and Statistics at the University of Ottawa is looking to hire two research fellows/postdocs beginning in September, 2003. The first position is part of a project on "Programming Languages for Quantum Computing" led by P. Selinger. The ideal applicant will have a background in programming language semantics, and an interest in developing and applying semantic methods in a quantum computation setting. Some experience in mathematical physics or related mathematics is an asset. The second position is in any area of category theory, categorical logic, and theoretical computer science. Both research fellows / postdocs will participate in the activities of the Logic and Foundations of Computation Group. This group includes faculty and students from several different Ottawa-area universities. In the Math Department, the Logic Group currently includes 3 faculty members (R. Blute, P. Scott, P. Selinger), 1 postdoc, and 6 graduate students. For more information about our team, see http://www.mathstat.uottawa.ca/lfc/ The research fellowships/postdocs are initially for one year, with a possible renewal for a second year. The annual salary is $40,000. Duties include research and the teaching of two one-semester courses. Potential applicants should contact one of us: Philip Scott (phil@site.uottawa.ca) Richard Blute (rblute@mathstat.uottawa.ca) Peter Selinger (selinger@mathstat.uottawa.ca) immediately by email to indicate their interest. They should then also send a curriculum vitae, a research plan, and arrange for three confidential letters of recommendation, with one addressing teaching, to be sent to Professor Mayer Alvo, Chairman, Department of Mathematics and Statistics, University of Ottawa, Ottawa, ON Canada, K1N 6N5. Applicants are also encouraged to include up to three copies of their most significant publications. The official application deadline has already passed, but we are still considering applications, and interested persons should contact us as soon as possible. Those who have already applied for a position will of course be considered and do not have to re-send an application. P. Scott, R. Blute, and P. Selinger From rrosebru@mta.ca Mon Feb 17 22:35:12 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 17 Feb 2003 22:35:12 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18kxav-0002Mk-00 for categories-list@mta.ca; Mon, 17 Feb 2003 22:34:53 -0400 From: John Longley X-Authentication-Warning: topper.inf.ed.ac.uk: apache set sender to jrl@localhost using -f To: Peter Lietz Subject: categories: Re: Realizability and Partial Combinatory Algebras Message-ID: <1045495641.3e50ff5947158@mail.inf.ed.ac.uk> Date: Mon, 17 Feb 2003 15:27:21 +0000 (GMT) Cc: categories References: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: IMP/PHP IMAP webmail program 2.2.8 X-Originating-IP: 129.215.32.128 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 41 Quoting Peter Lietz : > 1.) Let A be a c-pca. If I understand correctly, you say that the > indexed poset that maps a set I to the set of maps from I to P(A), > endowed with the usual entailment relation Not quite - you have to define the entailment relation to match the definition of implication (put a k in there!). The cheating way to see that all this must work out is of course via the equivalence to a PCA for which the standard construction works! > 2.) Given a c-pca A, you say that A equipped with the application > function a.b := akb is a (proper) pca. What exactly would be a > good S combinator for the new algebra ? Note that we can find elements if,true,false \in A satisfying if true x y = x, if false x y = y, and furthermore we can arrange that true = k. (I'll use "if then else" syntax below). We want to construct S such that (in A), Skxkykz ~ (xkz)k(ykz), and Skxky is always defined. Take S to be \lambda txuyvz. if v then (xkz)k(ykz) else false using the usual Curry translation of lambda terms. To see that Skxky is always defined, note that, provably, Skxky(false)z = false. Clearly there are two versions of this result, one with the axiom sxyz ~ (xz)(yz) and one with sxyz >~ (xz)(yz). Thomas asks whether every PCA with >~ is equivalent to one with ~ (Gordon Plotkin has also asked me this natural question). At the moment, the best I can do is: for any PCA A with >~, there's a PCA B with ~ and an applicative inclusion A -> B (giving rise to a geometric inclusion of toposes). Cheers, John From rrosebru@mta.ca Mon Feb 17 22:36:43 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 17 Feb 2003 22:36:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18kxcX-0002U9-00 for categories-list@mta.ca; Mon, 17 Feb 2003 22:36:33 -0400 Message-ID: <20030217210914.94383.qmail@web12205.mail.yahoo.com> Date: Mon, 17 Feb 2003 13:09:14 -0800 (PST) From: Galchin Vasili Subject: categories: Category of directed multigraphs with loops To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 42 Hello, Given two graphs, A and B, I am trying figure out how to construct the product AxB. I have been rereading "Conceptual Mathemtatics" by Lawvere. The category of irreflexive graphs is one of the running examples throughout the book. I have been concentrating on the chapters concerned with the product of objects, but I don't see any details of how to construct AxB. Have I skipped over something? Regards, Bill Halchin From rrosebru@mta.ca Thu Feb 20 12:07:57 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:07:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18lt6S-0004qD-00 for categories-list@mta.ca; Thu, 20 Feb 2003 11:59:16 -0400 Date: Mon, 17 Feb 2003 16:34:48 +0100 (CET) From: Andrzej Lingas Message-Id: <200302171534.h1HFYmi25615@ygg.cs.lth.se> To: categories@mta.ca Subject: categories: FCT'2003 - Deadline extended to February 27 X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 43 Call for Papers FCT'2003 - Deadline extended to February 27 14th International Symposium on Fundamentals of Computation Theory Malmo, Sweden, August 12-15, 2003 Invited Speakers: Sanjeev Arora, Princeton Christos Papadimitriou, Berkeley George Paun, Romanian Academy Scope: Authors are invited to submit papers presenting original and unpublished research in all areas of theoretical computer science. Topics of interest include (but are not limited to): design and analysis of algorithms, abstract data types, approximation algorithms, automata and formal languages, categorical and topological approaches, circuits, computational and structural complexity, circuit and proof theory, computational biology (new), computational geometry, computer systems theory, concurrency theory, cryptography, domain theory, distributed algorithms and computation, molecular computation, quantum computation and information, granular computation, probabilistic computation, learning theory, rewriting, semantics, logic in computer science, specification, transformation and verification, algebraic aspects of computer science. Submissions: Authors are invited to submit extended abstracts of their papers, presenting original contributions to the theory of computer science. All papers should be submitted in electronic form (in Postscript) to Andrzej.Lingas@cs.lth.se. Authors from countries where access to the Internet is difficult should contact the chair of the programme committee using the address: Andrzej Lingas, Department of Computer Science, Lund University, Box 118, SE-221 00 Lund, Sweden. Submissions should consist of: a cover page, with the author's full name, address, fax number, e-mail address, a 100-word abstract, keywords and an extended abstract describing original research. Papers should not be exceeding 12 pages in the standard LNCS-style. Important dates: Deadline for submission: February 27, 2003 (new) Notification to authors: April 8, 2003 (new) Final version: May 7, 2003 (new) Symposium: & August 12-15, 2003 Proceedings: Accepted papers will be published in the proceedings of the symposium (Lecture Notes in Computer Science, Springer-Verlag). Simultaneous submission to other conferences with published proceedings is not allowed. Tradition: The symposium on Fundamentals of Computation Theory was establi shed in 1977 as a biennial event for researchers interested in all aspects of theoretical computer science, in particular in algorithms, complexity, and formal and logical methods. The previous FCT conferences were held in the following cities: Poznan (Poland, 1977), Wendisch-Rietz (Germany, 1979), Szeged (Hungary, 1981), Borgholm (Sweden, 1983), Cottbus (Germany, 1985), Kazan (Russia, 1987), Szeged (Hungary, 1989), Gosen-Berlin (Germany, 1991), Szeged (Hungary, 1993), Dresden (Germany, 1995),=20 Krakow (Poland, 1997), Iasi (Romania, 1999) and Riga (Latvia, 2001). The 14-th International Symposium on Fundamentals of Computation Theory is organized jointly by Lund University and Malmo Hogskolan. Conference Chair Bengt Nilsson Malmo Hogskola Phone: +46 (0)40 6657244 Fax: +46 (0)40 6657320 Program Committee Arne Andersson, Uppsala Stefan Arnborg, KTH Stockholm Stephen Alstrup, ITU Copenhagen Zoltan Esik, Szeged Rusins Freivalds, UL Riga Alan Frieze, CMU Pittsburgh Leszek Gasieniec, Liverpool Magnus Halldorsson, UI Reykjavik Klaus Jansen, Kiel Juhani Karhumaki, Turku Marek Karpinski, Bonn Christos Levcopoulos, Lund Ming Li, Santa Barbara Andrzej Lingas, Lund (Chair) Jan Maluszynski, Linkoping Fernando Orejas, Barcelona Jurgen Promel, Berlin Rudiger Reischuk, Lubeck Wojciech Rytter, Warsaw/NJIT Miklos Santha, Paris-Sud Andrzej Skowron, Warsaw Paul Spirakis, Patras Esko Ukkonen, Helsinki Ingo Wegener, Dortmund Pawel Winter, Copenhagen Vladimiro Sassone, Sussex Organizing Committee: Bengt Nilsson, Malmo (Chair) Oscar Garrido, Malmo Thore Husfeldt, Lund Miroslaw Kowaluk, Warsaw Web site: www.ts.mah.se/forskn/cs/fct2003/ E-mail: bengt.nilsson@ts.mah.se From rrosebru@mta.ca Thu Feb 20 12:23:40 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:23:40 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltSL-0006Lp-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:21:53 -0400 Date: Tue, 18 Feb 2003 12:48:48 +0100 (CET) From: Message-Id: <200302181148.MAA14451@kodder.math.uu.nl> To: categories@mta.ca Subject: categories: Re: Realizability and Partial Combinatory Algebras X-Sun-Charset: US-ASCII X-Virus-Scanned: by AMaViS snapshot-20020300 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 44 Dear John, > Note that we can find elements if,true,false \in A satisfying > if true x y = x, if false x y = y, > and furthermore we can arrange that true = k. > (I'll use "if then else" syntax below). > We want to construct S such that (in A), > Skxkykz ~ (xkz)k(ykz), and Skxky is always defined. > Take S to be > \lambda txuyvz. if v then (xkz)k(ykz) else false > using the usual Curry translation of lambda terms. To see that > Skxky is always defined, note that, provably, Skxky(false)z = false. There is a point I don't understand. If I work out Skxky, then I find a term which contains subterms of the form xk, yk. So how can this be defined if x or y represent nowhere defined functions? It looks to me, that you are using a form of Combinatorial Completeness that is not valid with the weaker S-axiom. If I am correct, one has the following form of Combinatorial Completeness: For every term t and variable z, there is a term \lambda z.t with the property: If \lambda z.t is defined, then for each a, (\lambda z.t)a ~ t[a/z] (of course, a really correct version has more than one variable) Best, Jaap From rrosebru@mta.ca Thu Feb 20 12:23:40 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:23:40 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltT8-0006Ow-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:22:42 -0400 From: Thomas Streicher Message-Id: <200302181332.OAA06673@fb04209.mathematik.tu-darmstadt.de> Subject: categories: preservation of exponentials To: categories@mta.ca Date: Tue, 18 Feb 2003 14:32:50 +0100 (CET) X-Mailer: ELM [version 2.4ME+ PL66 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 45 Recently when rereading an old paper I came across a passage insinuating that every finite limit preserving full and faithful functor between toposes does also preserve exponentials. I am sceptical because I don't see any obvious reason for it. It is certainly wrong for ccc's (a counterexample is the inclusion of open sets of reals into powersets of reals). On the other hand Yoneda functors and direct image parts of injective geom morphs do preserve exponentials. So I was thinking of inverse image parts of connected geom.morph.'s. Of course, \Delta : Set -> Psh(C) for a connected C does preserve exponentials. What about Delta : Set -> Sh(X) for X connected but not locally connected, e.g. take for X Cantor space with a focal point added? Thomas Streicher From rrosebru@mta.ca Thu Feb 20 12:26:54 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:26:54 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltVm-0006h3-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:25:26 -0400 Message-ID: <002801c2d80a$2860cba0$b670fe8c@lucent.com> From: "Vidhyanath Rao" To: "categories" References: <200302181218.EAA06337@coraki.Stanford.EDU> Subject: Re: categories: Slightly cheaper elephants? Date: Wed, 19 Feb 2003 06:29:17 -0500 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.50.4920.2300 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4920.2300 X-RAVMilter-Version: 8.4.2(snapshot 20021217) (mathserv) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 46 > My apologies but I have abandonded this project, per my most recent post to > the categories list. If you're not a member of AMS, SIAM, or LMS and would > still like to be part of a group purchase from Amazon, please let me know and > I can put you in touch with the others in that situation who've contacted me. According to the e-mail I received from Ms. Jones (see below), this is available only from the UK catalog. So those of us in the US may still find it worthwhile to go through Amazon, or wait for the possibility that similar discount may be offered in the US at some point in the future. -------- Dear Mr Rao This discount is only available in the UK catalogues (OUP distributes and markets AMS titles in Europe) but I am making a discretionary exception for Prof Pratt because of current unavailability of this title in the US. From rrosebru@mta.ca Thu Feb 20 12:27:23 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:27:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltWe-0006rB-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:26:20 -0400 Message-ID: <20030220001651.79067.qmail@web12201.mail.yahoo.com> Date: Wed, 19 Feb 2003 16:16:51 -0800 (PST) From: Galchin Vasili Subject: categories: More Topos questions ala "Conceptual Mathematics" To: categories@mta.ca MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 47 Hello, 1) In the very last chapter (Session 33 "2: Toposes and logic" of "Conceptual Mathematics" where the authors cover topoi, they define '=>' for the internal Heyting algebra of Omega: "Another logical operation is 'implication', which is denoted '=>'. This is also a map Omega x Omega->Omega, defined as the classifying map of the subobject S 'hook' Omega x Omega determined by the all those in Omega x Omega such that alpha "subset of" beta." Starting from "subobject S 'hook" ......" I got totally lost. I am frustrated because I know this is crucial to understanding why Omega is an internal Heyting algebra, so any help would be appreciated. (I am assuming that alpha and beta are subojects of Omega???). 2) In the same Session 33 on pg 350 is a set "rules of logic". These are exactly the axioms for a Heyting algebra, yes? Regards, Bill Halchin From rrosebru@mta.ca Thu Feb 20 12:29:23 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:29:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltYP-0007Ez-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:28:09 -0400 Date: Tue, 18 Feb 2003 19:34:24 +0100 (CET) From: Peter Lietz To: categories Subject: categories: Re: Realizability and Partial Combinatory Algebras In-Reply-To: <200302181148.MAA14451@kodder.math.uu.nl> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-MailScanner: Found to be clean X-Scanner: exiscan for exim4 *18lCgI-0007W8-00*RfTA.exZoJY* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 48 Although in the meantime I was completely convinced by John's argument, I now believe that Jaap has indeed raised a serious point. However, I think that the flaw (if it indeed was) in John's argument is not in the form of combinatory completeness that he applies, but it is an illegal instance of substitution, which one has to be very careful with within a logic of partial terms where variables range over existing objects (as e.g. in E+ logic, presented in Troelstra & van Dalen, Vol. I). From IF FALSE x y >~ y one cannot conclude IF FALSE q r >~ r for q and r arbitrary terms. As to the definitive and correct form of combinatory completess in a c-pca I make the following proposition (which I have checked): Let A be a c-pca and t be a term built up using application from A-constants and variables. Then there is a term (\lambda x. t) that has the same free variables as t save x such that for all a\in A and all valuations of free variables (\lambda x. t) a >~ t[a/x] That means, if w.r.t. some valuation the right hand side denotes a value then the left hand side denotes the same value. In particular, if for some valuation and some a in A the right hand side exists (denotes a value) then so does the left hand side and hence (\lambda x. t) (for this particular valuation), as application is a strict function. The same is true for simultaneous abstraction (replace x and a by \vec{x} and \vec{a} resp.). One only needs to prove a little substitution lemma. This proposition is essentially in the Hyland-Ong paper (the small difference is that, in the paper all variables get abstracted away, but that is inessential). Best, Peter From rrosebru@mta.ca Thu Feb 20 12:53:02 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 12:53:02 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18ltu6-00023c-00 for categories-list@mta.ca; Thu, 20 Feb 2003 12:50:34 -0400 Date: Thu, 20 Feb 2003 17:44:57 +0100 (CET) From: Message-Id: <200302201644.RAA15105@kodder.math.uu.nl> To: categories@mta.ca Subject: categories: Re: Realizability and Partial Combinatory Algebras X-Sun-Charset: US-ASCII X-Virus-Scanned: by AMaViS snapshot-20020300 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 49 Dear Peter and John, Peter correctly pointed out the error in my message: the problem was in the use of the "if then .. else .." syntax, not in any form of combinatorial completeness. Answering John: I was using a construction of \lambda x.t where \lambda x.M is KM whenever M is any term not containing x free (this works just as well); so in my construction, \lambda vz. if v then xkzk(ykz) else false DOES contain subterms xk and yk. Anyway, I do now believe that John's latest version is correct. This is really very nice, and a surprise (for me, at least). I stand corrected and must apologize for my first posting in this discussion, casting doubt on PTJ's message. One little point, regarding Combinatorial Completeness. I believe the following form is valid (in the situation with the weak S-axiom): suppose t is a term, x a variable. There is a term \lambda x.t such that for all a,a_1,...,a_n in A: ((\lambda x.t)[a_1,...,a_n])a ~ t[a,a_1,...,a_n] So this is just like the ordinary form, except for the assertion that (\lambda x.t)[a_1,...,a_n] is always defined. We have that (\lambda x.t)[a_1,...,a_n] is defined whenever for some a in A, t[a,a_1,...,a_n] is defined. Best, Jaap From rrosebru@mta.ca Thu Feb 20 13:07:36 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 13:07:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18lu84-0003Fx-00 for categories-list@mta.ca; Thu, 20 Feb 2003 13:05:00 -0400 Date: Thu, 20 Feb 2003 16:59:59 +0000 (GMT) From: "Prof. Peter Johnstone" To: categories@mta.ca Subject: categories: Re: preservation of exponentials In-Reply-To: <200302181332.OAA06673@fb04209.mathematik.tu-darmstadt.de> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan for exim4 (http://duncanthrax.net/exiscan/) *18lu3D-0007Dt-00*zX9VwTnLJ9s* Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 50 On Tue, 18 Feb 2003, Thomas Streicher wrote: > Recently when rereading an old paper I came across a passage insinuating > that every finite limit preserving full and faithful functor between toposes > does also preserve exponentials. > I am sceptical because I don't see any obvious reason for it. It is certainly > wrong for ccc's (a counterexample is the inclusion of open sets of reals into > powersets of reals). On the other hand Yoneda functors and direct image parts > of injective geom morphs do preserve exponentials. > So I was thinking of inverse image parts of connected geom.morph.'s. > Of course, \Delta : Set -> Psh(C) for a connected C does preserve exponentials. > What about Delta : Set -> Sh(X) for X connected but not locally connected, > e.g. take for X Cantor space with a focal point added? > If a full and faithful functor between ccc's has a left adjoint which preserves binary products, then it preserves exponentials (Elephant, A1.5.9(ii)). In the absence of a left adjoint, the result is not true in general: Set --> Sh(X) for X connected but not locally connected gives a counterexample, as you suggest, and so does the inclusion (continuous G-sets) --> (arbitrary G-sets) for a topological group G. Peter Johnstone From rrosebru@mta.ca Thu Feb 20 15:02:39 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 15:02:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18lvuk-0004gp-00 for categories-list@mta.ca; Thu, 20 Feb 2003 14:59:22 -0400 Message-ID: <000701c2d910$a0faa480$39a14244@grassmann> From: "Stephen Schanuel" To: categories@mta.ca> References: <20030220001651.79067.qmail@web12201.mail.yahoo.com> Subject: categories: Re: More Topos questions ala "Conceptual Mathematics" Date: Thu, 20 Feb 2003 13:48:16 -0500 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 6.00.2800.1106 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1106 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 51 Probably it's easiest to try to define implication yourself, and then you'll see that it is just what 'Conceptual Mathematics' says -- but if you need more help: 'Implication' is supposed to be a binary operation on Omega, i.e. a map from OmegaxOmega to Omega. How can we go about specifying such a map? Well, a map from any object X to Omega amounts (by the universal property) to a subobject of X, so we're looking for a subobject of OmegaxOmega, i.e. a monomorphism with codomain X=OmegaxOmega. Now how can we go about specifying a nonomorphism with a given codomain X? Perhaps the simplest way is to specify two maps with domain X and common codomainY; then the equalizer of these will do. See if you can think of two maps from OmegaxOmega to Omega whose equalizer seems to capture the intuitive notion of 'implication'. It might help to start with a simple case, the category of sets, where Omega is just the two-element set with elements called T (true) and F (false). (If you have ever seen 'truth tables', you will see that what you are looking for is also called the 'truth table for implication', but if you haven't seen these, please ignore this remark.) If you succeed in specifying the pair of maps, you will have learned much more than you can by reading further; but if after trying you are still stuck, then read on. The desired two maps from OmegaxOmega to Omega are: (1) projection on the first factor, and (2) conjunction, which was defined in the paragraph just preceding the one you're stuck on. I hope you managed to find these maps, but even if you didn't, you can now have fun by looking at the maps conjunction, imlication, negation, etc, in irreflexive graphs (and other simple toposes) and comparing these with those in sets; you'll learn why Boolean algebra, so familiar in sets, needs to be replaced by Heyting algebra in more general toposes. Good luck in your studies! Yours, Steve Schanuel ----- Original Message ----- From: "Galchin Vasili" To: Sent: Wednesday, February 19, 2003 7:16 PM Subject: categories: More Topos questions ala "Conceptual Mathematics" > > Hello, > > 1) In the very last chapter (Session 33 "2: Toposes and logic" of "Conceptual Mathematics" where the authors cover topoi, they define '=>' for the internal Heyting algebra of Omega: > > "Another logical operation is 'implication', which is denoted '=>'. This is also a map Omega x Omega->Omega, defined as the classifying map of the subobject S 'hook' Omega x Omega determined by the all those in Omega x Omega such that alpha "subset of" beta." > > Starting from "subobject S 'hook" ......" I got totally lost. I am frustrated because I know this is crucial to understanding why Omega is an internal Heyting algebra, so any help would be appreciated. (I am assuming that alpha and beta are subojects of Omega???). > > 2) In the same Session 33 on pg 350 is a set "rules of logic". These are exactly the axioms for a Heyting algebra, yes? > > > > Regards, Bill Halchin > > > > From rrosebru@mta.ca Thu Feb 20 21:33:29 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Feb 2003 21:33:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18m1z8-0001FB-00 for categories-list@mta.ca; Thu, 20 Feb 2003 21:28:18 -0400 X-Mailer: exmh version 2.1.1 10/15/1999 To: categories@mta.ca Subject: categories: Re: More Topos questions ala "Conceptual Mathematics" In-Reply-To: Message from "Stephen Schanuel" of "Thu, 20 Feb 2003 13:48:16 EST." <000701c2d910$a0faa480$39a14244@grassmann> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 20 Feb 2003 16:57:26 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 52 >From: Stephen Schanuel >you'll learn why Boolean algebra, so familiar in sets, needs >to be replaced by Heyting algebra in more general toposes. I would expand this beyond Heyting algebras to quantales, residuated monoids, etc. See http://boole.stanford.edu/pub/seqconc.pdf for an example of a situation, namely event structures as a model catering simultaneously to concerns of branching time and "true" concurrency, that has traditionally been handled in a Boolean way. That paper extends event structures to three- and four-valued logics of behavior. This particular extension (expansion, augmentation) doesn't generalize the two-valued Boolean logic of event structures to Heyting algebras. There are exactly two three-element idempotent commutative quantales. Obviously the three-element Heyting algebra is one of them, and this HA does find application in drawing a distinction between accidental and causal temporal precedence, a topic Haim Gaifman looked into around 1988. The other, which isn't a Heyting algebra, is at the core of the notion of transition as the intermediate state between "ready" and "done," more on this in the above-cited paper. This is not to say that there is no topos-theoretic approach to this extension. In particular the above paper briefly mentions the presheaf category Set^FinBip where FinBip is the category of finite bipointed sets, as a notion of cubical set. Cubical sets certainly provide one algebraically attractive model of true concurrency that works roughly the same way as the one based on this 3-element quantale---both of them entail cubical structure---but I've been finding the latter a more elementary and natural tool for working with cubes, at least for my purposes---homologists may find limitations that I don't seem to run into. An advantage of Set^FinBip is that it accommodates cyclic structures (iterative concurrent automata), whereas the one based on 3' as I've been calling this 3-element quantale works with acyclic cubical sets, calling for iteration to be unfolded, much as formal languages "are" unfolded grammars. (Come to think of it, I don't know anything about the subobject classifier of Set^FinBip. If someone has a succinct description of it I'd be very grateful.) The main point here is that there *is* a logic of behavior that is close to but not quite intuitionistic, at least not in the strict Heyting algebra sense. Furthermore it is not a question of just finding the smallest Heyting algebra in which the above quantale embeds, since there isn't one that preserves the ordered monoid structure: a Heyting algebra must have its monoid unit at the top, which 3' as "the other three-element quantale" doesn't. So whatever relationship obtains between the subobject classifier of Set^FinBip and 3', it's not an ordered-monoid embedding of the latter in the former. See http://boole.stanford.edu/pub/seqconc.pdf for more details. Vaughan From rrosebru@mta.ca Sat Feb 22 15:41:32 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 22 Feb 2003 15:41:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18mfMC-0006k2-00 for categories-list@mta.ca; Sat, 22 Feb 2003 15:30:44 -0400 From: Thomas Streicher Message-Id: <200302201840.TAA29712@fb04305.mathematik.tu-darmstadt.de> Subject: categories: problem with "thunking" To: categories@mta.ca Date: Thu, 20 Feb 2003 19:40:17 +0100 (CET) X-Mailer: ELM [version 2.4ME+ PL66 (25)] 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: 53 I also for some time believed in John Longley's arguments that for any cpca A one may define an equivalent one where application is redefined as ab = akb but then I came across the following problem. Evidently, all his arguments are based on "thunking", i.e. an operator T such that Tt defined and Ttk \simeq t (1) for all polynomials t and elements a in the cpca. John suggest to take for T the combinator Txz \simeq zxk which certainly is definable. HOWEVER, this T doesn't satisfy (1) in general for closed terms t that aren't defined. To see this failure look at the paradigmatic cpca of normal forms. The problem there is that when applying the normal form T = \x.\z.zx(\u.\v.u) to t = (\x.xx)(\x.xx) then Tt does NOT normalize as t does not normalize. Actually, I even don't see how one can define composition in the cpca of normal forms: consider the normal forms a = \x.xx and b = \y.\x.xx for which we have that a(bu) is undefined for all u BUT I don't know of any normal form t such that tu is undefined for all u (as such a t would have to be lambda abstraction \x.t' with x not free in t' and then t' cannot be a normal form!). Thus there cannot be a normal form c with cu \simeq a(bu) for all u Admittedly, that looks a bit alarming because it might also affect the work of Hyland and Ong. But on the other hand I don't see where I am wrong. Moreover, in a sense the phenomenon is well known. When making normal forms into a category one has to prove a cut-elimination theorem that certainly fails for untyped terms. Thomas PS My impression is that people haven't really addressed Peter's question. The reason for the definedness axioms of a pca are derived from the intuition of "weak head normal forms" where \x.t is always defined (as like in functional programming one isn't allowed to reduce under a lambda abstraction). That is the "reason" why people have introduced the definedness axioms. There is no reason why pca's should be the most general structure for which the ``realizability construction'' works. As it seems to me normal forms are not an instance of such a generalization (however it might look). From rrosebru@mta.ca Sat Feb 22 15:41:32 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 22 Feb 2003 15:41:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18mfQA-0006xU-00 for categories-list@mta.ca; Sat, 22 Feb 2003 15:34:50 -0400 Date: Fri, 21 Feb 2003 16:03:39 +0100 (CET) From: Peter Lietz To: categories Subject: categories: Re: Realizability and Partial Combinatory Algebras In-Reply-To: <200302201644.RAA15105@kodder.math.uu.nl> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-MailScanner: Found to be clean Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 54 Dear Jaap, John and Thomas, I am not yet convinced. What I do more or less believe is that the operation of `thunking' works for a c-pca. But it does *not* seem to be the case that the combinator S that John defined (using thunking) satisfies the equations Skxky(false)z = false and Skxkykz = (xkz)k(ykz) , even in a total combinatory algebra! As I do not trust my term manipulation skills so much any more in this context, I wrote a little Haskell Program to compute the normal forms. The left hand side terms are indeed normalizing but their normal forms are considerably longer than the respective right hand side terms. Oddly enough, the normal form of the former term even contains variables. Now it is very well possible that my program has a bug, programming is hardly my main occupation. If you like to play with it you are invited to access it via http://www.mathematik.tu-darmstadt.de/~lietz/cpca/cpca.hs and if you find a bug please do let me know. I cannot put my finger on exactly what is the gap in the proof. I think it has to do with the fact that thunk(e,c) does not commute with substitution in the way one might expect. Or put differently, the `thunk' algorithm and the Curry algorithm don't play along very well. Something in that direction. Finally, I should apologize for taxing the categories mailing list readers' patience with a subject that is likely only of marginal interest to most. have a nice weekend, Peter From rrosebru@mta.ca Sat Feb 22 15:41:32 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 22 Feb 2003 15:41:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18mfMu-0006mL-00 for categories-list@mta.ca; Sat, 22 Feb 2003 15:31:28 -0400 Message-ID: <3E5638E0.3070906@mcs.le.ac.uk> Date: Fri, 21 Feb 2003 14:34:08 +0000 From: "V. Schmitt" User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020615 Debian/1.0.0-3 X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: job: ra position in Leicester Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 55 Dear all, there should be soon some ra position in Leicester. for about one year I guess. Subject: (enriched) category and CS. People interested shoulc contact me. All the best, Vincent. From rrosebru@mta.ca Sat Feb 22 15:41:32 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 22 Feb 2003 15:41:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18mfP9-0006sy-00 for categories-list@mta.ca; Sat, 22 Feb 2003 15:33:47 -0400 Date: Fri, 21 Feb 2003 09:35:39 -0500 Subject: categories: Re: Category of directed multigraphs with loops Content-Type: text/plain; charset=ISO-8859-1; format=flowed Mime-Version: 1.0 (Apple Message framework v551) To: categories@mta.ca From: Francois Magnan In-Reply-To: <20030217210914.94383.qmail@web12205.mail.yahoo.com> Message-Id: Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 56 Hi,=0D =0D The product in the category of directed irreflexive multigraphs = is =0D simple to compute. In fact, if you learn further about topos theory you =0D= will learn that all finite limits in a presheaf topos are computed =0D pointwise. The category that interests you is a presheaf category since =0D= it is the category of all functors from the category=0D =0D ------------>=0D C^op =3D A V=0D ------------>=0D =0D to the category of sets.=0D =0D =0D In simpler words, it means that if you take two graphs: G_1 and G_2 =0D with vertices sets V_1 and V_2 and arrows sets A_1 and A_2 =0D respectively. The product graph P=3DG_1 x G_2 will have V_P=3DV_1xV_2 =0D= (normal catesian product in sets) as vertices and A_P=3DA_1xA_2 as =0D arrows. The incidence relation are the expected ones.=0D =0D For the reflexive directed multigraphs as all presheafs the recipe is =0D= the same. I would suggest you to read the book:=0D =0D M.La Palme Reyes, G. Reyes, Generic Figures and their glueings: A =0D constructive approach to functor categories.=0D =0D Which is still unpublished as of now but I can send you a PDF.=0D =0D Hope this helps,=0D Francois Magnan=0D =0D =0D On Monday, Feb 17, 2003, at 16:09 America/Montreal, Galchin Vasili =0D wrote:=0D =0D >=0D > Hello,=0D >=0D > Given two graphs, A and B, I am trying figure out how to =0D > construct=0D > the product AxB. I have been rereading "Conceptual Mathemtatics" by=0D > Lawvere. The category of irreflexive graphs is one of the running =0D > examples=0D > throughout the book. I have been concentrating on the chapters =0D > concerned=0D > with the product of objects, but I don't see any details of how to=0D > construct AxB. Have I skipped over something?=0D >=0D > Regards, Bill Halchin=0D >=0D >=0D >=0D >=0D - --------------------------------------------=0D Francois Magnan=0D Recherche & D=E9veloppement=0D Cogniscience Editeurs Inc.=0D fmagnan@cogniscienceinc.com=0D =0D From rrosebru@mta.ca Tue Feb 25 20:28:55 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 25 Feb 2003 20:28:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18npK0-0001aU-00 for categories-list@mta.ca; Tue, 25 Feb 2003 20:21:16 -0400 Date: Mon, 24 Feb 2003 02:41:01 GMT Message-Id: <200302240241.h1O2f1W12469@glory.dcs.ed.ac.uk> X-Authentication-Warning: glory.dcs.ed.ac.uk: als set sender to als+lics-junk@inf.ed.ac.uk using -f To: LICS List From: Alex Simpson Subject: categories: LICS 2003 Call for Short Presentations Reply-To: als+lics-junk@dcs.ed.ac.uk Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 57 **************** Submission Deadline is MARCH 21, 2003 ********************* Eighteenth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE June 22nd - 25th, 2003, Ottawa, Canada http://www.lfcs.informatics.ed.ac.uk/lics CALL FOR SHORT PRESENTATIONS The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense. LICS 2003 will take place in Ottawa, Canada, June 22-25, 2003 and will feature invited talks, invited tutorials, and presentations of papers that will appear in the LICS 2003 proceedings. In addition, LICS 2003 will have a session of short (5-10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages long), should be entered by following the "Instructions for short presentations" link at the LICS 2003 website http://www.lfcs.informatics.ed.ac.uk/lics/lics03 between March 17th and March 21st, 2003. Authors will be notified of acceptance or rejection by April 4th, 2003. Suggested, but not exclusive, topics of interest for submissions include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, domain theory, finite model theory, formal aspects of program analysis, formal methods, hybrid systems, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logics of programs, logic programming, modal and temporal logics, model checking, programming language semantics, reasoning about security, rewriting, specifications, type systems and type theory, and verification. Program Chair: Phokion G. Kolaitis Computer Science Department University of California, Santa Cruz Santa Cruz, CA 95064, USA Email: kolaitis@cs.ucsc.edu Phone: + 1 831 459 4768 Fax: + 1 831 459 4829 Program Committee: Michael Benedikt, Bell Laboratories Andreas R. Blass, University of Michigan Maria Luisa Bonet, UPC, Barcelona Witold Charatonik, University of Wroclaw Marcelo Fiore, University of Cambridge Giorgio Ghelli, Universita di Pisa Thomas A. Henzinger, UC Berkeley Alan Jeffrey, DePaul University Assaf J. Kfoury, Boston University Phokion G. Kolaitis, UC Santa Cruz Orna Kupferman, Hebrew University of Jerusalem Ursula Martin, University of St Andrews Paul-Andre Mellies, CNRS & University of Paris 7 Eugenio Moggi, Universita di Genova Ugo Montanari, Universita di Pisa Paliath Narendran, University at Albany SUNY Luke Ong, University of Oxford & National University of Singapore Martin Otto, University of Wales Swansea Frank Pfenning, Carnegie Mellon University Mirek Truszczynski, University of Kentucky From rrosebru@mta.ca Tue Feb 25 20:42:07 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 25 Feb 2003 20:42:07 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18npcF-0002Nj-00 for categories-list@mta.ca; Tue, 25 Feb 2003 20:40:07 -0400 Message-ID: <3E5A49FA.2000005@mcs.le.ac.uk> Date: Mon, 24 Feb 2003 16:36:10 +0000 Subject: categories: Workshop on categorical methods for concurrency.... From: "A.Kurz" User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/2002062= Bcc: Status: RO X-Status: X-Keywords: X-UID: 58 3 Debian/1.0.0-0.woody.1 X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: CfP: CMCIM'03 Content-Type: text/plain; charset=3DISO-8859-1; format=3Dflowed Content-Transfer-Encoding: 8bit Sender: cat-dist@mta.ca Precedence: bulk [ Apologies for multiple copies ] Workshop on CATEGORICAL METHODS FOR CONCURRENCY, INTERACTION, AND MOBILITY Marseille, France, 6 September 2003 affiliated with CONCUR 2003 and held together with GETCO 2003 Call for Papers See also: http://www.mcs.le.ac.uk/events/cmcim03 Aims and Scope: The aim of the workshop is to bring together researchers applying category theory to concurrency, interaction, or mobility. Topics of interest include, but are not limited to: categorical algebras of processes categorical methods in game semantics and geometry of interaction categorical models of term/graph rewriting or rewriting logic Chu spaces coalgebras, bialgebras, coinduction comparing models of concurrency enriched categories of processes interaction categories presheaf models GETCO'03: Due to the close relation between geometric and topological methods on the one hand and categorical methods on the other hand, CMCIM'03 will be held jointly with the workshop on Geometric and Toplogical Methods in Concurrency Theory (GETCO'03). Both workshops will be on the same day with their talks not overlapping. Invited Lecture: Glynn Winskel Programme Committee: Marcelo Fiore (Cambridge) Eric Goubault (Paris) Thomas Hildebrandt (Copenhagen) Alexander Kurz (Leicester) Ugo Montanari (Pisa) John Power (Edinburgh) Jan Rutten (Amsterdam) Peter Selinger (Ottawa) Glynn Winskel (Cambridge) Important dates: Deadline for submission: June 1 Notification of acceptance: July 7 Final version due: July 27 Workshop dates: September 6 Location: The workshop will be held in Marseille. It is a satellite workshop of CONCUR 2003. For venue and registration see the CONCUR web page at http://concur03.univ-mrs.fr Submissions: It is planned to publish the proceedings of the meeting as a volume in Elsevier's ENTCS series. Papers must contain original contributions. Papers should be submitted as PostScript files by email to cmcim03@mcs.le.ac.uk, containing `CMCIM-submission' in the subject. A separate message should also be sent (subject: CMCIM-abstract), containing authors, title, and a text-only abstract. Workshop organizers: Thomas Hildebrandt BRICS, DAIMI, Computer Science Deptartment, University of Aarhus, Ny Munkegade, B. 540, 8000 =C5rhus C, DK Alexander Kurz Department of Mathematics and Computer Science, University of Leicester, University Road, Leicester, LE1 7RH. Email: cmcim03@mcs.le.ac.uk Further information at http://www.mcs.le.ac.uk/events/cmcim03 From rrosebru@mta.ca Tue Feb 25 20:58:17 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 25 Feb 2003 20:58:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18nprz-0003Dm-00 for categories-list@mta.ca; Tue, 25 Feb 2003 20:56:23 -0400 Message-ID: <20030225195501.74658.qmail@web12001.mail.yahoo.com> Date: Tue, 25 Feb 2003 11:55:01 -0800 (PST) From: Andrei Popescu Subject: categories: projective algebras To: categories@mta.ca 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: 59 Dear Categorists, Some time ago, I have posed you a question about the characterization of projective algebras in the category of all algebras of a given signature. Since some of you appeard interested in the subject, I allow myself to send you, in a slightly detailed manner, the answer that I have found. Projective algebras coincide with free algebras in the following cases: I. Any class (i.e. complete subcategory) of algebras that is closed to taking subobjects and for which free algebras exist and have a certain property (namely that there are no infinite chains of elements such that each one is obtained by applying an operation to an n-uple that includes the predecesor in the chain). In particular, II. Suppose X is a countably infinite set. Any quasivariety K of algebras for which the kernel of the unique morphism extending X from the term algebra to the algebra freely generated in K by X has finite congruence classes. In particular, III. - The category of all algebras (of a given signature); - The category of [commutative] semigroups; - The category of [commutative] (non-unital and non-anihilating) semirings. Best regards, Andrei From rrosebru@mta.ca Wed Feb 26 14:23:21 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 26 Feb 2003 14:23:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18o6BH-0002F8-00 for categories-list@mta.ca; Wed, 26 Feb 2003 14:21:24 -0400 Date: Wed, 26 Feb 2003 01:12:11 -0800 From: Vaughan Pratt Message-Id: <200302260912.BAA30134@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Lamarche casuistries paper Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 60 I seem to have misplaced my copy of Francois Lamarche's paper on casuistries. I'd be very grateful for either an online copy or Francois' current email address (preferably both). Vaughan Pratt From rrosebru@mta.ca Wed Feb 26 14:27:13 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 26 Feb 2003 14:27:13 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18o6FV-0002g0-00 for categories-list@mta.ca; Wed, 26 Feb 2003 14:25:45 -0400 Message-ID: <002001c2dd81$55acc1a0$b1e493d9@rmi.acnet.ge> From: "Mamuka Jibladze" To: References: <20030225195501.74658.qmail@web12001.mail.yahoo.com> Subject: categories: Re: projective algebras Date: Wed, 26 Feb 2003 14:24:55 +0400 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.50.4807.1700 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4807.1700 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 61 Here is some more information on the question of Andrei Popescu. In the paper "Projectives are free for nilpotent algebraic theories" by T. Pirashvili (pages 589-599 in: Algebraic $K$-theory and its applications. Proceedings of the workshop and symposium, ICTP, Trieste, Italy, September 1-19, 1997. World Scientific, Singapore (1999)) it is shown that if projectives are free in the category of internal abelian groups of a sufficiently nice (e. g. Maltsev) variety, then the same holds for the category of all nilpotent (in the sense of commutator calculus) algebras in that variety. This is derived from the fact that one can lift splittings of idempotents along a linear extension of algebraic theories. Mamuka > Dear Categorists, > > Some time ago, I have posed you a question about the characterization of > projective algebras in the category of all algebras of a given signature. > Since some of you appeard interested in the subject, I allow myself to > send you, in a slightly detailed manner, the answer that I have found. > > Projective algebras coincide with free algebras in the following cases: > > I. Any class (i.e. complete subcategory) of algebras that is closed to > taking subobjects and for which free algebras exist and have a certain > property (namely that there are no infinite chains of elements such that > each one is obtained by applying an operation to an n-uple that includes > the predecesor in the chain). > > In particular, > > II. Suppose X is a countably infinite set. Any quasivariety K of algebras > for which the kernel of the unique morphism extending X from the term > algebra to the algebra freely generated in K by X has finite congruence > classes. > > In particular, > > III. - The category of all algebras (of a given signature); > > - The category of [commutative] semigroups; > > - The category of [commutative] (non-unital and non-anihilating) semirings. > > Best regards, > > Andrei From rrosebru@mta.ca Wed Feb 26 19:06:29 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 26 Feb 2003 19:06:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18oAYp-0005k5-00 for categories-list@mta.ca; Wed, 26 Feb 2003 19:01:59 -0400 Date: Wed, 26 Feb 2003 15:04:23 -0500 (EST) From: japaridze g Message-Id: <200302262004.PAA19852@monet.vill.edu> To: categories@mta.ca Subject: categories: CFP: INT'L CONF ON ALGEBRAIC AND TOPOLOGICAL METHODS IN NON-CLASSICAL LOGICS Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 62 INTERNATIONAL CONFERENCE ON ALGEBRAIC AND TOPOLOGICAL METHODS IN NON-CLASSICAL LOGICS Tbilisi, Georgia, 7 - 11 July 2003 The aim of this conference is to present some recent advances in the use of algebraic, order-theoretic, and topological methods in non-classical logics. We also hope to bring together researchers in the fields of non-classical logics, lattice theory, universal algebra, category theory, and general topology in order to foster collaboration and to get new ideas for further research. CONFERENCE TOPICS: Lattices with operators Topological semantics of modal logic Topological and topos semantics of intuitionistic logic Ordered topological spaces. INVITED SPEAKERS: Johan van Benthem, University of Amsterdam Leo Esakia, Georgian Academy of Sciences Mai Gehrke, New Mexico State University John Harding, New Mexico State University Ramon Jansana, University of Barcelona Joachim Lambek, McGill University Daniele Mundici, Milan University Yde Venema, University of Amsterdam Michael Zakharyaschev, King's College Marek Zawadowski, University of Warsaw CALL FOR PAPERS: If you wish to speak at the conference, please send by email a title and abstract of your talk to Guram Bezhanishvili (gbezhani@nmsu.edu). The deadline for submissions is 1 May. We will let you know by 15 May if you will be invited to speak at the conference. The deadline to register for the conference is 1 June. LOCATION: Tbilisi State University, Tbilisi, Georgia WEB SITE: http://piscopia.nmsu.edu/morandi/TbilisiConference IMPORTANT DATES: Submission deadline: 1 May 2003 Notification of acceptance: 15 May 2003 Registration deadline: 1 June 2003 Conference: 7 - 11 July 2003 PROGRAM COMMITTEE: Guram Bezhanishvili, New Mexico State University Patrick Morandi, New Mexico State University Willem Blok, University of Illinois at Chicago Roberto Cignoli, University of Buenos Aires Josep Maria Font, University of Barcelona Dick de Jongh, University of Amsterdam Larisa Maksimova, Russian Academy of Sciences, Novosibirsk Hiroakira Ono, Japan Advanced Institute of Science and Technology Rohit Parikh, City University of New York Lazare Zambakhidze, Tbilisi State University ORGANIZATIONAL COMMITTEE: Merab Abashidze, Georgian Academy of Sciences Nick Arevadze, Georgian Academy of Sciences Nick Bezhanishvili, University of Amsterdam David Gabelaia, King's College Revaz Grigolia, Georgian Academy of Sciences Giorgi Japaridze, Villanova University Mamuka Jibladze, Georgian Academy of Sciences Ioseb Khutsishvili, Tbilisi State University Dimitri Pataraia, Georgian Academy of Sciences Levan Uridia, Tbilisi State University ORGANIZING INSTITUTIONS: New Mexico State University Tbilisi State University Georgian Academy of Sciences This conference is part of the activity of a grant funded by the Civil Research Development Fund and the Georgian Research Development Fund. For further information, contact Guram Bezhanishvili (gbezhani@nmsu.edu) or Pat Morandi (pmorandi@nmsu.edu). From rrosebru@mta.ca Fri Feb 28 13:54:30 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 28 Feb 2003 13:54:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18oocd-0001Mb-00 for categories-list@mta.ca; Fri, 28 Feb 2003 13:48:35 -0400 Message-ID: <3E5E51D6.9040609@mcs.le.ac.uk> Date: Thu, 27 Feb 2003 17:58:46 +0000 From: "A.Kurz" User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020623 Debian/1.0.0-0.woody.1 X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Lectureship positions Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 63 At the department of Mathematics and Computer Science of the University of Leicester are two lectureship postions available. They are advertised for the area of Software Engeneering but, to cite from the official announcement at http://www.le.ac.uk/personnel/jobs/a5549.html, "outstanding applicants with expertise in any related area of Computer Science are welcomed". Deadline is March 21. Many Greetings, Alexander -- http://www.mcs.le.ac.uk/~akurz From rrosebru@mta.ca Fri Feb 28 14:33:41 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 28 Feb 2003 14:33:41 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18opHE-0004FO-00 for categories-list@mta.ca; Fri, 28 Feb 2003 14:30:32 -0400 Message-ID: <20030227004049.57872.qmail@web12202.mail.yahoo.com> Date: Wed, 26 Feb 2003 16:40:49 -0800 (PST) From: Galchin Vasili Subject: categories: Topos: IL theorem prover To: categories@mta.ca 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: 64 Hello, Here is an intuitionistic logic theorem prover that might be interesting in light of the relationship of Heyting algebras to topoi: http://www.intellektik.informatik.tu-darmstadt.de/~jeotten/ileanTAP/ Regards, Bill Halchin From rrosebru@mta.ca Fri Feb 28 14:33:52 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 28 Feb 2003 14:33:52 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18opIY-0004Jf-00 for categories-list@mta.ca; Fri, 28 Feb 2003 14:31:54 -0400 Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Date: Fri, 28 Feb 2003 11:29:48 +0100 To: categories@mta.ca From: grandis@dima.unige.it (Marco Grandis) Subject: categories: Preprint: Adjoints for double categories X-OriginalArrivalTime: 28 Feb 2003 10:23:34.0968 (UTC) FILETIME=[732FCB80:01C2DF13] Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 65 The following preprint is available, in ps: M. Grandis - R. Pare=B4 Adjoints for double categories Dip. Mat. Univ. Genova, Preprint 476 (2003), 40 p. http://www.dima.unige.it/~grandis/Dbl.Adj.ps Abstract. After 'Limits in double categories' (Cahiers Topologie Geom. Differentielle Categ. 40 (1999), 162-220), we pursue our study of the general theory of weak double categories, addressing adjunctions and monads. A general 'double adjunction', which appears often in concrete constructions, has a *colax* double functor left adjoint to a *lax* one. This cannot be viewed as an adjunction in some bicategory, because lax and colax morphisms do not compose well and do not form one. However, such adjunctions live within an interesting construct, the strict double category of weak double categories, with horizontal and vertical arrows provided by the lax and colax double functors, respectively, and a suitable notion of double cell. Marco Grandis Dipartimento di Matematica Universita` di Genova via Dodecaneso 35 16146 GENOVA, Italy e-mail: grandis@dima.unige.it tel: +39.010.353 6805 fax: +39.010.353 6752 http://www.dima.unige.it/~grandis/