Seminars of the CENTRE de RECHERCHE en THEORIE des CATEGORIES CATEGORY THEORY RESEARCH CENTER C ---------> R | / | | / | | / | | / | v / v T ---------> C Tuesday 10 January 1995 2:30 - 4:00 pm Paul Cherenack (South Africa) `Smooth homotopy theory'. The talk will be about homotopy theory in the category of smooth spaces, a category considered by Lawvere and Schanuel and developped mainly by Frolicher. Tuesday 17 January 1995 2:30 - 4:00 pm M. Barr (McGill) "Two Easy Pieces" ABSTRACTS: 1. Recently, Ed Keenan gave a talk here in which he discussed a "theorem" of Putnam's that claimed that an n-ary relation on a set could *never* be characterized by a set of first order equations (in a language without equality) unless it was empty or total. Keenan showed by example that the binary relation of equality (or inequality) on a 2 element set was a counter-example and conjectured that there were counter-examples for any finite set. He also raised the question about finite sets. I will show that on a finite set, it is precisely the relations definable by equality and inequality that can be characterized by first order sentences and that Putnam's original theorem (though not his proof) is valid for infinite sets. 2. Recently, Rick Blute gave a talk here in which he discussed a *-autonomous category of topological vector and credited me with the assertion that the underlying functor to discrete vector space preserved the tensor product. It is true that I had made some such general assertion, involving Chu spaces, more precisely the subcategory of separated, extensional Chu spaces, but that assertion was wrong in that the tensor product of separated Chu spaces, though extensional, was not necessarily separated. I will show this by counter-example for abelian groups and also show that, for vector spaces, the tensor product of separated spaces is separated. Tuesday 24 January 1995 2:30 - 4:00 pm M. Bunge (McGill) "Paths versus coverings in defining the fundamental group of a topos." (Joint with Ieke Moerdijk; in progress) Tuesday 31 January 1995 2:30 - 4:00 pm G. Janelidze (Math Inst Georgia Acad Sci) "Internal categories in algebraic categories" Tuesday 7 February 1995 2:30 - 4:00 pm J. Funk (McGill) "The Lower Power Locale" (Joint with M. Bunge) Tuesday 14 February 1995 2:30 - 4:00 pm M. Makkai (McGill) "First order logic with dependent types, and categories" Tuesday 21 February 1995 2:30 - 4:00 pm J. Otto (McGill) "dependent products, Church numerals, fibrations, bounded alternations, linear space, P time, linear time, P space, and log space." Tuesday 28 February 1995 2:30 - 4:00 pm M. Markl (Prague) "DISTRIBUTIVE LAWS AND THE KOSZULNESS OF OPERADS" Tuesday 7 March 1995 2:30 - 4:00 pm M. Makkai (McGill) "First order logic with dependent types (Part II)" Tuesday 21 March 1995 2:30 - 4:00 pm Franck van Breugel (McGill) From Branching to Linear Metric Domains (and back) ABSTRACT Besides partial orders, also metric spaces have turned out to be very useful to give semantics to programming languages. In the literature, one encounters two main classes of metric domains: linear domains and branching domains. Linear domains were already studied by topologists in the early twenties. Branching domains have been introduced by, e.g., De Bakker and Zucker, and Golson and Rounds. The elements of these linear and branching domains are convenient to model---one might even say that they represent---trace equivalence classes and bisimulation equivalence classes, respectively. Linear domains are more abstract than branching domains. Our aim is to show that linear domains can be embedded in branching domains. We focus on the branching domain introduced by De Bakker and Zucker and the linear domain the elements of which can be viewed as nonempty and compact sets of sequences. We follow the work of Nielsen and Winskel et al. using category theory to classify the domains. The linear and branching domains are both turned into a quasimetric space which induces a preorder and hence a category. The quasimetrics are obtained from the metrics the domains are endowed with by dropping one half of the Hausdorff metric. The morphisms of the branching domain can be seen as simulations and the morphisms of the linear domains can be viewed simply as inclusion functions. The linear and branching domains are related by a reflection and a coreflection. Tuesday 28 March 1995 2:30 - 4:00 pm J. Otto (McGill) "Orthogonal Hulls by Resolution and Paramodulation" Tuesday 4 April 1995 2:30 - 4:00 pm Alan Jeffrey (Sussex) A fully abstract semantics for a higher-order functional concurrent language ABSTRACT This talk is about the relationship between the theory of monadic types and the practice of concurrent functional programming. I will present a typed functional programming language CMML, with a type system based on Moggi's monadic metalanguage, and concurrency based on Reppy's Concurrent ML. I will then present an operational semantics for the language, and describe some results about finding fully abstract semantics for may testing. Finally, I shall mention the relationship between CML and CMML, and describe some work in progress. Tuesday 11 April 1995 1:00 - 2:30 pm David Spooner (Calgary) "Interaction categories as categories of spans" 3:00 - 4:30 pm Wilfried Sieg (Carnegie-Mellon U.) "K-Graph Machines and Turing's Thesis" Tuesday 18 April 1995 2:30 - 4:00 pm W Boshuck (McGill) Descent for pretoposes and (Barr-)exact categories Abstract: I will present a short model-theoretic proof of Zawadowski's descent theorem for pretoposes, as well as an elementary argument deducing the descent theorem for (Barr-)exact categories from the descent theorem for pretoposes. Tuesday 2 May 1995 2:30 - 4:00 pm H Kiersted Recursive graph colouring Tuesday 16 May 1995 2:30 - 4:00 pm D Pavlovic (Imperial College) On categories of processes, actions, and interactions ABSTRACT Deep categorical analyses of various aspects of concurrency have been developed, but a uniform categorical treatment of the very first concepts seems to be hindered by the fact that the existing representations of processes as bisimilarity classes do not provide an account of computationally relevant morphisms. I shall first describe a universal construction of a "category of processes" over an arbitrary allegory with an abstract "notion of simulation". Instanciating to transition systems with respectively strong, weak, branching simulations, we get three actual categories of processes. However, their objects, as well as the morphisms, are given as large, hardly manageable equivalence classes. The canonical representatives are then effectively calculated as terminal coalgebras. On these representatives, the bisimilarity preserving simulations boil down to ordinary graph morphisms. In the setting of thes categories of processes, the operations on processes, as displayed in Abramsky's interaction categories, yield to a logical analysis. If the time permits, I shall finally discuss connections with Milner's action calculi, particularly the fenomenon of the "functional completeness" with respect to the names. ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Tuesday, 13 June 1995 2:30 - 4:00 pm J. Otto (McGill) Work in progess on complexity doctrines and orthogonal hulls Tuesday, 29 August 1995 1:30 - 3:00 Franz-Viktor Kuhlmann (U. Heidelberg) "What do we know about power series fields in positive characteristic?" 3:30 - 5:00 Salma Kuhlmann (U. Heidelberg) "What do we know about exonential power series fields?" Tuesday, 12 September 1995 2:30 - 4:00 M. Barr (McGill) Chu categories (work in progress) Tuesday, 19 September 1995 2:30 - 4:00 RAG Seely (McGill) Categories with general context Tuesday, 26 September 1995 2:00 - 3:00 C Hermida (McGill) Indeterminates and Kleisli Objects ABSTRACT: It is well-known (cf. Lambek and Scott's book) that for a cartesian/cartesian closed/distributive category C, the category C[x:I] obtained by adding an indeterminate (global element) x:1->I can be identified with the Kleisli category of the comonad - x I. Upon proving this result in its natural level of generality (in any 2-category admitting finite products and Kleisli objects subject to a mild exactness condition), we formulate two associated concepts: contextual and functional completeness. Contextual completeness amounts to the possibility to interpret contexts in the category, while functional completeness amounts to the possibility to internalize the `polynomial expressions' (morphisms of C[x:I]) in C. For the abovementioned kind of categories, functional completeness amounts to cartesian closure (in a non-tautological way). We then show the relevance of these concepts to formulate `parametrization' properties of say NNO (in fact, of initial algebras of polynomial endofunctors). As far as time allows, we present the technically more involved specialization of the above concepts to the 2-category Fib of fibrations over arbitrary bases and explain their logical significance in this setting. The work in the talk is joint with Bart Jacobs and should appear shortly in MSCS. Tuesday, 10 October 1995 2:30 - 4:00 Prakash Panangaden (McGill) Stochastic Transition Systems Saturday, 14 October - Sunday, 15 October, 1995 OKTOBERFEST Meeting Details at ftp://triples.math.mcgill.ca/pub/rags/oktoberfest.html and are announced regularly on CATEGORIES net-list. Tuesday, 17 October 1995 2:30 - 4:00 Beno Eckmann (ETH) 4-manifolds and group invariants Tuesday, 24 October 1995 2:00 - 3:00 C Hermida (McGill) Structural induction and coinduction I (joint with Bart Jacobs) 3:00 - 3:30 coffee 3:30 - 4:30 C Hermida (McGill) Structural induction and coinduction II ABSTRACTS: Part I: Fibrations and Logical Predicates We review the notion of (Grothendieck) fibration as a framework for (proof- relevant) predicate logic. The so-called logical predicates come about as a logical description of some categorical structure of the total category of a fibration, eg. products and exponentials. Such structure is crucial in formulating a suitably abstract version of structural induction and coinduction for initial algebras and final coalgebras in Part II. We review also the interpretation of first-order logic connectives and quantifiers in a fibration (with suitable structure), and related concepts: comprehension, equality and quotients. Part II: (Co)induction principles for (co)initial (co)algebras Using the above setup of predicate logic in a fibration, we categorize the induction principle for the initial algebra of a polynomial endofunctor in the base category. The base category is thought of as types and terms, and the initial algebra as a datatype. The associated induction principle asserts the initiality of a canonically determined algebra for an endofunctor on the total category (the endofunctor being also canonically determined by the given one in the base). In short, induction amounts to an exactness condition on a functor between categories of algebras. We then show that comprehension entails induction (as is routinely shown in Sets). Dualising the above we have a coinduction principle for final coalgebras. And putting both principles together, we get a mixed induction/coinduction principle for mixed variance functors (using Freyd's trick). These latter principle is shown to hold in the presence of comprehension and quotients. All the proofs are immediate consequences of the (known) characterisation of the category of algebras for an endofunctor as inserters (a simple kind of 2-categorical limit). Tuesday, 31 October 1995 2:30 - 4:00 M. Makkai (McGill) Bisimulations and Logic Tuesday, 7 November 1995 2:30 - 4:00 J. Funk (McGill) The Radon-Nikodym derivative of a measure on a Grothendieck topos Abstract: We associate to an arbitrary (Lawvere) measure on a locally connected topos an object of the topos which plays the role of its Radon-Nikodym derivative. Tuesday, 14 November 1995 2:30 - 4:00 M. Bunge (McGill) Comprehension for Measures Tuesday, 28 November 1995 3:00 - 4:30 S. Sawin (MIT) Quantum Field Theory, Topology and Functors Tuesday, 5 December 1995 2:30 - 4:00 M. Barr (McGill) Chu revisited PLACE: BURNSIDE HALL 920, McGILL UNIVERSITY (COOKIES AND COFFEE AS USUAL AFTER THE TALK)