nach oben

2016 | Buch

Kapitel lesen Erstes Kapitel lesen

Coalgebraic Methods in Computer Science

13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers

herausgegeben von: Ichiro Hasuo

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the thoroughly refereed post-conference proceedings of the 13th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2016, colocated with ETAPS 2016, held in Eindhoven, The Netherlands, in April 2016.
The 10 revised full papers were carefully reviewed and selected from 13 submissions. Also included are an invited paper and two keynote talks. The papers cover a wide range of topics in the theory, logics and applications of coalgebras.

Inhaltsverzeichnis

Frontmatter

Fixed Points of Functors - A Short Abstract

Abstract

Fixed points of endofunctors play a central role in program semantics (initial algebras as recursive specification of domains), in coalgebraic theory of systems (terminal coalgebras and coinduction) and in a number of other connections such as iterative theories (rational fixed point). In this survey we present some older and new results on the structure of the three fixed points we have mentioned.

Jiří Adámek

Compositional Coinduction with Sized Types

Abstract

Proofs by induction on some inductively defined structure, e. g., finitely-branching trees, may appeal to the induction hypothesis at any point in the proof, provided the induction hypothesis is only used for immediate substructures, e. g., the subtrees of the node we are currently considering in the proof. The basic principle of structural induction can be relaxed to course-of-value induction, which allows application of the induction hypothesis also to non-immediate substructures, like any proper subtree of the current tree. If course-of-value induction is not sufficient yet, we can resort to define a well-founded relation on the considered structure and use the induction hypothesis for any substructure which is strictly smaller with regard to the constructed relation.

Andreas Abel

Lawvere Categories as Composed PROPs

Abstract

PROPs and Lawvere categories are related notions adapted to the study of algebraic structures borne by an object in a category, but whereas PROPs are symmetric monoidal, Lawvere categories are cartesian. This paper formulates the connection between the two notions using Lack’s technique for composing PROPs via distributive laws. We show Lawvere categories can be seen as resulting from a distributive law of two PROPs — one expressing the algebraic structure in linear form and the other expressing the ability of copying and discarding variables.

Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi

Transitivity and Difunctionality of Bisimulations

Abstract

Bisimilarity and observational equivalence are notions that agree in many classical models of coalgebras, such as e.g. Kripke structures. In the general category \(Set_{F}\) of \(F-\)coalgebras these notions may, however, diverge. In many cases, observational equivalence, being transitive, turns out to be more useful.

In this paper, we shall investigate the role of transitivity for the largest bisimulation of a coalgebra. Passing to relations between two coalgebras, we choose difunctionality as generalization of transitivity. Since in \(Set_{F}\) bisimulations are known to coincide with \(\bar{F}-\)simulations, we are led to study the notion of \(L-\)similarity, where L is a relation lifting.

Mehdi Zarrad, H. Peter Gumm

Affine Monads and Side-Effect-Freeness

Abstract

The notions of side-effect-freeness and commutativity are typical for probabilistic models, as subclass of quantum models. This paper connects these notions to properties in the theory of monads. A new property of a monad (‘strongly affine’) is introduced. It is shown that for such strongly affine monads predicates are in bijective correspondence with side-effect-free instruments. Also it is shown that these instruments are commutative, in a suitable sense, for monads which are commutative (monoidal).

Bart Jacobs

Duality of Equations and Coequations via Contravariant Adjunctions

Abstract

In this paper we show duality results between categories of equations and categories of coequations. These dualities are obtained as restrictions of dualities between categories of algebras and coalgebras, which arise by lifting contravariant adjunctions on the base categories. By extending this approach to (co)algebras for (co)monads, we retrieve the duality between equations and coequations for automata proved by Ballester-Bolinches, Cosme-Llópez and Rutten, and generalize it to dynamical systems.

Julian Salamanca, Marcello Bonsangue, Jurriaan Rot

Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness

Abstract

A propositional logic program P may be identified with a \(P_fP_f\)-coalgebra on the set of atomic propositions in the program. The corresponding \(C(P_fP_f)\)-coalgebra, where \(C(P_fP_f)\) is the cofree comonad on \(P_fP_f\), describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi’s saturation semantics for logic programming that complements lax semantics.

Ekaterina Komendantskaya, John Power

Product Rules and Distributive Laws

Abstract

We give a categorical perspective on various product rules, including Brzozowski’s product rule (\((st)_a = s_a t + o(s) t_a\)) and the familiar rule of calculus (\((st)_a = s_a t + s t_a\)). It is already known that these product rules can be represented using distributive laws, e.g. via a suitable quotient of a GSOS law. In this paper, we cast these product rules into a general setting where we have two monads S and T, a (possibly copointed) behavioural functor F, a distributive law of T over S, a distributive law of S over F, and a suitably defined distributive law \(TF \Rightarrow FST\). We introduce a coherence axiom giving a sufficient and necessary condition for such triples of distributive laws to yield a new distributive law of the composite monad ST over F, allowing us to determinize FST-coalgebras into lifted F coalgebras via a two step process whenever this axiom holds.

Joost Winter

On the Logic of Generalised Metric Spaces

Abstract

The aim of the paper is to work towards a generalisation of coalgebraic logic enriched over a commutative quantale. Previous work has shown how to dualise the coalgebra type functor \(T:\varOmega \text {-}\mathsf {Cat}\rightarrow \varOmega \text {-}\mathsf {Cat}\) in order to obtain the modal operators and axioms describing transitions of type T. Here we give a logical description of the dual of \(\varOmega \text {-}\mathsf {Cat}\).

Octavian Babus, Alexander Kurz

A Complete Logic for Behavioural Equivalence in Coalgebras of Finitary Set Functors

Abstract

This paper presents a sound and complete sequent-style deduction system for determining behavioural equivalence in coalgebras of finitary set functors preserving weak pullbacks. We select finitary set functors because they are quotients of polynomial functors: the polynomial functor provides a ready-made signature and the quotient provides necessary additional axioms. We also show that certain operations on functors can be expressed with uniform changes to the presentations of the input functors, making this system compositional for a range of widely-studied classes of functors, such as the Kripke polynomial functors. Our system has roots in the \(FLR_0\) proof system of Moschovakis et al., particularly as used by Moss, Wennstrom, and Whitney for non-wellfounded sets. Similarities can also be drawn to expression calculi in the style of Bonsangue, Rutten, and Silva.

David Sprunger

Coalgebraic Completeness-via-Canonicity

Principles and Applications

Abstract

We present the technique of completeness-via-canonicity in a coalgebraic setting and apply it to both positive and boolean coalgebraic logics with relational semantics.

Fredrik Dahlqvist

Relational Lattices via Duality

Abstract

The natural join and the inner union combine in different ways tables of a relational database. Tropashko [18] observed that these two operations are the meet and join in a class of lattices—called the relational lattices—and proposed lattice theory as an alternative algebraic approach to databases. Aiming at query optimization, Litak et al. [12] initiated the study of the equational theory of these lattices. We carry on with this project, making use of the duality theory developed in [16]. The contributions of this paper are as follows. Let A be a set of column’s names and D be a set of cell values; we characterize the dual space of the relational lattice \(\mathsf {R}(D,A)\) by means of a generalized ultrametric space, whose elements are the functions from A to D, with the P(A)-valued distance being the Hamming one but lifted to subsets of A. We use the dual space to present an equational axiomatization of these lattices that reflects the combinatorial properties of these generalized ultrametric spaces: symmetry and pairwise completeness. Finally, we argue that these equations correspond to combinatorial properties of the dual spaces of lattices, in a technical sense analogous of correspondence theory in modal logic. In particular, this leads to an exact characterization of the finite lattices satisfying these equations.

Luigi Santocanale

On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems

Abstract

We consider two notions of timed bisimulation on states of continuous-time dynamical systems: global and local timed bisimulation. By analogy with the notion of a bisimulation relation on states of a labeled transition system which requires the existence of matching transitions starting from states in such a relation, local timed bisimulation requires the existence of sufficiently short (locally defined) matching trajectories. Global timed bisimulation requires the existence of arbitrarily long matching trajectories. For continuous-time systems the notion of a global bisimulation is stronger than the notion of a local bisimulation and its definition has a non-local character. In this paper we give a local characterization of global timed bisimulation. More specifically, we consider a large class of abstract dynamical systems called Nondeterministic Complete Markovian Systems (NCMS) which covers various concrete continuous and discrete-continuous (hybrid) dynamical models and introduce the notion of an \(f^+\)-timed bisimulation, where \(f^+\) is a so called extensibility measure. This notion has a local character. We prove that it is equivalent to global timed bisimulation on states of a NCMS. In this way we give a local characterization of the notion of a global timed bisimulation.

Ievgen Ivanov

Backmatter

Titel: Coalgebraic Methods in Computer Science
herausgegeben von: Ichiro Hasuo
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-40370-0
Print ISBN: 978-3-319-40369-4
DOI: https://doi.org/10.1007/978-3-319-40370-0