Volume
LIPIcs, Volume 139
8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO)
Event
CALCO 2019, June 3-6, 2019, London, United KingdomEditors
Publication Details
- published at: 2019-11-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-120-7
- DBLP: db/conf/calco/calco2019
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 139, CALCO'19, Complete Volume
Abstract
LIPIcs, Volume 139, CALCO'19, Complete Volume
Cite as
8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{roggenbach_et_al:LIPIcs.CALCO.2019,
title = {{LIPIcs, Volume 139, CALCO'19, Complete Volume}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019},
URN = {urn:nbn:de:0030-drops-115619},
doi = {10.4230/LIPIcs.CALCO.2019},
annote = {Keywords: Theory of computation, Models of computation; Modal and temporal logics; Algebraic semantics; Categorical semantics, Quantum computation theory; Software and its engineering, Specification languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{roggenbach_et_al:LIPIcs.CALCO.2019.0,
author = {Roggenbach, Markus and Sokolova, Ana},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.0},
URN = {urn:nbn:de:0030-drops-114282},
doi = {10.4230/LIPIcs.CALCO.2019.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
Matching mu-Logic: Foundation of K Framework (Invited Paper)
Abstract
K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.
Cite as
Xiaohong Chen and Grigore Roşu. Matching mu-Logic: Foundation of K Framework (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CALCO.2019.1,
author = {Chen, Xiaohong and Ro\c{s}u, Grigore},
title = {{Matching mu-Logic: Foundation of K Framework}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.1},
URN = {urn:nbn:de:0030-drops-114296},
doi = {10.4230/LIPIcs.CALCO.2019.1},
annote = {Keywords: Matching mu-logic, Program verification, Reachability logic}
}
Document
Invited Paper
From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper)
Abstract
This extended abstract first presents a new category theoretic approach to equationally axiomatizable classes of algebras. This approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. We present a generic HSP theorem and a sound and complete equational logic, which encompass numerous flavors of equational axiomizations studied in the literature. In addition, we use the generic HSP theorem as a key ingredient to obtain Eilenberg-type correspondences yielding algebraic characterizations of properties of regular machine behaviours. When instantiated for orbit-finite nominal monoids, the generic HSP theorem yields a crucial step for the proof of the first Eilenberg-type variety theorem for data languages.
Cite as
Stefan Milius. From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 2:1-2:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{milius:LIPIcs.CALCO.2019.2,
author = {Milius, Stefan},
title = {{From Equational Specifications of Algebras with Structure to Varieties of Data Languages}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {2:1--2:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.2},
URN = {urn:nbn:de:0030-drops-114309},
doi = {10.4230/LIPIcs.CALCO.2019.2},
annote = {Keywords: Birkhoff theorem, Equational logic, Eilenberg theorem, Data languages}
}
Document
Invited Paper
Principles of Natural Language, Logic, and Tensor Semantics (Invited Paper)
Abstract
Residuated monoids model the structure of sentences. Vectors provide meaning representations for words. A functorial mapping between the two is obtained by lifting the vectors to tensors. The resulting sentence representations solve similarity, disambiguation and entailment tasks.
Cite as
Mehrnoosh Sadrzadeh. Principles of Natural Language, Logic, and Tensor Semantics (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 3:1-3:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sadrzadeh:LIPIcs.CALCO.2019.3,
author = {Sadrzadeh, Mehrnoosh},
title = {{Principles of Natural Language, Logic, and Tensor Semantics}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {3:1--3:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.3},
URN = {urn:nbn:de:0030-drops-114312},
doi = {10.4230/LIPIcs.CALCO.2019.3},
annote = {Keywords: Residuated Monoids, Vector Space Semantics, Corpora of Textual Data, Sentence Similarity and Disambiguation}
}
Document
Invited Paper
Coinduction: Automata, Formal Proof, Companions (Invited Paper)
Abstract
Coinduction is a mathematical tool that is used pervasively in computer science: to program and reason about infinite data-structures, to give semantics to concurrent systems, to obtain automata algorithms. We present some of these applications in automata theory and in formalised mathematics. Then we discuss recent developments on the abstract theory of coinduction and its enhancements.
Cite as
Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{pous:LIPIcs.CALCO.2019.4,
author = {Pous, Damien},
title = {{Coinduction: Automata, Formal Proof, Companions}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {4:1--4:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.4},
URN = {urn:nbn:de:0030-drops-114323},
doi = {10.4230/LIPIcs.CALCO.2019.4},
annote = {Keywords: Coinduction, Automata, Coalgebra, Formal proofs}
}
Document
Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages
Abstract
In this work, we provide a simple coalgebraic characterisation of regular omega-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Omega-automata. In earlier work we introduced Omega-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Omega-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Omega-automata are expressively complete for the regular omega-languages. We show that, due to their coalgebraic nature, Omega-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Omega-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular omega-languages.
Cite as
Vincenzo Ciancia and Yde Venema. Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{ciancia_et_al:LIPIcs.CALCO.2019.5,
author = {Ciancia, Vincenzo and Venema, Yde},
title = {{Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {5:1--5:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.5},
URN = {urn:nbn:de:0030-drops-114338},
doi = {10.4230/LIPIcs.CALCO.2019.5},
annote = {Keywords: omega-automata, regular omega-languages, coalgebra, streams, bisimilarity}
}
Document
Tree Automata as Algebras: Minimisation and Determinisation
Abstract
We study a categorical generalisation of tree automata, as algebras for a fixed endofunctor endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.
Cite as
Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva. Tree Automata as Algebras: Minimisation and Determinisation. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{vanheerdt_et_al:LIPIcs.CALCO.2019.6,
author = {van Heerdt, Gerco and Kapp\'{e}, Tobias and Rot, Jurriaan and Sammartino, Matteo and Silva, Alexandra},
title = {{Tree Automata as Algebras: Minimisation and Determinisation}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {6:1--6:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.6},
URN = {urn:nbn:de:0030-drops-114341},
doi = {10.4230/LIPIcs.CALCO.2019.6},
annote = {Keywords: tree automata, algebras, minimisation, determinisation, Nerode equivalence}
}
Document
Coalgebraic Geometric Logic
Abstract
Using the theory of coalgebra, we introduce a uniform framework for adding modalities to the language of propositional geometric logic. Models for this logic are based on coalgebras for an endofunctor T on some full subcategory of the category Top of topological spaces and continuous functions. We compare the notions of modal equivalence, behavioural equivalence and bisimulation on the resulting class of models, and we provide a final object for the corresponding category. Furthermore, we specify a method of lifting an endofunctor on Set, accompanied by a collection of predicate liftings, to an endofunctor on the category of topological spaces.
Cite as
Nick Bezhanishvili, Jim de Groot, and Yde Venema. Coalgebraic Geometric Logic. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{bezhanishvili_et_al:LIPIcs.CALCO.2019.7,
author = {Bezhanishvili, Nick and de Groot, Jim and Venema, Yde},
title = {{Coalgebraic Geometric Logic}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.7},
URN = {urn:nbn:de:0030-drops-114354},
doi = {10.4230/LIPIcs.CALCO.2019.7},
annote = {Keywords: Coalgebra, Geometric Logic, Modal Logic, Topology}
}
Document
Coinduction in Flow: The Later Modality in Fibrations
Abstract
This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This enables easily understandable coinductive proofs and programs, and fosters automatic proof search.
Part of the framework are also various results that enable a wide range of applications: transportation of (co)limits, exponentials, fibred adjunctions and first-order connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any first-order logic with the later modality. Moreover, we obtain soundness and completeness results, and can use up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal mu-calculus. Finally, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results.
Cite as
Henning Basold. Coinduction in Flow: The Later Modality in Fibrations. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{basold:LIPIcs.CALCO.2019.8,
author = {Basold, Henning},
title = {{Coinduction in Flow: The Later Modality in Fibrations}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {8:1--8:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.8},
URN = {urn:nbn:de:0030-drops-114369},
doi = {10.4230/LIPIcs.CALCO.2019.8},
annote = {Keywords: Coinduction, Fibrations, Later Modality, Recursive Proofs, Up-to techniques, Probabilistic Logic, Probabilistic Programming}
}
Document
Causal Unfoldings
Abstract
In the simplest form of event structure, a prime event structure, an event is associated with a unique causal history, its prime cause. However, it is quite common for an event to have disjunctive causes in that it can be enabled by any one of multiple sets of causes. Sometimes the sets of causes may be mutually exclusive, inconsistent one with another, and sometimes not, in which case they coexist consistently and constitute parallel causes of the event. The established model of general event structures can model parallel causes. On occasion however such a model abstracts too far away from the precise causal histories of events to be directly useful. For example, sometimes one needs to associate probabilities with different, possibly coexisting, causal histories of a common event. Ideally, the causal histories of a general event structure would correspond to the configurations of its causal unfolding to a prime event structure; and the causal unfolding would arise as a right adjoint to the embedding of prime in general event structures. But there is no such adjunction. However, a slight extension of prime event structures remedies this defect and provides a causal unfolding as a universal construction. Prime event structures are extended with an equivalence relation in order to dissociate the two roles, that of an event and its enabling; in effect, prime causes are labelled by a disjunctive event, an equivalence class of its prime causes. With this enrichment a suitable causal unfolding appears as a pseudo right adjoint. The adjunction relies critically on the central and subtle notion of extremal causal realisation as an embodiment of causal history.
Cite as
Marc de Visme and Glynn Winskel. Causal Unfoldings. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{devisme_et_al:LIPIcs.CALCO.2019.9,
author = {de Visme, Marc and Winskel, Glynn},
title = {{Causal Unfoldings}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.9},
URN = {urn:nbn:de:0030-drops-114376},
doi = {10.4230/LIPIcs.CALCO.2019.9},
annote = {Keywords: Event Structures, Parallel Causes, Causal Unfolding, Probability}
}
Document
A Coalgebraic Perspective on Probabilistic Logic Programming
Abstract
Probabilistic logic programming is increasingly important in artificial intelligence and related fields as a formalism to reason about uncertainty. It generalises logic programming with the possibility of annotating clauses with probabilities. This paper proposes a coalgebraic perspective on probabilistic logic programming. Programs are modelled as coalgebras for a certain functor F, and two semantics are given in terms of cofree coalgebras. First, the cofree F-coalgebra yields a semantics in terms of derivation trees. Second, by embedding F into another type G, as cofree G-coalgebra we obtain a "possible worlds" interpretation of programs, from which one may recover the usual distribution semantics of probabilistic logic programming.
Cite as
Tao Gu and Fabio Zanasi. A Coalgebraic Perspective on Probabilistic Logic Programming. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{gu_et_al:LIPIcs.CALCO.2019.10,
author = {Gu, Tao and Zanasi, Fabio},
title = {{A Coalgebraic Perspective on Probabilistic Logic Programming}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.10},
URN = {urn:nbn:de:0030-drops-114387},
doi = {10.4230/LIPIcs.CALCO.2019.10},
annote = {Keywords: probabilistic logic programming, coalgebraic semantics, distribution semantics}
}
Document
Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity
Abstract
The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theory.
Cite as
Astrid Belder, Bas Luttik, and Jos Baeten. Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{belder_et_al:LIPIcs.CALCO.2019.11,
author = {Belder, Astrid and Luttik, Bas and Baeten, Jos},
title = {{Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {11:1--11:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.11},
URN = {urn:nbn:de:0030-drops-114390},
doi = {10.4230/LIPIcs.CALCO.2019.11},
annote = {Keywords: Sequencing, Sequential composition, Bisimilarity, Axiomatisation, Decidability}
}
Document
On Terminal Coalgebras Derived from Initial Algebras
Abstract
A number of important set functors have countable initial algebras, but terminal coalgebras are uncountable or even non-existent. We prove that the countable cardinality is an anomaly: every set functor with an initial algebra of a finite or uncountable regular cardinality has a terminal coalgebra of the same cardinality.
We also present a number of categories that are algebraically complete and cocomplete, i.e., every endofunctor has an initial algebra and a terminal coalgebra.
Finally, for finitary set functors we prove that the initial algebra mu F and terminal coalgebra nu F carry a canonical ultrametric with the joint Cauchy completion. And the algebra structure of mu F determines, by extending its inverse continuously, the coalgebra structure of nu F.
Cite as
Jiří Adámek. On Terminal Coalgebras Derived from Initial Algebras. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{adamek:LIPIcs.CALCO.2019.12,
author = {Ad\'{a}mek, Ji\v{r}{\'\i}},
title = {{On Terminal Coalgebras Derived from Initial Algebras}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {12:1--12:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.12},
URN = {urn:nbn:de:0030-drops-114403},
doi = {10.4230/LIPIcs.CALCO.2019.12},
annote = {Keywords: terminal coalgebras, initial algebras, algebraically complete category, finitary functor, fixed points of functors}
}
Document
Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot
Abstract
We introduce a new notion of "guarded Elgot monad", that is a monad equipped with a form of iteration. It requires every guarded morphism to have a specified fixpoint, and classical equational laws of iteration to be satisfied. This notion includes Elgot monads, but also further examples of partial non-unique iteration, emerging in the semantics of processes under infinite trace equivalence.
We recall the construction of the "coinductive resumption monad" from a monad and endofunctor, that is used for modelling programs up to bisimilarity. We characterize this construction via a universal property: if the given monad is guarded Elgot, then the coinductive resumption monad is the guarded Elgot monad that freely extends it by the given endofunctor.
Cite as
Paul Blain Levy and Sergey Goncharov. Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{levy_et_al:LIPIcs.CALCO.2019.13,
author = {Levy, Paul Blain and Goncharov, Sergey},
title = {{Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.13},
URN = {urn:nbn:de:0030-drops-114414},
doi = {10.4230/LIPIcs.CALCO.2019.13},
annote = {Keywords: Guarded iteration, guarded monads, coalgebraic resumptions}
}
Document
Decomposing Comonad Morphisms
Abstract
The analysis of set comonads whose underlying functor is a container functor in terms of directed containers makes it a simple observation that any morphism between two such comonads factors through a third one by two comonad morphisms, whereof the first is identity on shapes and the second is identity on positions in every shape. This observation turns out to generalize into a much more involved result about comonad morphisms to comonads whose underlying functor preserves Cartesian natural transformations to itself on any category with finite limits. The bijection between comonad coalgebras and comonad morphisms from costate comonads thus also yields a decomposition of comonad coalgebras.
Cite as
Danel Ahman and Tarmo Uustalu. Decomposing Comonad Morphisms. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{ahman_et_al:LIPIcs.CALCO.2019.14,
author = {Ahman, Danel and Uustalu, Tarmo},
title = {{Decomposing Comonad Morphisms}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {14:1--14:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.14},
URN = {urn:nbn:de:0030-drops-114427},
doi = {10.4230/LIPIcs.CALCO.2019.14},
annote = {Keywords: container functors (polynomial functors), container comonads, comonad morphisms and comonad coalgebras, cofunctors, lenses}
}
Document
The Axiom of Choice in Cartesian Bicategories
Abstract
We argue that cartesian bicategories, often used as a general categorical algebra of relations, are also a natural setting for the study of the axiom of choice (AC). In this setting, AC manifests itself as an inequation asserting that every total relation contains a map. The generality of cartesian bicategories allows us to separate this formulation from other set-theoretically equivalent properties, for instance that epimorphisms split. Moreover, via a classification result, we show that cartesian bicategories satisfying choice tend to be those that arise from bicategories of spans.
Cite as
Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CALCO.2019.15,
author = {Bonchi, Filippo and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
title = {{The Axiom of Choice in Cartesian Bicategories}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.15},
URN = {urn:nbn:de:0030-drops-114439},
doi = {10.4230/LIPIcs.CALCO.2019.15},
annote = {Keywords: Cartesian bicategories, Axiom of choice, string diagrams}
}
Document
Linear-Time Graph Algorithms in GP 2
Abstract
GP 2 is an experimental programming language based on graph transformation rules which aims to facilitate program analysis and verification. However, implementing graph algorithms efficiently in a rule-based language is challenging because graph pattern matching is expensive. GP 2 mitigates this problem by providing rooted rules which, under mild conditions, can be matched in constant time. In this paper, we present linear-time GP 2 programs for three problems: tree recognition, binary directed acyclic graph (DAG) recognition, and topological sorting. In each case, we show the correctness of the program, prove its linear time complexity, and also give empirical evidence for the linear run time. For DAG recognition and topological sorting, the linear behaviour is achieved by implementing depth-first search strategies based on an encoding of stacks in graphs.
Cite as
Graham Campbell, Brian Courtehoute, and Detlef Plump. Linear-Time Graph Algorithms in GP 2. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{campbell_et_al:LIPIcs.CALCO.2019.16,
author = {Campbell, Graham and Courtehoute, Brian and Plump, Detlef},
title = {{Linear-Time Graph Algorithms in GP 2}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {16:1--16:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.16},
URN = {urn:nbn:de:0030-drops-114440},
doi = {10.4230/LIPIcs.CALCO.2019.16},
annote = {Keywords: Graph transformation, rooted graph programs, GP 2, linear-time algorithms, depth-first search, topological sorting}
}
Document
Tool Paper
Hybridisation of Institutions in HETS (Tool Paper)
Abstract
We present a tool for the specification and verification of reconfigurable systems. The foundation of the tool is provided by a generic method, called hybridisation of institutions, of extending an arbitrary base institution with features characteristic to hybrid logic, both at the syntactic and the semantic level. Automated proof support for hybridised institutions is obtained via a generic lifting of encodings to first-order logic from the base institution to the hybridised institution. We describe how hybridisation and lifting of encodings to first-order logic are implemented in an extension of the Heterogeneous Tool Set in their full generality. We illustrate the formalism thus obtained with the specification and verification of an autonomous car driving system for highways.
Cite as
Mihai Codescu. Hybridisation of Institutions in HETS (Tool Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 17:1-17:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{codescu:LIPIcs.CALCO.2019.17,
author = {Codescu, Mihai},
title = {{Hybridisation of Institutions in HETS}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {17:1--17:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.17},
URN = {urn:nbn:de:0030-drops-114451},
doi = {10.4230/LIPIcs.CALCO.2019.17},
annote = {Keywords: hybrid logics, formal verification, institutions, reconfigurable systems}
}
Document
Nominal String Diagrams
Abstract
We introduce nominal string diagrams as string diagrams internal in the category of nominal sets. This requires us to take nominal sets as a monoidal category, not with the cartesian product, but with the separated product. To this end, we develop the beginnings of a theory of monoidal categories internal in a symmetric monoidal category. As an instance, we obtain a notion of a nominal PROP as a PROP internal in nominal sets. A 2-dimensional calculus of simultaneous substitutions is an application.
Cite as
Samuel Balco and Alexander Kurz. Nominal String Diagrams. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{balco_et_al:LIPIcs.CALCO.2019.18,
author = {Balco, Samuel and Kurz, Alexander},
title = {{Nominal String Diagrams}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.18},
URN = {urn:nbn:de:0030-drops-114466},
doi = {10.4230/LIPIcs.CALCO.2019.18},
annote = {Keywords: string diagrams, nominal sets, separated product, simultaneous substitutions, internal category, monoidal category, internal monoidal categories, PROP}
}
Document
A Diagrammatic Approach to Quantum Dynamics
Abstract
We present a diagrammatic approach to quantum dynamics based on the categorical algebraic structure of strongly complementary observables. We provide physical semantics to our approach in terms of quantum clocks and quantisation of time. We show that quantum dynamical systems arise naturally as the algebras of a certain dagger Frobenius monad, with the morphisms and tensor product of the category of algebras playing the role, respectively, of equivariant transformations and synchronised parallel composition of dynamical systems. We show that the Weyl Canonical Commutation Relations between time and energy are an incarnation of the bialgebra law and we derive Schrödinger’s equation from a process-theoretic perspective. Finally, we use diagrammatic symmetry-observable duality to prove Stone’s proposition and von Neumann’s Mean Ergodic proposition, recasting the results as two faces of the very same coin.
Cite as
Stefano Gogioso. A Diagrammatic Approach to Quantum Dynamics. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{gogioso:LIPIcs.CALCO.2019.19,
author = {Gogioso, Stefano},
title = {{A Diagrammatic Approach to Quantum Dynamics}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {19:1--19:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.19},
URN = {urn:nbn:de:0030-drops-114472},
doi = {10.4230/LIPIcs.CALCO.2019.19},
annote = {Keywords: Quantum dynamics, String diagrams, Categorical algebra}
}
Document
Tool Paper
CARTOGRAPHER: A Tool for String Diagrammatic Reasoning (Tool Paper)
Abstract
We introduce cartographer, a tool for editing and rewriting string diagrams of symmetric monoidal categories. Our approach is principled: the layout exploits the isomorphism between string diagrams and certain cospans of hypergraphs; the implementation of rewriting is based on the soundness and completeness of convex double-pushout rewriting for string diagram rewriting.
Cite as
Paweł Sobociński, Paul W. Wilson, and Fabio Zanasi. CARTOGRAPHER: A Tool for String Diagrammatic Reasoning (Tool Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 20:1-20:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sobocinski_et_al:LIPIcs.CALCO.2019.20,
author = {Soboci\'{n}ski, Pawe{\l} and Wilson, Paul W. and Zanasi, Fabio},
title = {{CARTOGRAPHER: A Tool for String Diagrammatic Reasoning}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {20:1--20:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Roggenbach, Markus and Sokolova, Ana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.20},
URN = {urn:nbn:de:0030-drops-114482},
doi = {10.4230/LIPIcs.CALCO.2019.20},
annote = {Keywords: tool, string diagram, symmetric monoidal category, graphical reasoning}
}