eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
0
0
10.4230/LIPIcs.CALCO.2017
article
LIPIcs, Volume 72, CALCO'17, Complete Volume
Bonchi, Filippo
König, Barbara
LIPIcs, Volume 72, CALCO'17, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017/LIPIcs.CALCO.2017.pdf
Theory of Computation, Models of computation, Logics and Meanings of Programs, Semantics of Programming Languages – Algebraic Approach
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
0:i
0:x
10.4230/LIPIcs.CALCO.2017.0
article
Front Matter, Table of Contents, Preface, List of Authors
Bonchi, Filippo
König, Barbara
Front Matter, Table of Contents, Preface, List of Authors
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.0/LIPIcs.CALCO.2017.0.pdf
Front Matter
Table of Contents
Preface
List of Authors
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
1:1
1:6
10.4230/LIPIcs.CALCO.2017.1
article
Probability Sheaves and the Giry Monad
Simpson, Alex
I introduce the notion of probability sheaf, which is a mathematical structure capturing the relationship between probabilistic concepts (such as random variable) and sample spaces. Various probability-theoretic notions can be (re)formulated in terms of category-theoretic structure on the category of probability sheaves.
As a main example, I consider the Giry monad, which, in its original formulation, constructs spaces of probability measures. I show that the Giry monad generalises to the category of probability sheaves, where it turns out to have a simple, purely category-theoretic definition.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.1/LIPIcs.CALCO.2017.1.pdf
Random variable
conditional independence
category theory
sheaves
Giry monad
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
2:1
2:17
10.4230/LIPIcs.CALCO.2017.2
article
Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks
Gianola, Alessandro
Kasangian, Stefano
Sabadini, Nicoletta
Span(Graph) was introduced by Katis, Sabadini and Walters as a categorical algebra of automata with interfaces, with main operation being communicating-parallel composition. Additional operations provide also a calculus of connectors or wires among components.
A system so described has two aspects: an informal network geometry arising from the algebraic expression, and a space of states and transition given by its evaluation in Span(Graph). So, Span(Graph) yields purely compositional, hierarchical descriptions of networks with a fixed topology .
The dual algebra Cospan(Graph) allows to describe also the sequential behaviour of systems. Both algebras, of spans and of cospans, are symmetrical monoidal categories with commutative separable algebra structures on the objects.
Hence, the combined algebra CospanSpan(Graph) can be interpreted as a general algebra for reconfigurable/hierarchical networks, generalizing the usual Kleene's algebra for classical automata. We present some examples of systems described in this setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.2/LIPIcs.CALCO.2017.2.pdf
Categories
Automata
Composition
Networks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
3:1
3:15
10.4230/LIPIcs.CALCO.2017.3
article
On Corecursive Algebras for Functors Preserving Coproducts
Adámek, Jiri
Milius, Stefan
For an endofunctor H on a hyper-extensive category preserving countable coproducts we describe the free corecursive algebra on Y as the coproduct of the terminal coalgebra for H and the free H-algebra on Y. As a consequence, we derive that H is a cia functor, i.e., its corecursive algebras are precisely the cias (completely iterative algebras). Also all functors H(-) + Y are then cia functors. For finitary set functors we prove that, conversely, if H is a cia functor, then it has the form H = W \times (-) + Y for some sets W and Y.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.3/LIPIcs.CALCO.2017.3.pdf
terminal coalgebra
free algebra
corecursive algebra
hyper-extensive category
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
4:1
4:16
10.4230/LIPIcs.CALCO.2017.4
article
Bisimulation for Weakly Expressive Coalgebraic Modal Logics
Bakhtiari, Zeinab
Hvid Hansen, Helle
Research on the expressiveness of coalgebraic modal logics with respect to semantic equivalence notions has so far focused mainly on finding logics that are able to distinguish states that are not behaviourally equivalent (such logics are said to be expressive). In other words, the notion of behavioural equivalence is taken as the starting point, and the expressiveness of the logic is evaluated against it.
However, for some applications, modal logics that are not expressive are of independent interest. Such an example is given by contingency logic.
We can now turn the question of expressiveness around and ask, given a modal logic, what is a suitable notion of semantic equivalence? In this paper, we propose a notion of \Lambda-bisimulation which is parametric in a collection
\Lambda of predicate liftings. We study the basic properties of \Lambda-bisimilarity, and prove as our main result a Hennessy-Milner style theorem, which shows that (for finitary functors) \Lambda-bisimilarity exactly matches the expressiveness of the coalgebraic modal logic arising from \Lambda.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.4/LIPIcs.CALCO.2017.4.pdf
Coalgebraic modal logic
bisimulation
expressiveness
Hennessy-Milner theorem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
5:1
5:16
10.4230/LIPIcs.CALCO.2017.5
article
Monoidal Company for Accessible Functors
Basold, Henning
Pous, Damien
Rot, Jurriaan
Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties.
Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.5/LIPIcs.CALCO.2017.5.pdf
coalgebras
distributive laws
accessible functors
monoidal categories
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
6:1
6:17
10.4230/LIPIcs.CALCO.2017.6
article
On Path-Based Coalgebras and Weak Notions of Bisimulation
Beohar, Harsh
Küpper, Sebastian
It is well known that the theory of coalgebras provides an abstract definition of behavioural equivalence that coincides with strong bisimulation across a wide variety of state-based systems. Unfortunately, the theory in the presence of so-called silent actions is not yet fully developed. In this paper, we give a coalgebraic characterisation of branching (delay) bisimulation in the context of labelled transition systems (fully probabilistic systems). It is shown that recording executions (up to a notion of stuttering), rather than the set of successor states, from a state is sufficient to characterise the respected bisimulation relations in both cases.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.6/LIPIcs.CALCO.2017.6.pdf
Paths
Executions
Branching bisimulation
Coalgebras
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
7:1
7:18
10.4230/LIPIcs.CALCO.2017.7
article
Parity Automata for Quantitative Linear Time Logics
Cirstea, Corina
Shimizu, Shunsuke
Hasuo, Ichiro
We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Buchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naive algorithm for computing extents, under additional assumptions on the domain of truth values.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.7/LIPIcs.CALCO.2017.7.pdf
coalgebra
quantitative logic
linear time logic
parity automaton
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
8:1
8:16
10.4230/LIPIcs.CALCO.2017.8
article
Automata Minimization: a Functorial Approach
Colcombet, Thomas
Petrisan, Daniela
In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as
functors from input categories that specify the type of the
languages and of the machines to categories that specify the type of
outputs.
Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be applied to several phenomena in automata theory, starting with determinization and
minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to
Choffrut's minimization algorithm for subsequential transducers and revisit Brzozowski's minimization algorithm.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.8/LIPIcs.CALCO.2017.8.pdf
functor automata
minimization
Choffrut's minimization algorithm
subsequential transducers
Brzozowski's minimization algorithm
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
9:1
9:15
10.4230/LIPIcs.CALCO.2017.9
article
The Positivication of Coalgebraic Logics
Dahlqvist, Fredrik
Kurz, Alexander
We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos->Pos from an endofunctor T: Set->Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor L': DL->DL from a syntax-building functor L: BA->BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case of several modal logics. We show how the semantics of a boolean coalgebraic logic can be canonically lifted to define a semantics for its positive fragment, and that weak completeness transfers from the boolean case to the positive case.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.9/LIPIcs.CALCO.2017.9.pdf
Coalgebraic logic
coalgebras
enriched category theory
boolean algebra
distributive lattice
positive modal logic
monotone modal logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
10:1
10:16
10.4230/LIPIcs.CALCO.2017.10
article
Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics
Eberhart, Clovis
Hirschowitz, Tom
Recent developments of game semantics have given rise to new models of concurrent languages. On the one hand, an approach based on string diagrams has given models of CCS and the pi-calculus, and on the other hand, Tsukada and Ong have designed a games model for a non-deterministic lambda-calculus. There is an obvious, shallow relationship between the two approaches, as they both define innocent strategies as sheaves for a Grothendieck topology embedding
"views" into "plays". However, the notions of views and plays differ greatly between the approaches: Tsukada and Ong use notions from standard game semantics, while the authors of this paper use string diagrams. We here aim to bridge this gap by showing that even though the notions of plays, views, and innocent strategies differ, it is mostly a matter of presentation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.10/LIPIcs.CALCO.2017.10.pdf
Concurrency
Sheaves
Presheaf models
Game Semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
11:1
11:16
10.4230/LIPIcs.CALCO.2017.11
article
Disjunctive Bases: Normal Forms for Modal Logics
Enqvist, Sebastian
Venema, Yde
We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here
we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "one-step" level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full
fixpoint logic, its fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive
bases, and provide a partial solution.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.11/LIPIcs.CALCO.2017.11.pdf
Modal logic
fixpoint logic
automata
coalgebra
graded modal logic
Lyndon theorem
uniform interpolation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
12:1
12:16
10.4230/LIPIcs.CALCO.2017.12
article
A Universal Construction for (Co)Relations
Fong, Brendan
Zanasi, Fabio
Calculi of string diagrams are increasingly used to present the syntax and algebraic structure of various families of circuits, including signal flow graphs, electrical circuits and quantum processes. In many such approaches, the semantic interpretation for diagrams is given in terms of relations or corelations (generalised equivalence relations) of some kind. In this paper we show how semantic categories of both relations and corelations can be characterised as colimits of simpler categories. This modular perspective is important as it simplifies the task of giving a complete axiomatisation for semantic equivalence of string diagrams. Moreover, our general result unifies various theorems that are independently found in literature and are relevant for program semantics, quantum computation and control theory.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.12/LIPIcs.CALCO.2017.12.pdf
corelation
prop
string diagram
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
13:1
13:17
10.4230/LIPIcs.CALCO.2017.13
article
Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics
Gowers, William John
Laird, James
The non-commutative sequoid operator (/) on games was introduced to capture algebraically the presence of state in history-sensitive strategies in game semantics, by imposing a causality relation on the tensor product of games. Coalgebras for the functor A (/) _ - i.e., morphisms from S to A (/) S --- may be viewed as state transformers: if A (/) _ has a final coalgebra, !A, then the anamorphism of such a state transformer encapsulates its explicit state, so that it is shared only between successive invocations.
We study the conditions under which a final coalgebra !A for A (/) _ is the carrier of a cofree commutative comonoid on A. That is, it is a model of the exponential of linear logic in which we can construct imperative objects such as reference cells coalgebraically, in a game semantics setting. We show that if the tensor decomposes into the sequoid, the final coalgebra !A may be endowed with the structure of the cofree commutative comonoid if there is a natural isomorphism from !(A × B)to !A (x) !B. This condition is always satisfied if !A is the bifree algebra for A (/) _, but in general it is necessary to impose it, as we establish by giving an example of a sequoidally decomposable category of games in which plays will be allowed to have transfinite length. In this category, the final coalgebra for the functor A (/)_ is not the cofree commutative comonoid over A: we illustrate this by explicitly contrasting the final sequence for the functor A (/) _ with the chain of symmetric tensor powers used in the construction of the cofree commutative comonoid as a limit by Melliès, Tabareau and Tasson.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.13/LIPIcs.CALCO.2017.13.pdf
Game Semantics
Stateful Languages
Transfinite Games
Sequoid Operator
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
14:1
14:15
10.4230/LIPIcs.CALCO.2017.14
article
Free Constructions and Coproducts of d-Frames
Jakl, Tomás
Jung, Achim
A general theory of presentations for d-frames does not yet exist. We review the difficulties and give sufficient conditions for when they can be overcome. As an application we prove that the category of d-frames is closed under coproducts.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.14/LIPIcs.CALCO.2017.14.pdf
Free construction
d-frame
coproduct
C-ideals
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
15:1
15:15
10.4230/LIPIcs.CALCO.2017.15
article
UML Interactions Meet State Machines - An Institutional Approach
Knapp, Alexander
Mossakowski, Till
UML allows the multi-viewpoint modelling of systems. One important question is whether an interaction as specified by a sequence diagram can be actually realised in the system. Here, the latter is specified as a combination of several state machines (one for each lifeline in the interaction) by a composite structure diagram. In order to tackle this question, we formalise the involved UML diagram types as institutions, and their relations as institution (co)morphisms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.15/LIPIcs.CALCO.2017.15.pdf
UML
state machines
interactions
composite structure diagrams
institutions
multi-view consistency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
16:1
16:15
10.4230/LIPIcs.CALCO.2017.16
article
Being Van Kampen in Presheaf Topoi is a Uniqueness Property
König, Harald
Wolter, Uwe
Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, e.g. the category of directed graphs. Multimodeling requires to construct colimits of diagrams of single models and their instances, while decomposition of instances of the multimodel is given by pullback. Compositionality requires an exact interplay of these operations, i.e., the diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible.
In this paper we state a necessary and sufficient yet easily checkable condition for the Van Kampen property to hold for diagrams in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Sobocinski presented at CALCO 2009 the fact that the Van Kampen property reveals a set-based structural uniqueness feature.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.16/LIPIcs.CALCO.2017.16.pdf
Van Kampen Cocone
Presheaf Topos
Fibred Semantics
Mapping Path
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
17:1
17:16
10.4230/LIPIcs.CALCO.2017.17
article
Custom Hypergraph Categories via Generalized Relations
Marsden, Dan
Genovese, Fabrizio
Process theories combine a graphical language for compositional reasoning with an underlying categorical semantics. They have been successfully applied to fields such as quantum computation, natural language processing, linear dynamical systems and network theory. When investigating a new application, the question arises of how to identify a suitable process theoretic model.
We present a conceptually motivated parameterized framework for the construction of models for process theories. Our framework generalizes the notion of binary relation along four axes of variation, the truth values, a choice of algebraic structure, the ambient mathematical universe and the choice of proof relevance or provability. The resulting categories are preorder-enriched and provide analogues of relational converse and taking graphs of maps. Our constructions are functorial in the parameter choices, establishing mathematical connections between different application domains. We illustrate our techniques by constructing many existing models from the literature, and new models that open up ground for further development.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.17/LIPIcs.CALCO.2017.17.pdf
Process Theory
Categorical Compositional Semantics
Generalized Relations
Hypergraph Category
Compact Closed Category
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
18:1
18:16
10.4230/LIPIcs.CALCO.2017.18
article
Proper Functors and their Rational Fixed Point
Milius, Stefan
The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be a subcoalgebra of the final coalgebra. Inspired by Ésik and Maletti's notion of proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.18/LIPIcs.CALCO.2017.18.pdf
proper functor
proper semiring
coalgebra
rational fixed point
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
19:1
19:18
10.4230/LIPIcs.CALCO.2017.19
article
A Classical Groupoid Model for Quantum Networks
Reutter, David
Vicary, Jamie
We give a mathematical analysis of a new type of classical computer network architecture, intended as a model of a new technology that has recently been proposed in industry. Our approach is based on groubits, generalizations of classical bits based on groupoids. This network architecture allows the direct execution of a number of protocols that are usually associated with quantum networks, including teleportation, dense coding and secure key distribution.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.19/LIPIcs.CALCO.2017.19.pdf
groupoids
networks
quantum
semantics
key distribution
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
20:1
20:20
10.4230/LIPIcs.CALCO.2017.20
article
A 2-Categorical Approach to Composing Quantum Structures
Reutter, David
Vicary, Jamie
We present an infinite number of construction schemes for quantum structures, including unitary error bases, Hadamard matrices, quantum Latin squares and controlled families, many of which have not previously been described. Our results rely on the type structure of biunitary connections, 2-categorical structures which play a central role in the theory of planar algebras. They have an attractive graphical calculus which allows simple correctness proofs for the constructions we present. We apply these techniques to construct a unitary error basis that cannot be built using any previously known method.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.20/LIPIcs.CALCO.2017.20.pdf
quantum constructions
2-category
graphical calculus
planar algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
21:1
21:16
10.4230/LIPIcs.CALCO.2017.21
article
Uniform Interpolation in Coalgebraic Modal Logic
Seifan, Fatemeh
Schröder, Lutz
Pattinson, Dirk
A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula - the interpolant - to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.21/LIPIcs.CALCO.2017.21.pdf
modal logic
coalgebraic logic
uniform interpolation
preservation of weak pullbacks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
22:1
22:16
10.4230/LIPIcs.CALCO.2017.22
article
Termination in Convex Sets of Distributions
Sokolova, Ana
Woracek, Harald
Convex algebras, also called (semi)convex sets, are at the heart of modelling probabilistic systems including probabilistic automata. Abstractly, they are the Eilenberg-Moore algebras of the
finitely supported distribution monad. Concretely, they have been studied for decades within algebra and convex geometry.
In this paper we study the problem of extending a convex algebra by a single point. Such extensions enable the modelling of termination in probabilistic systems. We provide a full description of all possible extensions for a particular class of convex algebras: For a fixed convex subset D of a vector space satisfying additional technical condition, we consider the algebra of convex subsets of D. This class contains the convex algebras of convex subsets of distributions, modelling (nondeterministic) probabilistic automata. We also provide a full description of all possible extensions for the class of free convex algebras, modelling fully probabilistic systems.
Finally, we show that there is a unique functorial extension, the so-called black-hole extension.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.22/LIPIcs.CALCO.2017.22.pdf
convex algebra
one-point extensions
convex powerset monad
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
23:1
23:15
10.4230/LIPIcs.CALCO.2017.23
article
Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence
Sprunger, David
Moss, Lawrence S.
We present a new proof system for equality of terms which present elements of the final coalgebra of a finitary set functor. This is most important when the functor is finitary, and we improve on logical systems which have already been proposed in several papers. Our contributions here are (1) a new logical rule which makes for proofs which are somewhat easier to find, and (2) a soundness/completeness theorem which works for all finitary functors, in particular removing a weak pullback preservation requirement that had been used previously. Our work is based on properties of precongruence relations and also on a new parametrized coinduction principle.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.23/LIPIcs.CALCO.2017.23.pdf
precongruence
kernel bisimulation
finitary functor
coalgebra
behavioural equivalence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
24:1
24:16
10.4230/LIPIcs.CALCO.2017.24
article
Finite Behaviours and Finitary Corecursion
Urbat, Henning
In the coalgebraic approach to state-based systems, semantics is captured up to behavioural equivalence by special coalgebras such as the final coalgebra, the final locally finitely presentable coalgebra (Adámek, Milius, and Velebil), or the final locally finitely generated coalgebra (Milius, Pattinson, and Wißmann). The choice of the proper semantic domain is determined by finiteness restrictions imposed on the systems of interest. We propose a unifying perspective by introducing the concept of a final locally (I,M)-presentable coalgebra, where the two parameters I and M determine what a "finite" system is. Under suitable conditions on the categories and type functors, we show that the final locally (I,M)-presentable coalgebra exists and coincides with the initial (I,M)-iterative algebra, thereby putting a common roof over several results on iterative, fg-iterative and completely iterative algebras that were given a separate treatment before.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.24/LIPIcs.CALCO.2017.24.pdf
Iterative algebra
completely iterative algebra
fg-iterative algebra
rational fixpoint
terminal coalgebra
iterative monad
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-11-17
72
25:1
25:8
10.4230/LIPIcs.CALCO.2017.25
article
The EfProb Library for Probabilistic Calculations
Cho, Kenta
Jacobs, Bart
EfProb is an abbreviation of Effectus Probability. It is the name of
a library for probability calculations in Python. EfProb offers a
uniform language for discrete, continuous and quantum probability.
For each of these three cases, the basic ingredients of the language
are states, predicates, and channels. Probabilities are typically
calculated as validities of predicates in states. States can be
updated (conditioned) with predicates. Channels can be used for state
transformation and for predicate transformation. This short paper
gives an overview of the use of EfProb.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.25/LIPIcs.CALCO.2017.25.pdf
probability
embedded language
effectus theory