Resolution rewritings as cospans of cospans J. R. (Jim) Otto http://www.mcs.net/~quant/ Resolutions (in the logic programming sense) and term rewritings are fundamental techniques in computational logic and deal with, for example, definite Horn clauses and equations. We smoothly generalize definite Horn clauses and equations to maps in the opposites (Set^S)_fp of finite limits completions of small categories S. (The categories of Makkai sketches are essentially the Set^S with S Noetherian. Noetherian categories are called inverse categories in homotopy theory. For example, the opposites of ordinals are Noetherian.) We present the small finite limits categories (and dually the locally finitely presentable categories) by small finite fan-out Noetherian categories S and sets E of maps in (Set^S)_fp. With E' the closure of E under push outs, the small finite limits categories are (up to equivalence) the opposites of the categories of fractions (Set^S)_fp[E'^-1]. These categories of fractions are the collapses of weak n-categories whose 1-cells are resolutions (in the logic programming sense) and are certain (Set^S)_fp cospans and whose 2-cells are resolution rewritings and are certain cospans of cospans. While the category S expresses first order dependent types, that some of these types are relations or functions is expressed by some of the maps in E. Thus terms are some of the resolutions and resolution rewriting smoothly generalizes term rewriting. ======================================================== KINOSHITA Yoshiki Title: Lax logical relations for computational lambda calculus Abstract: Logical relations are found to be useful in many ways; so called "basic lemma for logical relations" makes us tempting to apply them even to data refinement as well; they are, however, not good as a basis for date refinement because they are not closed under composition. So, a few attempts, such as proposal of L-relations and that of lax logical relations, have been made, using category theoretic techniques, to find a class of relations which is closed under composition, but the basic lemma still holds. In this talk, we apply lax logical relations to E. Moggi's computational lambda calculus, which gives a neat basis for call-by-value programming languages, rather than a simply typed lambda calculus. This is joint work with John Power. ======================================================== \input amstex \documentstyle{amsppt} \topmatter \title Convergence structures for categories \endtitle \author Josef \v Slapal, Technical University of Brno \endauthor \endtopmatter \document In their paper [1], D. Dikranjan and E. Giuli introduced the concept of a closure operator for a category. (The theory of closure operators for categories has then been developed in the book [2] by D. Dikranjan and W. Tholen.) Roughly, a category with a closure operator is obtained as a generalization of $Top$ where topological spaces are considered as closure spaces (given by Kuratowski closure operators). But topological spaces can also be considered as convergence structures with the convergence expressed by nets. With this idea on mind, we introduce another generalization of $Top$, the notion of a category with a convergence structure. Some fundamental categorical and topological properties of these categories are investigated and relations between convergence structures and closure operators for categories are studied. \Refs \ref\no 1\manyby D. Dikranjan, E. Giuli\paper Closure operators I \jour Topology Appl.\vol 27\yr 1987\pages 129-143\endref \ref\no 2\manyby D. Dikranjan, W. Tholen\book Categorical Structure of Closure Operators\publ Kluwer Academic Publ.\publaddr Dordrecht-Boston-London\yr 1995\endref \endRefs \enddocument ======================================================== Noson Yanofsky "The Syntax of Coherence" Abstract We tackle categorical coherence within a two-dimensional generalization of Lawvere's functorial semantics. 2-theories, a syntactical way of describing categories with structure, are presented. From the perspective here afforded, many coherence results become simple statements about the quasi-Yoneda lemma and 2-theory-morphisms. Given two 2-theories and a 2-theory-morphism between them, we explore the induced relationship between the corresponding 2-categories of algebras. The strength of the induced quasi-adjoints are classified by the strength of the 2-theory-morphism. These quasi-adjoints reflect the extent to which one structure can be replaced by another. A two-dimensional analogue of the Kronecker product is defined and constructed. ======================================================== \documentclass[12pt]{article} \usepackage{fullpage} \begin{document} \thispagestyle{empty} \begin{center} {\large\em Geometry of Proofs and Full Completeness} \end{center} \vspace*{2ex} \begin{center} Esfandiar Haghverdi\\ Department of Mathematics\\ University of Ottawa\\ E-mail {\tt ehaghver@mathstat.uottawa.ca} \end{center} Girard introduced his Geometry of Interaction Programme (GoI) in a series of influential papers. The goal of this programme was to provide a mathematical analysis of the cut elimination process in linear logic proofs. This new interpretation replaces graph-rewriting by information flow in proof-nets. A specific model considered by Girard was based on the $C^*$-algebra of bounded linear operators on the space $\ell^2$. From a computational point of view this yields an analysis of $\lambda$-calculus $\beta$-reduction and has been applied in such areas as the analysis of optimal reduction strategies. GoI has also brought forward a new perspective for the semantics of computation which places it in a kind of ``middle ground'' between imperative/procedural, denotational/operational approaches in the semantics of programming languages. This new view helps to model the computational dynamics which is absent in denotational semantics and manages to offer a mathematical analysis which is lacking in operational semantics. In this talk we give a general categorical framework for the Girard programme inspired by recent work of Samson Abramsky. We show how to construct linear combinatory algebras and models of untyped combinatory logic in this framework. In particular, we will focus on combinatory algebras constructed using a special class of traced symmetric monoidal categories called {\em traced unique decomposition categories}. These categories provide an algebraic setting for an important class of examples and axiomatize the ``particle-style'' GoI. We also show how to construct models of multiplicative linear logic using the Int construction of Joyal, Street and Verity. We discuss the full completeness problem for such models, which amounts to a kind of representation theorem for free *-autonomous categories into GoI models. \end{document} ======================================================== John Duskin Title: " On the equivalence of bigroupoids and 2-dimensional hypergroupoids" Abstract: If C is a bicategory in the sense of Benabou, then it is possible to assign to C a simplicial set, the (geometric) nerve of C, in such a fashion that morphisms of bicategories define (semi-) simplicial maps of the corresponding nerves, and transformations and modifications define 1 and 2-dimensional homotopies. If all of the 2-cells of the bicategory are isomorphisms and all of the 1-cells are equivalences, i.e., if C is a bigroupoid , then its nerve is a Kan-complex which is a 2-dimensional hypergroupoid in the sense of Glenn. Somewhat surprisingly, any such 2-hypergroupoid ( i.e., any simplicial set in which all of the canonical maps from the set of n-simplices to any one of its horns are surjective if n =BE 2 and bijective for n > 2) is the nerve of a bigroupoid which is unique up to a choice of its composition tensor. Under this correspondence, (semi-) simplicial maps correspond to morphisms with 1-and 2- homotopies corresponding to transformations and modifications, respectively. The proofs of these results are delicate with the associativity isomorphisms and their pentagonal coherence resulting from the interaction of the (algebraic) 2-hypergroupoid conditions with the (geometric) simplicial identities. They directly generalize the result which asserts that a 1-dimensional hypergroupoid is just the nerve of a groupoid in which the corresponding coherence condition is just that of associativity. In both cases the proofs are made perspicuous by the modification of a novel "simplicial matrix technique" originally developed by Glenn. They give some hope that the same techniques may be useful in higher dimensions as well since an n-dimensional hypergroupoid is exactly what one obtains when one takes a Kan-complex (such as the singular complex of a topological space) and replaces the set of n-simplices with the set of equivalence classes under homotopy relative to the boundary. ============================================ Hongde Hu Title: Total graphs coloring Abstract: The connection between P_{4}-free graphs and objects of free bicompletions of categories has been recently studied in several papers. Here we give an intrinsic characterization of P_{4}-free graphs in connection with total graphs. We prove that the chromatic number of a total graph is equal to its clique number. We therefore obtain that every P_{4}-free graph is perfect. =============================================== Luigi Santocanale: Free $\mu$-lattices. ABSTRACT: A $\mu$-lattice is a lattice with the property that every unary polynomial with coefficients in it has both a least and a greatest fix-point. In this talk I'll define the category of $\mu$-lattices and for a given partially ordered set $P$ I'll show how to construct a $\mu$-lattice ${\cal J}_{P}$ by means of games. Also I'll discuss how to prove that the order relation of ${\cal J}_{P}$ is decidable, given that the order relation of $P$ is decidable. The $\mu$-lattice ${\cal J}_{P}$ is actually free over the partially ordered set $P$. I'll discuss the proof of freeness and explain why it suggests circular proofs as good models of proofs. ==================================================== Dusko Pavlovic Minimal (Dedekind-MacChu) bicompletion of a category Abstract. The minimal bicompletion of a category preserves all limits and colimits that may already exist in it. For posets, the minimal bicompletion is provided by the Dedekind-MacNeille construction. The question of its categorical generalization has been raised in Lambek's 1966 monograph on "Completions of categories". We provide an answer, which turns out to be closely related to Barr's work on the Chu construction. ====================================================