Seminars of the CENTRE de RECHERCHE en THEORIE des CATEGORIES CATEGORY THEORY RESEARCH CENTER C ---------> R | / | | / | | / | | / | v / v T ---------> C Tuesday, 23 January 1996 2:30 - 4:00 F. van Breugel (McGill) Generalized Ultrametric Spaces: completion, topologies, and powerdomains ABSTRACT by Franck van Breugel (joint work with Marcello Bonsangue and Jan Rutten) Generalized ultrametric spaces are a common generalization of preorders and ordinary ultrametric spaces. In terms of (an ultrametric version of) the categorical Yoneda embedding we construct 1. completion, 2. topologies, and 3. powerdomains for generalized ultrametric spaces. Restricted to the special cases of preorders and ordinary ultrametric spaces, these constructions yield, respectively 1. omega-chain completion and Cauchy completion, 2. the Alexandroff and the Scott topology, and the epsilon-ball topology, 3. the Hoare, Smyth, and Plotkin powerdomains, and the Vietoris hyperspace. As an illustration of the use of the theory in semantics, a domain for `quantitative' simulation is constructed. Tuesday, 30 January 1996 2:30 - 4:00 R. Blute (U. Ottawa) A Noncommutative Full Completeness Theorem. Tuesday, 6 February 1996 2:30 - 4:00 S. Finkelstein (McGill) A new framework for declarative programming I Tuesday, 13 February 1996 2:30 - 4:00 S. Finkelstein (McGill) A new framework for declarative programming II Tuesday, 20 February 1996 2:30 - 4:00 P.J. Scott (Ottawa) Solving Word Problems for Cartesian Closed Categories using Yoneda Embeddings; or "Eliminating Cut Elimination" Tuesday, 5 March 1996 2:30 - 4:00 M Makkai (McGill) On James Dolan's definition of a weak n-category Tuesday, 12 March 1996 2:30 - 4:00 R. Squire (McGill) An application of the Cantor Bendixon derivative to a duality between a category of posets and a category of completely distributive Heyting algebras Tuesday, 19 March 1996 2:30 - 4:00 M Makkai (McGill) On James Dolan's definition of a weak n-category II Tuesday, 23 April 1996 2:30 - 4:00 J. Benabou (Paris) Principes de connaissance et analyse non-standard Tuesday, 30 April 1996 2:30 - 4:00 J. Otto From functionality within logic programming to arithmetic, higher types, and finite models ABSTRACT: First order signatures usefully generalize to small Noetherian categories with finite fan-out Sig. Then the objects of set^{Sig} can be thought of as formulas or Makkai sketches and the maps as clauses or sequents. Resolutions are then cospans d : --> <-- : i in set^{Sig} with d a deduction and i a partial answer. This includes paramodulation and unification and recalls right existence introduction. In so presenting N 0 : N s x : N [x : N] x + y : N [x : N, y : N] 0 + y = y : N [y : N] (s x) + y = s (x + y) : N [x : N, y : N] one obtains functional resolution of queries such as 1 + 1 = ? by eliminating some syntactic and equational axioms. Simple types can be so presented as certain fibrations with 2-comprehension. Expanding a linear time doctrine with fibrations and tier 0 rank 1 types may characterize the log time hierarchy and thus connect finite models and bounded recursion characterizations of complexity classes. Tuesday, 7 May 1996 12:30 - 2:00 C. Pedicchio (Trieste) Internal groupoids and commutators. 2:30 - 4:00 J. Power (Edinburgh) Categories enriched in bicategories. Tuesday, 14 May 1996 11:00 - 12:30 M. Okada (Keio) Generalized Phase Semantics, Strong Normalization, and Concurrency Models Abstract: We consider a uniform framework to analyse provability, proofs and (concurrent) processes, based on a generalized phase semantics of Linear Logic. First we show that Tait-Girard's computability (and candidates of reducibility) argument for the (higher order) strong normalizability proofs can be characterized by a phase-semantic completeness proof. We also show that, in some interesting frameworks, the safe concurrent processes for a given formal specification can be characterized by a phase-semantic completeness proof (for a suitable fragment of Linear Logic). Wednesday, 22 May 1996 2:30 - 4:00 R. Cockett (Calgary) Shape Rings Abstract: A shape ring is a functorial structure on a lextensive category which is equivalently provided by an internal full subcategory with certain colimit structure. This internal category can be viewed as playing the role of finite sets and provides, through its accompanying functorial stucture, the basis for building datatypes. These datatypes do not satisfy a universal property and thus allow the categorical modelling of sub-primitive recursive functions. Tuesday, 4 June 1996 2:30 - 4:00 R. Squire (McGill) A course-of-values induction principle for K-finite sets Abstract: In a recent paper on K-finite sets in the setting of intuitionistic type theory, Andreas Blass established a useful induction principle, whereby, in order to establish that a property holds for all finite subsets of a set $U,$ one assumes the property for all complemented, proper subsets of an arbitrary finite subset $X,$ then proves the property for $X.$ He then raised the question of whether the principle would remain valid if "complemented " were replaced by "finite". We settle this question and other possible variants, by proving an optimal course-of-values induction principle. Tuesday, 11 June 1996 2:30 - 4:00 Kira Adaricheva. "The problem of Birkhoff-Mal'cev: overview and recent results" ABSTRACT This talk will deal with the problem of characterization of lattices of universal Horn theories, or lattices of quasivarieties raised independently by G.Birkhoff and A.I.Mal'cev, and the progress in its solution made by the author, V.Gorbunov and W.Dziobiak during several last years. Tuesday, 18 June 1996 2:30 - 4:00 R. Guitart (Paris VII) Introduction `a la logique spe'culaire: en relation avec la logique intuitioniste et co-intuitioniste, la dualite' de Stone, et la cohomologie non-abe'lienne (Apologies for the weird accents - the WWW site has the correct syntax. I am not satisfied with any of the usual ASCII solutions...) Tuesday, 25 June 1996 C A N C E L L E D 2:30 - 4:00 C. Casadio (Bologna) Extension of the Lambek calculus to non-commutative classical linear logic: negation vs duality Wednesday, 26 June 1996 C A N C E L L E D 2:30 - 4:00 C. Casadio (Bologna) Application of the Lambek calculus to natural language (Italian, in particular) Friday, 28 June 1996 C A N C E L L E D 2:30 - 4:00 C. Casadio (Bologna) Application of the extended calculus to Romance languages: interaction of cliticization and negation Tuesday, 25 June 1996 2:30 - 4:00 Dusko Pavlovic Descent and tripleability without the Beck-Chevalley condition Abstract. The Beck-Benabou-Roubaud theorem says that a morphism under a bifibration with the Beck-Chevalley property is of effective descent whenever the induced inverse image functor is tripleable. This is an important tool of the descent teory, and it has actually motivated Beck to characterise tripleable functors in the first place. I shall show that this theorem, in essence, holds without the Beck-Chevalley property, and for arbitrary fibrations: a morphism in the base is of effective descent if and only if the induced inverse image functor satisfies the tripleability criteria minus the left adjoint (i.e., reflects the isos, and the coequalisers of the contractible cartesian pairs over its kernel). Wednesday, 26 June 1996 2:30 - 4:00 Richard Squire K-finiteness ==> Dedekind finiteness Abstract: An object is said to be Dedekind finite if every monic endomorphism is an automorphism. It is known (Acuna-Ortega, 1992) that a decidable K-finite object is Dedekind finite. We show that the theorem holds without the decidability assumption. Advance notice: Tuesday, 3 September 1996 C A N C E L L E D 1:30 & 3:00 Salma Kuhlmann and Franz Kuhlmann TBA Tuesday, 13 August 1996 2:30 - 4:00 H.-J. Hoehnke CATEGORIES, FRACTEGORIES, FRACTAL LAX FUNCTORS Tuesday, 10 September 1996 2:30 - 4:00 Victor Harnik 'Pushouts and tensor products of categories' Abstract: We work in the (2-)category of categories with arbitrary small coproducts and finite products that distribute over the coproducts. We describe pushouts in this category as tensor products. The idea comes, of course, from a classical construction in linear algebra and was used by Joyal-Tierney in their study of the category of posets called 'frames'. As an application, we generalize one of their theorems. Tuesday, 24 September 1996 2:30 - 4:00 John Power 'Premonoidal categories' Tuesday, 22 October 1996 2:30 - 4:00 Claudio Hermida 'FIB as a 2-fibration' ABSTRACT: We present some analysis of the 2-category of fibrations (over arbitrary bases) as an instance of a 2-fibration over Cat. We contend this point of view is very useful for proving properties of fibrations themselves. The main intrinsic property we present is a factorization of adjunctions, which is fairly basic to infer known (and new?) results about fibrations themselves, eg. Benabou's characterization of `fibrations over fibrations'. Time allowing, we touch upon the applications to the interpretation of logical predicates. Tuesday, 29 October 1996 2:30 - 4:00 Thomas Mackling (McGill) A Recent Discovery in Binary Clausal Resolution/Refutation Theorem-Proving ABSTRACT: We present a new restriction on ordinary binary merge resolution, called ``predicate colouring'', (PCL), which essentially involves restricting resolution to <=-maximal predicate names, where <= is an arbitrary fixed partial order on predicate names. We show its refuation-completeness in the ground/propsitional case, and sketch the proof (obtained by ``lifting'') for the predicate case. We then present the ``discovery'': without significant modification the (quite straight-forward) proof of the ref-comp. of PCL also shows ref-comp. of a much more restrictive system,``signed predicate colouring'' , (SPCL), in which essentially, the predicate name partial order, <=, is replaced by an arbitrary, fixed, partial order on SIGNED predicate names. We will briefly touch upon how SPCL generalizes some other similar restrictions (as in ``hyper-resolution''), and some ramifications. Tuesday, 5 November 1996 Left clear (no seminar) so folks can attend Leon Henkin's talk at Universite de Montreal "Logical Completeness and Decidability" 4:00, salle 6214, Pav. Andre Aisenstadt (2920 ch. de la Tour) Tuesday, 19 November 1996 2:30 - 4:00 Vladimir Lyubashenko (Kansas State) "Ribbon Hochschild homology via operads" Thursday, 5 December 1996 2:30 - 4:00 Robin Cockett, University of Calgary Understanding linear structure: a matter of choosing the right 2-category? Abstract: Linearly (aka. weakly) distributive categories express precisely the categorical proof theory of the cut rule between two associative connectives in the (two-sided) sequent calculus. The coherence diagrams are exactly those required to permit cut-elimination. Upon this foundation, therefore, one should be able to build, in a modular fashion, the categorical proof theories for logics with more elaborate features. The logistics, however, of such a programme look quite forbidding. The axiomatization of linearly distributive categories already requires some two dozen coherence diagrams. To capture the proof theory of the exponentials (bang and whimper), one must add a further two dozen diagrams. The additives, as shall be discussed, result in a similar salutary dose of coherence. Clearly when the definition of categorical structure requires such a large number of coherence diagrams it is essential to have a reliable method of generating the diagrams. The key to this, I claim, lies in choosing the right notion of linear functor and transformation. For, with the right notion, these additional features can be seen (rather simply) as functorial structure. I will be describing joint work with Rick Blute and Robert Seely. The aim of work has been to elucidate the coherence results for these settings. I suggest that this new view of linear structure facilitates this programme as the functorial structure itself already permits a coherence theorem. This suggests there may be a more modular approach to establishing coherence theorems for these settings. (Aside: it is disappointing to note that proofs viewed as programs (e.g. maps of a distributive category) already fail to satisfy cut-elimination when $\times$ and $+$ are taken to be the connectives. This means that the proof theory of the and/or fragment of logic expressed intuitionistically (as sequents in which the right side is required to be a single proposition) is significantly different from the proof theory of it's expression as a two-sided sequent calculus.) COFFEE as usual after the talk PLACE: BURNSIDE HALL 920, McGILL UNIVERSITY