Concurrent Realizations of Reactive Systems
by Marek Bednarczyk, Andrzej Borzyszkowski
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
by Roberto Bruni, José Meseguer, Ugo Montanari, Vladimiro Sassone
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
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
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.
by Adam Eppendahl
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
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
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
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
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.
by Zhaohui Luo and Sergei Soloviev
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
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
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
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
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
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
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
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.
by Martin Wehr
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.