Concurrent Realizations of Reactive Systems
by Marek Bednarczyk, Andrzej Borzyszkowski
Abstract:
The problem of finding a (functorial) concurrent realization of a
reactive system by means of a labelled safe Petri net is studied.
Firstly, a (functorial) construction is described that leads from
the category of concrete asynchronous systems introduced by Morin to
the category of labelled safe Petri nets.
Then, the general problem is discussed. It is indicated that in
general there are no optimal solutions, i.e., that the most
concurrent realizations of a reactive system need not exist.
Nevertheless, a framework to support the process of building
a concurrent realization of a reactive system is presented.
Functorial semantics for Petri nets under the individual token
philosophy
by Roberto Bruni, José Meseguer, Ugo Montanari, Vladimiro Sassone
Abstract:
Although the algebraic semantics of place/transition Petri
nets}under the collective token philosophy has been fully
explained in terms of (strictly) symmetric (strict) monoidal
categories, the analogous construction under the individual
token philosophy is not completely satisfactory because it lacks
universality and also functoriality. We introduce
the notion of pre-net to recover these aspects, obtaining a
fully satisfactory categorical treatment centered on the notion
of adjunction.
This allows us to present a purely logical description of net
behaviours under the individual token philosophy in terms of theories
and theory morphisms in partial membership equational logic,
yielding a complete match with the theory developed by the authors
for the collective token view of nets.
Equational Lifting Monads
by Anna Bucalo, Carsten Führmann, Alex Simpson
Abstract:
We introduce the notion of an "equational lifting monad": a commutative
strong monad satisfying one additional equation (valid for monads
arising from partial map classifiers). We prove that any equational
lifting monad has a representation by a partial map classifier such that
the Kleisli category of the former fully embeds in the partial category of
the latter. Thus equational lifting monads precisely capture the
(partial) equational properties of partial map classifiers. The
representation theorem also provides a tool for transferring non-equational
properties of partial map classifiers to equational lifting monads.
Structured Theories and Institutions
by Francisco Durán, José Meseguer
Abstract:
Category theory provides an excellent foundation for studying
structured specifications and their composition. For example, theories can be
structured together in a diagram, and their composition can be obtained as a
colimit. There is, however, a growing awareness, both in theory and in
specification practice, that structured theories should not be viewed just as
the "scaffolding" used to build unstructured theories: they should become
first-class citizens in the specification process. Given a logic
formalized as an institution I, we therefore ask whether there is a good
definition of the category of I -structured theories, and whether they can be
naturally regarded as the ordinary theories of an appropriate institution S(I)
generalizing the original institution I. We answer both question in the
affirmative, and study good properties of the institution I inherited by
S(I). We show that, under natural conditions, a number of important properties
are indeed inherited, including cocompleteness of the category of theories,
liberality, and extension of the basic framework by freeness constraints. The
results presented here have been used as a foundation for the module algebra
of the Maude language, and seem promising as a semantic basis for a generic
module algebra that could be both specified and executed within the logical
framework of rewriting logic.
Coalgebra-to-Algebra Morphisms
by Adam Eppendahl
Abstract:
Given a coalgebra p for HG, an algebra s for GH and the obvious notion
of morphism from coalgebra to algebra, we observe that morphisms from
Gp to s correspond to morphisms from p to Hs in the manner of an
adjunction even when there is no adjunction between G and H. This
appears to be one of the basic phenomena underlying the transport of
special algebras. A proof of Freyd's Iterated Square Theorem
illustrates the interaction with Lambek's Lemma.
On the Semantics of Message Passing Processes
by Lindsay Errington
Abstract:
Let J be a shape in some category Shp for which there is a functor
k : Shp -> Cat. A categorical transition system (or system) is a
pair (J, k(J) -> C) consisting of a shape labelled by a functor in a
category in C.
Systems generalize conventional labelled transition systems. By
choosing a suitable universe of shapes, systems can model concurrent
and asynchronous computation. By labelling in a category, rather than
an alphabet or term algebra, the actions of an algorithm or process can
have structure.
We study a class of systems called twisted systems having the form
(J, F\tw(J) -> C) where J is a reflexive graph and \tw(-) : RGrph ->
RGrph
is the twisted graph construction. The relevance of twisted
systems lies in the relationship between twists and spans. A functor
FJ -> Sp(C) into a bicategory of spans is equivalent to a functor
F\tw(J) -> C.
The connection with spans means that when the target category C = Set,
then following Burstall, a twisted system can be viewed as a
generalized flow-chart. The theory extends to modeling interacting
processes. If U is a system, then a process of type U is a system S
and a morphism p : S -> U. The system U represents the interface to
the process. It describes what can be observed and what the process
offers to the environment for interaction. The system S describes the
internal behaviour of the process and the morphism p describes how S
realizes observable behaviour. Processes compose by pullback over a
common interface.
A Fully abstract presheaf semantics for SCCS with finite delay
by Thomas Hildebrandt
Abstract:
We present a presheaf model for the observation of infinite as well
as finite computations. We apply it to give a denotational semantics
of SCCS with finite delay, in which the meanings of recursion are
given by final coalgebras and meanings of finite delay by initial
algebras of the process equations for delay. This can be viewed as a
first step in representing fairness in presheaf semantics. We give a
concrete representation of the presheaf model as a category of
generalised synchronisation trees and show that it is coreflective in
a category of generalised transition systems, which are a special case
of the general transition systems of Hennessy and Stirling. The open
map bisimulation is shown to coincide with the extended bisimulation
of Hennessy and Stirling. Finally we formulate Milners operational
semantics of SCCS with finite delay in terms of generalised transition
systems and prove that the presheaf semantics is fully abstract with
respect to extended bisimulation.
Abstract Games for Linear Logic
by Martin Hyland, Andrea Schalk
Abstract:
We draw attention to a number of constructions which lie behind many
concrete models for linear logic; we develop an abstract context for
these and describe their general theory. Using these constructions we
give a model of classical linear logic based on an abstract notion of
game. We derive this not from a category with built-in computational
content but from the simple category of sets and relations. To
demonstrate the computational content of the resulting model we make
comparisons at each stage of the construction with a standard very
simple notion of game. Our model provides motivation for a less
familiar category of games (played on directed graphs) which is
closely reflected by our notion of abstract game. We briefly indicate
a number of variations on this theme and sketch how the abstract
concept of game may be refined further.
Internal Languages for Autonomous and *-Autonomous Categories
by T W Koh and C-H L Ong
Abstract:
We introduce a family of type theories as internal languages for
autonomous (or symmetric monoidal closed) and *-autonomous categories, in
the same sense that the simply-typed lambda-calculus with surjective
pairing is the internal language for cartesian closed categories. The
rules for the typing judgements are presented in the style of Gentzen's
Sequent Calculus. A notable feature is the systematic treatment of
naturality conditions by expressing the categorical composition, or cut in
the type theory, by explicit substitution. We use let-constructs, one for
each of the three type constructors tensor unit, tensor and linear
function space, and a Parigot-style mu-abstraction to express the
involutive negation. We show that the eight equality and three commutation
congruence axioms of the *-autonomous type theory characterise
*-autonomous categories exactly. More precisely we prove that there is a
canonical interpretation of the (*-autonomous) type theories in
*-autonomous categories which is complete i.e. for any type theory, there
is a model (i.e. *-autonomous category) whose theory is exactly that. The
associated rewrite systems are all strongly normalising; modulo a simple
notion of congruence, they are also confluent. As a corollary, we solve a
Coherence Problem a la Lambek: the equality of maps in any *-autonomous
category freely generated from a discrete graph is decidable.
Dependent Coercions
by Zhaohui Luo and Sergei Soloviev
Abstract:
A notion of dependent coercion is introduced and studied in the
context of dependent type theories. It extends our earlier work on
coercive subtyping into a uniform framework and increases
significantly the expressive power with new applications.
A dependent coercion introduces a subtyping relation between a type
and a family of types in that an object of a type is mapped into one
of the types in the family. We present the formal framework and
discuss applications such as its use in functional programming with
dependent types. Dependent coercions also make it possible to
represent some mathematical constructions such as coverings.
Precategories for combining probabilistic automata
by Paulo Mateus, Amílcar Sernadas, Cristina Sernadas
Abstract:
A relaxed notion of category is presented having in mind the categorical
caracterization of the mechanisms for combining probabilistic automata,
since the composition of the appropriate morphisms is not always defined.
A detailed discussion of the required notion of morphism is provided. The
partiality of composition of such morphisms is illustrated at the abstract
level of countable probability spaces. The relevant fragment of the
theory
of the proposed precategories is developed, including (constrained)
products and Cartesian liftings. Precategories are precisely placed in the
universe of neocategories. Some classical results from category theory are
shown to carry over to precategories. Other results are shown not to hold
in general. As an application, the precategorical universal constructs are
used for characterizing the basic mechanisms for combining probabilistic
automata: aggregation, interconnection and state constraining.
Mathematics Subject Classifications: 18A10 68Q75.
Keywords: neocategory, precategory, Cartesian lifting, probabilistic au- tomaton, aggregation, interconnection.
Monads, shapely functors, and traversals
by Eugenio Moggi, Gianna Bellè, C Barry Jay
Abstract:
This paper demonstrates the potential for combining the
polytypic and monadic programming styles, by introducing a new kind of
combinator, called a traversal. The natural setting for defining
traversals is the class of shapely data types. This result reinforces
the view that shapely data types form a very natural domain for
polytypism: they include most of the data types of interest, while to
exceed them would sacrifice a very smooth interaction between
polytypic and monadic programming.
Exhausting Strategies, Joker Games and IMLL with Units
by Andrzej S Murawski and C-H Luke Ong
Abstract:
We present a game description of free symmetric monoidal closed
categories, which can also be viewed as a fully complete model for the
Intuitionistic Multiplicative Linear Logic with the tensor unit. We model
the unit by a distinguished one-move game called Joker. Special rules
apply to the joker move. Proofs are modelled by what we call conditionally
exhausting strategies, which are deterministic and total only at positions
where no joker move exists in the immediate neighbourhood, and satisfy a
kind of reachability condition called P-exhaustion. We use the model to
give an analysis of a counting problem in free autonomous categories which
is a natural extension of the Triple Unit Problem.
Hilbert Q-Modules and Nuclear Ideals in the Category of
v-Semilattices with a Duality
by Jan Paseka
Abstract:
The paper is divided in two parts. The first part attempts
to begin the investigation of the Hilbert Q-modules. The
basics of the theory of Hilbert Q-modules are established.
Hilbert C*-modules provide a conceptual and mathematical
framework for modern operator algebra. They play a large role
in noncommutative topology and geometry, being a noncommutative
version of a vector bundle. A Hilbert C*-module Y is defined
exactly like a Hilbert space, except that Y is also a module
over a C*-algebra A, the inner product is A-valued and we have
a compatibility condition.
Our idea is, similarly as for Hilbert C*-modules, to
generalize a V-semilattice with a duality by allowing the
inner product to take values in a (unital) involutive quantale
rather than in the two-element Boolean algebra 2. Note that
quantales form the basis for posetal models of linear logic.
Analogously as for Hilbert C*-modules the morphisms in the
category of Hilbert Q-modules are adjointable maps. A special
class of the so called compact operators playing a similar role
as finite-rank operators is introduced. Moreover, the category
of Hilbert Q-modules and adjointable maps between them is an
idempotent involutive category with biproducts and an involutive
quantaloid.
To get insight into the structure of Hilbert Q-modules we explore
in the second part of the paper the notion of the tensor product
in the category of Hilbert 2-modules. We shall give its explicit
description using only the order. We prove that the category of
(strict) Hilbert 2-modules is a tensored category and, motivated
by the results of Abramsky and others, that the class of compact
operators forms a traced nuclear ideal for (strict) Hilbert
2-modules i.e. a partial adjunction for the tensor. Nuclear
ideals are slight variants of compact closed categories, and
hence can be viewed as models of multiplicative linear logic.
Moreover, there are via trace ideals also connections to the
geometry of interaction. A characterization of nuclear maps and
nuclear objects is given.
A Coalgebraic Foundation for Linear Time Semantics
by John Power, Daniele Turi
Abstract:
We present a coalgebraic approach
to trace equivalence semantics based on lifting
behaviour endofunctors for deterministic action
to Kleisli categories of monads
for non-deterministic choice.
In Set, this gives a category with ordinary transition systems
as objects and with morphisms characterised in terms of a
linear notion of bisimulation. The final object in this
category is the canonical abstract model for trace equivalence
and can be obtained by extending the final coalgebra
of the deterministic action behaviour to the Kleisli category of
the non-empty powerset monad. The corresponding final coalgebra
semantics is fully abstract with respect to trace equivalence.
Denotational Completeness Revisited
by Thomas Streicher
Abstract:
We extend the technique of Kripke logical predicates for characterising
lambda definability as originally introduced by Jung and Tiuryn to classical
linear logic (CLL). By defining appropriate Kripke logical predicates for
an arbitrary model of CLL we characterise those morphisms appearing as
denotations of proofs. This amounts to a simplification of Girard's proof
in his paper on ``Denotational Completeness'' in particular avoiding the
additional phase semantics component used there.
A domain-theoretic semantics of lax generic functions
by Hideki Tsuiki
Abstract:
A polymorphic calculus over a hierarchical type structure is designed
and studied. The polymorphism we consider is intermediate between
ad-hoc and coherent (parametric) ones in that function applications
and coercion functions from subtypes to supertypes 'lax' commutes. For
this reason, it has syntactic properties lying between those of
calculi with ac-hoc ones and coherent ones studied in [Tsuiki94].
That is, though it is not normalizing, each basic type term has a kind
of head normal form. For this reason, the semantic structure is
defined through mutually recursive equations between domains without
least elements, which are solved by considering opfibrations. The
adequacy theorem is also proved following the construction of A. Pitts,
from which some syntactic properties are derived.
Higher-dimensional syntax
by Martin Wehr
Abstract:
Higher Dimensional Syntax
Martin Wehr
The aim of this paper is to present the notion of higher-dimensional
syntax, which is a hierarchy of languages. Each term of a n-dimensional
language will be typed by terms of the underlying n-1-dimensional language.
This is an application of the emerging higher-dimensional category notions.
On the lower dimensions live notions of syntax which are already known.
So dimension zero corresponds to words, dimension one corresponds to
equation-free algebraic theories and dimension two corresponds to algebraic
data types available in programming languages like ML and Haskell. In this
paper I show that this hierarchy continues for higher dimensions and
contributes
new notions of syntax. As expected syntax comes with a structural induction
principle which allows definition of several operation. The operations of
substitution, unification and type inference have been investigated.
Further the operation of recursive iteration schemes like generalised map and
fold algorithms have been presented in a previous paper.
This paper concentrates on the issue of a categorical characterisation
of higher dimensional syntax using notions which are partly folklore
(free monoidal object in a monoidal category) partly are new higher-dimensional
category notions. I will characterise higher dimensional syntax as a
left globular set having structure of a free Lawvere theory at each dimension
with a right action and a right coaction of the lower dimension language.
The right action is reminiscent to the substitution property in polymorphic
type theories. The right coaction is reminiscent to the minimal typing
property of a polymorphic type theory.