Volume
LIPIcs, Volume 211
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO)
Publication Details
- published at: 2021-11-08
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-212-9
- DBLP: db/conf/calco/calco2021
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 211, CALCO 2021, Complete Volume
Abstract
LIPIcs, Volume 211, CALCO 2021, Complete Volume
Cite as
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 1-384, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@Proceedings{gadducci_et_al:LIPIcs.CALCO.2021,
title = {{LIPIcs, Volume 211, CALCO 2021, Complete Volume}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {1--384},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021},
URN = {urn:nbn:de:0030-drops-153544},
doi = {10.4230/LIPIcs.CALCO.2021},
annote = {Keywords: LIPIcs, Volume 211, CALCO 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{gadducci_et_al:LIPIcs.CALCO.2021.0,
author = {Gadducci, Fabio and Silva, Alexandra},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.0},
URN = {urn:nbn:de:0030-drops-153559},
doi = {10.4230/LIPIcs.CALCO.2021.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Distributive Laws for Lawvere Theories (Invited Talk)
Abstract
Distributive laws give a way of combining two algebraic structures expressed as monads; in this work we propose a theory of distributive laws for combining algebraic structures expressed as Lawvere theories. We propose four approaches, involving profunctors, monoidal profunctors, an extension of the free finite-product category 2-monad from Cat to Prof, and factorisation systems respectively. We exhibit comparison functors between CAT and each of these new frameworks to show that the distributive laws between the Lawvere theories correspond in a suitable way to distributive laws between their associated finitary monads. The different but equivalent formulations then provide, between them, a framework conducive to generalisation, but also an explicit description of the composite theories arising from distributive laws.
Cite as
Eugenia Cheng. Distributive Laws for Lawvere Theories (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{cheng:LIPIcs.CALCO.2021.1,
author = {Cheng, Eugenia},
title = {{Distributive Laws for Lawvere Theories}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.1},
URN = {urn:nbn:de:0030-drops-153560},
doi = {10.4230/LIPIcs.CALCO.2021.1},
annote = {Keywords: Distributive laws, Monads, Lawvere theories}
}
Document
Invited Talk
Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems (Invited Talk)
Abstract
A dramatic transformation of our technical world towards smart cyber-physical systems can be currently observed. This transformation results in a networked technical world where besides the embedded systems with their interaction with the physical world the interconnection of these nodes in the cyber world becomes a key element. Furthermore, there is a strong trend towards smart systems where artificial intelligence techniques and in particular machine learning is employed to make software behave accordingly. This raises the question whether our capabilities to model these future embedded systems are ready to tackle the resulting challenges.
In this presentation, we will first discuss how extensions of graph transformation systems can be employed to design and analyse the envisioned future cyber-physical systems with an emphasis on the synergies networking can offer and then characterise which challenges for the design, production, and operation of these systems and how they can be tacked with graph transformation systems. We will therefore discuss to what extent our current capabilities in particular concerning engineering with graph transformation systems match these challenges and where substantial improvements for the graph transformation systems have been crucial and will be crucial in the future.
Models are used in classical engineering to plan systems upfront to maximise envisioned properties resp. minimise cost. For smart cyber-physical systems this decoupling of development-time and run-time considerations vanishes, and self-adaptation and runtime models have been advocated as concepts to shift some considerations to run-time. We will review the underlying causes for this shift to run-time, discuss some our work with graph transformation systems in this direction, and outline related open challenges and implications for future work for graph transformation systems to engineer smart cyber-physical systems.
Cite as
Holger Giese. Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{giese:LIPIcs.CALCO.2021.2,
author = {Giese, Holger},
title = {{Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.2},
URN = {urn:nbn:de:0030-drops-153573},
doi = {10.4230/LIPIcs.CALCO.2021.2},
annote = {Keywords: Cyber-physical systems, Graph transformation}
}
Document
Invited Talk
Dialectica Comonads (Invited Talk)
Abstract
Dialectica categories are interesting categorical models of Linear Logic which preserve the differences between linear connectives that the logic is supposed to make, unlike some of the most traditional models like coherence spaces. They arise from the categorical modelling of Gödel’s Dialectica interpretation and seem to be having a revival: connections between Dialectica constructions and containers, lenses and polynomials have been described recently in the literature. In this note I will recap the basic Dialectica constructions and then go on to describe the less well-known interplay of comonads, coalgebras and comonoids that characterizes the composite functor standing for the "of course!" operator in dialectica categories. This composition of comonads evokes some work on stateful games by Laird and others, also discussed in the setting of Reddy’s system LLMS (Linear Logic Model of State).
Cite as
Valeria de Paiva. Dialectica Comonads (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 3:1-3:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{depaiva:LIPIcs.CALCO.2021.3,
author = {de Paiva, Valeria},
title = {{Dialectica Comonads}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {3:1--3:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.3},
URN = {urn:nbn:de:0030-drops-153581},
doi = {10.4230/LIPIcs.CALCO.2021.3},
annote = {Keywords: Dialectica categories, Linear logic, Comonads}
}
Document
Invited Talk
The Challenges of Weak Persistency (Invited Talk)
Abstract
Non-volatile memory (NVM) is a new hardware technology that provides durable storage at performance similar to that of plain volatile RAM. As such, there is a lot of interest in exploiting this technology to improve the performance of existing disk-bound applications and to find new applications for it. Nevertheless, developing correct programs that interact with non-volatile memory is by no means easy, since mainstream architectures provide rather weak persistency semantics and rather low-level and expensive mechanisms in order to avoid weak behaviors. This creates many opportunities for researchers in programming language semantics, logic, and verification to develop techniques to assist programmers writing NVM programs. This short paper and the associated talk outline the challenges caused by NVM and the research opportunities for PL researchers.
Cite as
Viktor Vafeiadis. The Challenges of Weak Persistency (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{vafeiadis:LIPIcs.CALCO.2021.4,
author = {Vafeiadis, Viktor},
title = {{The Challenges of Weak Persistency}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {4:1--4:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.4},
URN = {urn:nbn:de:0030-drops-153593},
doi = {10.4230/LIPIcs.CALCO.2021.4},
annote = {Keywords: Weak Persistency, Non-Volatile Memory}
}
Document
(Co)algebraic pearls
Initial Algebras Without Iteration ((Co)algebraic pearls)
Abstract
The Initial Algebra Theorem by Trnková et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point A of the functor, it uses Pataraia’s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of A. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.
Cite as
Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras Without Iteration ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.5,
author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.},
title = {{Initial Algebras Without Iteration}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {5:1--5:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.5},
URN = {urn:nbn:de:0030-drops-153606},
doi = {10.4230/LIPIcs.CALCO.2021.5},
annote = {Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra chain}
}
Document
(Co)algebraic pearls
Which Categories Are Varieties? ((Co)algebraic pearls)
Abstract
Categories equivalent to single-sorted varieties of finitary algebras were characterized in the famous dissertation of Lawvere. We present a new proof of a slightly sharpened version: those are precisely the categories with kernel pairs and reflexive coequalizers having an abstractly finite, effective strong generator. A completely analogous result is proved for varieties of many-sorted algebras provided that there are only finitely many sorts. In case of infinitely many sorts a slightly weaker result is presented: instead of being abstractly finite, the generator is required to consist of finitely presentable objects.
Cite as
Jiří Adámek and Jiří Rosický. Which Categories Are Varieties? ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.6,
author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Rosick\'{y}, Ji\v{r}{\'\i}},
title = {{Which Categories Are Varieties?}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {6:1--6:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.6},
URN = {urn:nbn:de:0030-drops-153610},
doi = {10.4230/LIPIcs.CALCO.2021.6},
annote = {Keywords: variety, many-sorted algebra, abstractly finite object, effective object, strong generator}
}
Document
Tensor of Quantitative Equational Theories
Abstract
We develop a theory for the commutative combination of quantitative effects, their tensor, given as a combination of quantitative equational theories that imposes mutual commutation of the operations from each theory. As such, it extends the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor.
We show that under certain assumptions on the quantitative theories the free monad that arises from the tensor of two theories is the categorical tensor of the free monads on the theories. As an application, we provide the first algebraic axiomatizations of labelled Markov processes and Markov decision processes. Apart from the intrinsic interest in the axiomatizations, it is pleasing they are obtained compositionally by means of the sum and tensor of simpler quantitative equational theories.
Cite as
Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Tensor of Quantitative Equational Theories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bacci_et_al:LIPIcs.CALCO.2021.7,
author = {Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
title = {{Tensor of Quantitative Equational Theories}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.7},
URN = {urn:nbn:de:0030-drops-153628},
doi = {10.4230/LIPIcs.CALCO.2021.7},
annote = {Keywords: Quantitative equational theories, Tensor, Monads, Quantitative Effects}
}
Document
Pushdown Automata and Context-Free Grammars in Bisimulation Semantics
Abstract
The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence.
Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness.
Cite as
Jos C. M. Baeten, Cesare Carissimo, and Bas Luttik. Pushdown Automata and Context-Free Grammars in Bisimulation Semantics. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{baeten_et_al:LIPIcs.CALCO.2021.8,
author = {Baeten, Jos C. M. and Carissimo, Cesare and Luttik, Bas},
title = {{Pushdown Automata and Context-Free Grammars in Bisimulation Semantics}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.8},
URN = {urn:nbn:de:0030-drops-153632},
doi = {10.4230/LIPIcs.CALCO.2021.8},
annote = {Keywords: pushdown automaton, context-free grammar, bisimilarity, intermediate acceptance, state awareness}
}
Document
(Co)algebraic pearls
From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls)
Abstract
Farkas' lemma is a celebrated result on the solutions of systems of linear inequalities, which finds application pervasively in mathematics and computer science. In this work we show how to formulate and prove Farkas' lemma in diagrammatic polyhedral algebra, a sound and complete graphical calculus for polyhedra. Furthermore, we show how linear programs can be modeled within the calculus and how some famous duality results can be proved.
Cite as
Filippo Bonchi, Alessandro Di Giorgio, and Fabio Zanasi. From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.9,
author = {Bonchi, Filippo and Di Giorgio, Alessandro and Zanasi, Fabio},
title = {{From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9},
URN = {urn:nbn:de:0030-drops-153643},
doi = {10.4230/LIPIcs.CALCO.2021.9},
annote = {Keywords: String diagrams, Farkas Lemma, Duality, Linear Programming}
}
Document
On Doctrines and Cartesian Bicategories
Abstract
We study the relationship between cartesian bicategories and a specialisation of Lawvere’s hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines.
Cite as
Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.10,
author = {Bonchi, Filippo and Santamaria, Alessio and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
title = {{On Doctrines and Cartesian Bicategories}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {10:1--10:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10},
URN = {urn:nbn:de:0030-drops-153656},
doi = {10.4230/LIPIcs.CALCO.2021.10},
annote = {Keywords: Cartesian bicategories, elementary existential doctrines, string diagram}
}
Document
(Co)algebraic pearls
Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls)
Abstract
We prove that every finitely generated convex set of finitely supported probability distributions has a unique base. We apply this result to provide an alternative proof of a recent result: the algebraic theory of convex semilattices presents the monad of convex sets of probability distributions.
Cite as
Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.11,
author = {Bonchi, Filippo and Sokolova, Ana and Vignudelli, Valeria},
title = {{Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {11:1--11:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11},
URN = {urn:nbn:de:0030-drops-153666},
doi = {10.4230/LIPIcs.CALCO.2021.11},
annote = {Keywords: Convex sets of distributions monad, Convex semilattices, Unique base}
}
Document
Closure Hyperdoctrines
Abstract
(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems.
In this paper we present an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators. Hence, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, and for the definition of new spatial logics for new applications.
Cite as
Davide Castelnovo and Marino Miculan. Closure Hyperdoctrines. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{castelnovo_et_al:LIPIcs.CALCO.2021.12,
author = {Castelnovo, Davide and Miculan, Marino},
title = {{Closure Hyperdoctrines}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {12:1--12:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12},
URN = {urn:nbn:de:0030-drops-153678},
doi = {10.4230/LIPIcs.CALCO.2021.12},
annote = {Keywords: categorical logic, topological semantics, closure operators, spatial logic}
}
Document
(Co)algebraic pearls
How to Write a Coequation ((Co)algebraic pearls)
Abstract
There is a large amount of literature on the topic of covarieties, coequations and coequational specifications, dating back to the early seventies. Nevertheless, coequations have not (yet) emerged as an everyday practical specification formalism for computer scientists. In this review paper, we argue that this is partly due to the multitude of syntaxes for writing down coequations, which seems to have led to some confusion about what coequations are and what they are for. By surveying the literature, we identify four types of syntaxes: coequations-as-corelations, coequations-as-predicates, coequations-as-equations, and coequations-as-modal-formulas. We present each of these in a tutorial fashion, relate them to each other, and discuss their respective uses.
Cite as
Fredrik Dahlqvist and Todd Schmid. How to Write a Coequation ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 13:1-13:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dahlqvist_et_al:LIPIcs.CALCO.2021.13,
author = {Dahlqvist, Fredrik and Schmid, Todd},
title = {{How to Write a Coequation}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {13:1--13:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.13},
URN = {urn:nbn:de:0030-drops-153686},
doi = {10.4230/LIPIcs.CALCO.2021.13},
annote = {Keywords: Coalgebra, coequation, covariety}
}
Document
Monads on Categories of Relational Structures
Abstract
We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity λ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders (λ = ω) or metric spaces (λ = ω₁). We establish a bijective correspondence between λ-accessible enriched monads on the given category of relational structures and a notion of λ-ary algebraic theories (i.e. with operations of arity < λ), with the syntax of algebraic theories induced by the relational signature (e.g. inequations or equations-up-to-ε). We provide a generic sound and complete derivation system for such relational algebraic theories, thus in particular recovering (extensions of) recent systems of this type for monads on partial orders and metric spaces by instantiation. In particular, we present an ω₁-ary algebraic theory of metric completion. The theory-to-monad direction of our correspondence remains true for the case of κ-ary algebraic theories and κ-accessible monads for κ < λ, e.g. for finitary theories over metric spaces.
Cite as
Chase Ford, Stefan Milius, and Lutz Schröder. Monads on Categories of Relational Structures. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{ford_et_al:LIPIcs.CALCO.2021.14,
author = {Ford, Chase and Milius, Stefan and Schr\"{o}der, Lutz},
title = {{Monads on Categories of Relational Structures}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.14},
URN = {urn:nbn:de:0030-drops-153697},
doi = {10.4230/LIPIcs.CALCO.2021.14},
annote = {Keywords: monads, relational structures, Horn theories, relational logic}
}
Document
Stream Processors and Comodels
Abstract
In 2009, Ghani, Hancock and Pattinson gave a coalgebraic characterisation of stream processors A^ℕ → B^ℕ drawing on ideas of Brouwerian constructivism. Their stream processors have an intensional character; in this paper, we give a corresponding coalgebraic characterisation of extensional stream processors, i.e., the set of continuous functions A^ℕ → B^ℕ. Our account sites both our result and that of op. cit. within the apparatus of comodels for algebraic effects originating with Power-Shkaravska.
Cite as
Richard Garner. Stream Processors and Comodels. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{garner:LIPIcs.CALCO.2021.15,
author = {Garner, Richard},
title = {{Stream Processors and Comodels}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.15},
URN = {urn:nbn:de:0030-drops-153700},
doi = {10.4230/LIPIcs.CALCO.2021.15},
annote = {Keywords: Comodels, residual comodels, bimodels, streams, stream processors}
}
Document
A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity
Abstract
By adapting Salomaa’s complete proof system for equality of regular expressions under the language semantics, Milner (1984) formulated a sound proof system for bisimilarity of regular expressions under the process interpretation he introduced. He asked whether this system is complete. Proof-theoretic arguments attempting to show completeness of this equational system are complicated by the presence of a non-algebraic rule for solving fixed-point equations by using star iteration.
We characterize the derivational power that the fixed-point rule adds to the purely equational part Mil- of Milner’s system Mil: it corresponds to the power of coinductive proofs over Mil- that have the form of finite process graphs with the loop existence and elimination property LEE. We define a variant system cMil by replacing the fixed-point rule in Mil with a rule that permits LEE-shaped circular derivations in Mil- from previously derived equations as a premise. With this rule alone we also define the variant system CLC for combining LEE-shaped coinductive proofs over Mil-. We show that both cMil and CLC have proof interpretations in Mil, and vice versa. As this correspondence links, in both directions, derivability in Mil with derivation trees of process graphs, it widens the space for graph-based approaches to finding a completeness proof of Milner’s system.
Cite as
Clemens Grabmayer. A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{grabmayer:LIPIcs.CALCO.2021.16,
author = {Grabmayer, Clemens},
title = {{A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {16:1--16:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.16},
URN = {urn:nbn:de:0030-drops-153712},
doi = {10.4230/LIPIcs.CALCO.2021.16},
annote = {Keywords: regular expressions, process theory, bisimilarity, coinduction, proof theory}
}
Document
Functorial Semantics as a Unifying Perspective on Logic Programming
Abstract
Logic programming and its variations are widely used for formal reasoning in various areas of Computer Science, most notably Artificial Intelligence. In this paper we develop a systematic and unifying perspective for (ground) classical, probabilistic, weighted logic programs, based on categorical algebra. Our departure point is a formal distinction between the syntax and the semantics of programs, now regarded as separate categories. Then, we are able to characterise the various variants of logic program as different models for the same syntax category, i.e. structure-preserving functors in the spirit of Lawvere’s functorial semantics.
As a first consequence of our approach, we showcase a series of semantic constructs for logic programming pictorially as certain string diagrams in the syntax category. Secondly, we describe the correspondence between probabilistic logic programs and Bayesian networks in terms of the associated models. Our analysis reveals that the correspondence can be phrased in purely syntactical terms, without resorting to the probabilistic domain of interpretation.
Cite as
Tao Gu and Fabio Zanasi. Functorial Semantics as a Unifying Perspective on Logic Programming. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{gu_et_al:LIPIcs.CALCO.2021.17,
author = {Gu, Tao and Zanasi, Fabio},
title = {{Functorial Semantics as a Unifying Perspective on Logic Programming}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {17:1--17:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.17},
URN = {urn:nbn:de:0030-drops-153723},
doi = {10.4230/LIPIcs.CALCO.2021.17},
annote = {Keywords: string diagrams, functorial semantics, logic programming}
}
Document
Early Ideas
The Central Valuations Monad (Early Ideas)
Abstract
We give a commutative valuations monad Z on the category DCPO of dcpo’s and Scott-continuous functions. Compared to the commutative valuations monads given in [Xiaodong Jia et al., 2021], our new monad Z is larger and it contains all push-forward images of valuations on the unit interval [0, 1] along lower semi-continuous maps. We believe that this new monad will be useful in giving domain-theoretic denotational semantics for statistical programming languages with continuous probabilistic choice.
Cite as
Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev. The Central Valuations Monad (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 18:1-18:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{jia_et_al:LIPIcs.CALCO.2021.18,
author = {Jia, Xiaodong and Mislove, Michael and Zamdzhiev, Vladimir},
title = {{The Central Valuations Monad}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {18:1--18:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.18},
URN = {urn:nbn:de:0030-drops-153733},
doi = {10.4230/LIPIcs.CALCO.2021.18},
annote = {Keywords: Valuations, Commutative Monad, DCPO, Probabilistic Choice, Recursion}
}
Document
Coderelictions for Free Exponential Modalities
Abstract
In a categorical model of the multiplicative and exponential fragments of intuitionistic linear logic (MELL), the exponential modality is interpreted as a comonad ! such that each cofree !-coalgebra !A comes equipped with a natural cocommutative comonoid structure. An important case is when ! is a free exponential modality so that !A is the cofree cocommutative comonoid over A. A categorical model of MELL with a free exponential modality is called a Lafont category. A categorical model of differential linear logic is called a differential category, where the differential structure can equivalently be described by a deriving transformation !A⊗A →{𝖽_A} !A or a codereliction A →{η_A} !A. Blute, Lucyshyn-Wright, and O'Neill showed that every Lafont category with finite biproducts is a differential category. However, from a differential linear logic perspective, Blute, Lucyshyn-Wright, and O'Neill’s approach is not the usual one since the result was stated in the dual setting and the proof is in terms of the deriving transformation 𝖽. In differential linear logic, it is often the codereliction η that is preferred and that plays a more prominent role. In this paper, we provide an alternative proof that every Lafont category (with finite biproducts) is a differential category, where we construct the codereliction η using the couniversal property of the cofree cocommtuative comonoid !A and show that η is unique. To achieve this, we introduce the notion of an infinitesimal augmentation k⊕A →{𝖧_A} !(k ⊕ A), which in particular is a !-coalgebra and a comonoid morphism, and show that infinitesimal augmentations are in bijective correspondence to coderelictions (and deriving transformations). As such, infinitesimal augmentations provide a new equivalent axiomatization for differential categories in terms of more commonly known concepts. For a free exponential modality, its infinitesimal augmentation is easy to construct and allows one to clearly see the differential structure of a Lafont category, regardless of the construction of !A.
Cite as
Jean-Simon Pacaud Lemay. Coderelictions for Free Exponential Modalities. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{lemay:LIPIcs.CALCO.2021.19,
author = {Lemay, Jean-Simon Pacaud},
title = {{Coderelictions for Free Exponential Modalities}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {19:1--19:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.19},
URN = {urn:nbn:de:0030-drops-153742},
doi = {10.4230/LIPIcs.CALCO.2021.19},
annote = {Keywords: Differential Categories, Coderelictions, Differential Linear Logic, Free Exponential Modalities, Lafont Categories, Infinitesimal Augmentations}
}
Document
The Open Algebraic Path Problem
Abstract
The algebraic path problem provides a general setting for shortest path algorithms in optimization and computer science. We explain the universal property of solutions to the algebraic path problem by constructing a left adjoint functor whose values are given by these solutions. This paper extends the algebraic path problem to networks equipped with input and output boundaries. We show that the algebraic path problem is functorial as a mapping from a double category whose horizontal composition is gluing of open networks. We introduce functional open matrices, for which the functoriality of the algebraic path problem has a more practical expression.
Cite as
Jade Master. The Open Algebraic Path Problem. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{master:LIPIcs.CALCO.2021.20,
author = {Master, Jade},
title = {{The Open Algebraic Path Problem}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {20:1--20:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.20},
URN = {urn:nbn:de:0030-drops-153754},
doi = {10.4230/LIPIcs.CALCO.2021.20},
annote = {Keywords: The Algebraic Path Problem, Open Systems, Shortest Paths, Categorical Semantics, Compositionality}
}
Document
Early Ideas
Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)
Abstract
We describe our ongoing work on generalizing some quantitatively constrained notions of weak simulation up-to that are recently introduced for deterministic systems modeling program execution. We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison between words using a preorder, instead of equality.
Cite as
Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{muroya_et_al:LIPIcs.CALCO.2021.21,
author = {Muroya, Koko and Sanada, Takahiro and Urabe, Natsuki},
title = {{Preorder-Constrained Simulation for Nondeterministic Automata}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {21:1--21:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21},
URN = {urn:nbn:de:0030-drops-153762},
doi = {10.4230/LIPIcs.CALCO.2021.21},
annote = {Keywords: simulation, weak simulation, up-to technique, language inclusion, preorder}
}
Document
Early Ideas
Quantitative Polynomial Functors (Early Ideas)
Abstract
We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.
Cite as
Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 22:1-22:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{nakov_et_al:LIPIcs.CALCO.2021.22,
author = {Nakov, Georgi and Nordvall Forsberg, Fredrik},
title = {{Quantitative Polynomial Functors}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {22:1--22:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22},
URN = {urn:nbn:de:0030-drops-153774},
doi = {10.4230/LIPIcs.CALCO.2021.22},
annote = {Keywords: quantitative type theory, polynomial functors, inductive data types}
}
Document
(Co)algebraic pearls
Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls)
Abstract
We reprove the countable splitting lemma by adapting Nawrotzki’s algorithm which produces a sequence that converges to a solution. Our algorithm combines Nawrotzki’s approach with taking finite cuts. It is constructive in the sense that each term of the iteratively built approximating sequence as well as the error between the approximants and the solution is computable with finitely many algebraic operations.
Cite as
Ana Sokolova and Harald Woracek. Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{sokolova_et_al:LIPIcs.CALCO.2021.23,
author = {Sokolova, Ana and Woracek, Harald},
title = {{Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {23:1--23:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.23},
URN = {urn:nbn:de:0030-drops-153781},
doi = {10.4230/LIPIcs.CALCO.2021.23},
annote = {Keywords: countable splitting lemma, distributions with given marginals, couplings}
}
Document
(Co)algebraic pearls
Minimality Notions via Factorization Systems ((Co)algebraic pearls)
Abstract
For the minimization of state-based systems (i.e. the reduction of the number of states while retaining the system’s semantics), there are two obvious aspects: removing unnecessary states of the system and merging redundant states in the system. In the present article, we relate the two aspects on coalgebras by defining an abstract notion of minimality.
The abstract notion minimality and minimization live in a general category with a factorization system. We will find criteria on the category that ensure uniqueness, existence, and functoriality of the minimization aspects. The proofs of these results instantiate to those for reachability and observability minimization in the standard coalgebra literature. Finally, we will see how the two aspects of minimization interact and under which criteria they can be sequenced in any order, like in automata minimization.
Cite as
Thorsten Wißmann. Minimality Notions via Factorization Systems ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{wimann:LIPIcs.CALCO.2021.24,
author = {Wi{\ss}mann, Thorsten},
title = {{Minimality Notions via Factorization Systems}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {24:1--24:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.24},
URN = {urn:nbn:de:0030-drops-153791},
doi = {10.4230/LIPIcs.CALCO.2021.24},
annote = {Keywords: Coalgebra, Reachability, Observability, Minimization, Factorization System}
}