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.
====================================================