FMCS'04 Abstracts
On Combining Probabilistic and Nondeterministic Theories of Process Algebras
Guy Beaulieu
In this paper, we construct two factorizations of the set theoretic monad associated to the model category for a mixed choice algebra, i.e. an algebra which admits a nondeterministic and a probabilistic operator. In a set theoretic environment, the finite powerset functor models finite nondeterminism choice and there exists a functor which models discrete probabilistic choice. However, the composition of the above functors is not a monad. We show how one can obtain a monad which corresponds to the category of models of a mixed choice algebra, starting either with the powerset monad or the monad for probabilistic choice.
Undecidable constructions in two-dimensional categories
Robert Dawson
In computer science, a problem is usually considered to be "hard" if it cannot be solved in less than exponential time. Mathematicians, who do not have to pay for the numbers they use, may shamelessly exhibit algorithms with running times such as $O(e^{e^{e^N}})$. However, even mathematicians admit that a problem is hard if it is formally undecidable. (Of course, it was the computer scientist Alan Turing who really made this concept tractable.) This paper presents various examples of apparently straightforward constructions in two-dimensional category theory for which the problem of determining the equivalence of two elements is undecidable.
Rough sets
Jonathon Funk
Rough sets are an instance of the following 2 general constructions:
(1) If a comonad G and monad M in a category are mutually compatible in
the sense that `GM = MG' (similar to a distributive law for two monads),
then there is a naturally defined `Kleisli category' associated with the comonad-monad
pair.
(2) Any given category (usually small) has a so-called collage category,
following Johnstone and Carboni (this construction is itself an instance
of the ``twist category of a topos'' from Bunge-Funk, 1998).
Let (U,R) be a relational system (Pawlak): U is a set and R is a partial
order of equivalence relations on U. Then presheaves on the collage of the
partial order RxU supports a mutually compatible comonad-monad pair in the
above sense. We define the category of rough sets for (U,R) as the Kleisli
category for this comonad-monad pair in the presheaves on the collage of
RxU.
Range Restriction Categories
Xiuzhan Guo
Cockett and Lack's restriction categories provide a general framework for working with abstract categories of partial maps in which the notion of partiality is captured abstractly by a single combinator $\rst{(\;)}$ and four restriction axioms. In order to examine categories of partial maps in which not only is the domain of the partial map abstractly defined but also the image of the partial map, in this talk we shall introduce introduce range restriction categories and show their relationship with fibrations. (Joint with Robin Cockett.)
Polarized MALL and Double Gluing Hypercoherences
Masahiro Hamano
Polarized MALL (MALLP) is a fragment of Laurent's polarized linear logic without structural rules. In this talk, first, we discuss a categorical framework to model MALLP starting from positive/negative categories with polarity changing functors. Second, as concrete examples, we focus on Ehrhrad's hypercoherences and on double gluing construction over them. We discuss a polarized version of Joyal's softness, which proof-theoretically corresponds to a partial invertibility on certain connectives for positives. We show how the polarized softness together with a focalization property associates morphisms with Laurent's MALLP proof-structures. (A joint work with Phil Scott)
Inferring Types for Reference Sharing
Dana Harrington
We discuss type inference for a system which distinguishes between shared
and unshared values in a programming language. This type system allows the
reuse of storage for unshared values without compromising referential transparency.
The type inference algorithm uses data-flow analysis to detect reference
sharing, and to track which storage is to be reused. We show how the logical
proof structure generated by the inference process generates a model of the
categorical semantics of the system.
Partial Combinatory Algebras and Realizability Toposes
Pieter Hofstra
This lecture will consist of two parts. In part 1 we will introduce partial applicative structures, combinatory completeness and partial combinatory algebras (PCAs). To get a feel for the definition, some examples are given: term models, Kleene's recursion-theoretic PCA, the Graph Model, Engeler's graph algebra and Scott's D_\infty. Then we look at some facets of the theory of PCAs. In part 2 we construct a realizability topos from a PCA. This will be done in two steps: first we build a certain Set-indexed category called a tripos, and next we apply the so-called tripos-to-topos construction. Finally, some features of the resulting topos and the functoriality of the construction will be discussed.
Partial morphisms, fibrations, and database specifications
Michael Johnson
Database interoperations are vital for e-commerce, but designing interoperations, especially for already extant databases, is challenging. In particular, "attribute harmonisation" (AH) is usually required. This talk will explain why (basically AH is needed to ensure that certain arrows are pre-(op)-cartesian) as well as why AH is a bad thing in e-commerce applications. We then explore the use of notions of partial morphism in database specification and their interaction with cartesian-ness. It turns out that the notion of partial morphism *not* usually used in the database community is the one which allows automatic support for the universal properties required for catesian-ness and so avoids attribute harmonisation. (Joint work with Robert Rosebrugh and Kit Dampney, and in memory of Kit Dampney)
Multilevel Algebraic Structures
John Macdonald
Multilevel structures arise when monads or comonads on the 2-dimensional level are combined with similar structures on the 1-dimensional level. Specific examples of this phenomenon are presented from the work of the author and also from that of Tom Leinster. In particular we consider monads on the co-Kleisli category of a 2-comonad, including examples of parameterized monads, multicategories and operads.
Guarded Semigroups
Ernie Manes
When I read Cockett and Lack's paper "Restriction Categories I", I was taken with the absence of universal mapping properties in the definition. The object was to capture categories of partial maps and the approach was to append a new unary operation for the domain of a morphism (as a partial inclusion) with four equations that relate this operation to composition. Even identity morphisms were not mentioned. It looked to me like semigroup theory! And sure enough, a literature search reveals that some semigroup theorists had been moving in that direction. In this tutorial, I will discuss elementary semigroup theory and give the semigroup viewpoint on the progression beginning with groups through inverse semigroups, left ample semigroups, weakly left ample semigroups, semi-feeble marginally left ample semigroups and, finally, guarded semigroups. Part of the structure of a guarded semigroup is that of a strongly right normal band and I will show how these are represented as Kripke sets with global element. Time permitting, I will speculate on the impact of the rich Cockett-Lack-Guo category-theoretic results on semigroup issues as well as interactions between guarded semigroups and lattice-ordered groups.
System specifications and the View Update Model
Catherine Menon
In this talk we take a category theoretical approach to expressing the semantics of a general specification language, with examples taken from Rosetta, a language currently under development at Kansas University. We produce a category corresponding to a system specification, and use the view update model to analyse how an alteration in the state of one component of the system can affect the underlying system state. We provide a framework for specifying properties of systems which have a certain minimal amount of total change which occurs as a result of this partial update. Certain underlying system changes with minimal disruption to the system state are then considered canonical, and can be composed to produce a canonical simulation path.
Monad Constructions and Data Types
Phil Mulry
We outline some recent work related to developing a framework for monad constructions. Some examples associated with several data types will be introduced. Joint work with Ernie Manes.
Construction of the free braided pivotal category
David Oury
Two approaches are taken. The first is to describe the tangle category
of Freyd and Yetter (1989) and demonstrate the freeness property. The second
is to construct a formal strict monoidal category using generators and relations,
and show that it is in fact the free braided pivotal category. The formal
approach clarifies the creation of the braiding and pivotal structure within
a strict monoidal category.
A Process Interpretation of Additive Linear Logic
Craig Pastro
In this talk I will first show how formulas and proofs in additive linear logic (with the additive units) correspond respectively to protocols and processes. I will then give an interpretation of proofs as concurrent processes and derive its categorical semantics. Time permitting I will discuss current work which is adding the multiplicative fragment into our model and the problems we have encountered trying to do so. (Joint work with Robin Cockett.)
Universal Properties of Span
Doretta Pronk
First I will present the known universal property of Span in terms of sinister morphisms of bicategories as a restriction of the universal property of Pi_2 of a category. Then I will extend this to a new universal property involving the notion of paranormal morphisms between bicategories. This new notion does not require the existence of pullbacks in the original category and allows us to extend the Span( ) construction to arbitrary categories and even bicategories.
A categorical semantics for formal pragmatics
Kurt Ranalter
The logic of formal pragmatics extends classical logic to a logic of propositions and judgements. In this talk we will introduce shortly the philosophical principles underlying formal pragmatics and define a categorical semantics for the intuitionistic fragment of the logic. We will outline the relationship between the logic of formal pragmatics and other logics with mixed contexts and give an overview of possible directions for future research.
Logics for Context Free Grammars
Keith Rogers
In this talk we will introduce a logic for context free grammars, in which proofs correspond to inclusion between languages. Circular rules are used to represent infinite languages. We describe two logics with different styles of circular rules, and explore the relation between them.
Gluing
Andrea Schalk
Glueing is a technique frequently applied in categorical logic and topos theory. It is a special instance of a `comma category' where one functor is the identity. The construction deals well with the structure of a symmetric monoidal closed category, sums, products, and the like, in that if one starts with a category with (some of) this structure then the constructed category will also have it. However, when starting with a *-autonomous category there is no obvious way in which the result can be made *-autonomous as well; negation being the issue. Having looked at the standard glueing construction we will introduce `double glueing' which overcomes this problem. There are notes here.
Tutorial on the Geometry of Interaction and the dynamics of proofs
Philip Scott
Girard, in a fundamental series of three papers (GoI 1--GoI 3) beginning in 1988, introduced his Geometry of Interaction program. It develops a new kind of dynamic semantics in which proofs are modelled by operators in various C*-algebras and in which cut-elimination is given a new dynamic sense, in terms of a "feedback equation" known as the Execution Formula. Joyal-Street-Verity in their paper on Traced Monoidal Categories already observed that the GoI interpretation of CUT in Girard's models is related to composition in the compact closure of a traced monoidal category. This led Abramsky to a categorical framework ("GoI Situations") further developed by Esfan Haghverdi and me. But the original Girard papers GoI 1--GoI 3 (and his newest GoI 4 paper) have many deep mathematical details and fascinating insights not captured by pure GoI situations. I shall report on recent joint work with E. Haghverdi on a re-examination of Girard's GoI.
Towards a semantics for higher-order quantum computation
Peter Selinger
The search for a semantics for higher-order quantum computation leads naturally to the study of categories of continuous normed cones. In this talk, I will describe two such categories of cones, and the *-autonomous structure that they possess. I will also discuss why neither of these categories fully characterizes the higher-order quantum functionals (or even the probabilistic functionals, which arise as a special case). I will argue that, nevertheless, continuous normed cones are interesting objects to study, and that they are a likely a stepping stone on the way towards a fully complete semantics of higher-order quantum computation.
Introduction to Polarized Categories
Robert Seely
Motivated by an analysis of Abramsky-Jagadeesan games the talk will consider the categorical semantics of the polarized notion of two-player games. This semantics has a close connection with the logic of (finite cartesian) sums and products, as well as with the multiplicative structure of linear logic. The novel aspect is that the traditional categorical structures must be polarized, this in the sense that it is modelled by two categories, one for each polarity, connected by a module. The manner in which logical features can be polarized will be discussed (work with Robin Cockett).
Relating Church-style Typing and Curry-style Typing: Preliminary Report
Jonathan P. Seldin
There are two versions of type assignment in $\lambda$-calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called ``domain free''), in which it is not. As an example, in Church-style typing, $\lambda x : A . x$ is the identity function on type A, and it has type $A \rightarrow A$ but not $B \rightarrow B$ for a type $B$ different from $A$. In Curry-style typing, $\lambda x . x$ is a general identity function with type $C \rightarrow C$ for \emph{every} type $C$. In this paper, I will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style. (This generalizes some unpublished work with Garrel Pottinger.) I will then show how to interpret in a system of the Church-style (a modified PTS) every PTS-like system in the Curry style. I will also discuss the conditions under which each interpretation can be reversed.
Quantum typing
Benoit Valiron
In this talk we will see how to develop a functional programming language for quantum computers. Following the work of P. Selinger (2003) on quantum flow-charts, we will construct a lambda-calculus for the QRAM model, and define a call-by-value operational semantics together with a type system using affine intuitionistic linear logic. The main result of this talk will be the subject-reduction of the language. An inference algorithm is being built and may also be presented.
Build, Augment and Destroy. Universally.
Varmo Vene
We give a semantic footing to the fold/build syntax of programming with inductive types, covering shortcut deforestation, based on a universal property. Specifically, we give a semantics for inductive types based on limits of algebra structure forgetting functors and show that it is equivalent to the usual initial algebra semantics. We also give a similar semantic account of the augment generalization of build and of the unfold/destroy syntax of coinductive types. For augment, we show that it is definable for a much wider class of inductive types than has previously been recognized. (Joint with Neil Ghani and Tarmo Uustalu)
Finite-valued Approximations of Propositional Logics
Richard Zach
In contrast to many propositional logics, finite-valued logics are proof-theoretically
well-behaved and can computationally be dealt with relatively easily. This
suggests a study of methods for finding a finite-valued logic which "approximates"
a given logic, i.e., which has as few tautologies as possible, but which
includes all the valid formulas of the given logic among them. We investigate
how far this method can be carried using a single or an infinite sequence
of finite-valued logics. We show that the best candidate matrices for (1)
can be computed from a calculus, and how sequences for (2) can be found for
certain classes of logics (including, in particular, logics characterized
by Kripke semantics). (Joint work with Matthias Baaz)
