Volume
LIPIcs, Volume 35
6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO)
Event
CALCO 2015, June 24-26, 2015, Nijmegen, The NetherlandsEditors
Publication Details
- published at: 2015-10-28
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-84-2
- DBLP: db/conf/calco/calco2015
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 35, CALCO'15, Complete Volume
Abstract
LIPIcs, Volume 35, CALCO'15, Complete Volume
Cite as
6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{moss_et_al:LIPIcs.CALCO.2015,
title = {{LIPIcs, Volume 35, CALCO'15, Complete Volume}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015},
URN = {urn:nbn:de:0030-drops-55622},
doi = {10.4230/LIPIcs.CALCO.2015},
annote = {Keywords: Theory of Computation, Logics and Meanings of Programs, Semantics of Programming Languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, List of Authors
Abstract
Front Matter, Table of Contents, Preface, List of Authors
Cite as
6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{moss_et_al:LIPIcs.CALCO.2015.i,
author = {Moss, Lawrence S. and Sobocinski, Pawel},
title = {{Front Matter, Table of Contents, Preface, List of Authors}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {i--xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.i},
URN = {urn:nbn:de:0030-drops-55225},
doi = {10.4230/LIPIcs.CALCO.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, List of Authors}
}
Document
Syntactic Monoids in a Category
Abstract
The syntactic monoid of a language is generalized to the level of a symmetric monoidal closed category D. This allows for a uniform treatment of several notions of syntactic algebras known in the literature, including the syntactic monoids of Rabin and Scott (D = sets), the syntactic semirings of Polák (D = semilattices), and the syntactic associative algebras of Reutenauer (D = vector spaces). Assuming that D is a commutative variety of algebras, we prove that the syntactic D-monoid of a language L can be constructed as a quotient of a free D-monoid modulo the syntactic congruence of L, and that it is isomorphic to the transition D-monoid of the minimal automaton for L in D. Furthermore, in the case where the variety D is locally finite, we characterize the regular languages as precisely the languages with finite syntactic D-monoids.
Cite as
Jiri Adamek, Stefan Milius, and Henning Urbat. Syntactic Monoids in a Category. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2015.1,
author = {Adamek, Jiri and Milius, Stefan and Urbat, Henning},
title = {{Syntactic Monoids in a Category}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {1--16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.1},
URN = {urn:nbn:de:0030-drops-55235},
doi = {10.4230/LIPIcs.CALCO.2015.1},
annote = {Keywords: Syntactic monoid, transition monoid, algebraic automata theory, duality, coalgebra, algebra, symmetric monoidal closed category, commutative variety}
}
Document
Extensions of Functors From Set to V-cat
Abstract
We show that for a commutative quantale V every functor from Set to V-cat has an enriched left-Kan extension. As a consequence, coalgebras over Set are subsumed by coalgebras over V-cat. Moreover, one can build functors on V-cat by equipping Set-functors with a metric.
Cite as
Adriana Balan, Alexander Kurz, and Jiri Velebil. Extensions of Functors From Set to V-cat. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 17-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{balan_et_al:LIPIcs.CALCO.2015.17,
author = {Balan, Adriana and Kurz, Alexander and Velebil, Jiri},
title = {{Extensions of Functors From Set to V-cat}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {17--34},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.17},
URN = {urn:nbn:de:0030-drops-55244},
doi = {10.4230/LIPIcs.CALCO.2015.17},
annote = {Keywords: enriched category, quantale, final coalgebra}
}
Document
Towards Trace Metrics via Functor Lifting
Abstract
We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, by identifying conditions under which also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra in Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.
Cite as
Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Towards Trace Metrics via Functor Lifting. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 35-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.CALCO.2015.35,
author = {Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara},
title = {{Towards Trace Metrics via Functor Lifting}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {35--49},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.35},
URN = {urn:nbn:de:0030-drops-55254},
doi = {10.4230/LIPIcs.CALCO.2015.35},
annote = {Keywords: trace metric, monad lifting, pseudometric, coalgebra}
}
Document
A Fibrational Approach to Automata Theory
Abstract
For predual categories C and D we establish isomorphisms between opfibrations representing local varieties of languages in C, local pseudovarieties of D-monoids, and finitely generated profinite D-monoids. The global sections of these opfibrations are shown to correspond to varieties of languages in C, pseudovarieties of D-monoids, and profinite equational theories of D-monoids, respectively. As an application, a new proof of Eilenberg's variety theorem along with several related results is obtained, covering uniformly varieties of languages and their coalgebraic modifications, Straubing's C-varieties, and fully invariant local varieties.
Cite as
Liang-Ting Chen and Henning Urbat. A Fibrational Approach to Automata Theory. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 50-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CALCO.2015.50,
author = {Chen, Liang-Ting and Urbat, Henning},
title = {{A Fibrational Approach to Automata Theory}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {50--65},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.50},
URN = {urn:nbn:de:0030-drops-55268},
doi = {10.4230/LIPIcs.CALCO.2015.50},
annote = {Keywords: Eilenberg’s variety theorem, duality, coalgebra, Grothendieck fibration}
}
Document
Canonical Coalgebraic Linear Time Logics
Abstract
We extend earlier work on linear time fixpoint logics for coalgebras with branching, by showing how propositional operators arising from the choice of branching monad can be canonically added to these logics. We then consider two semantics for the uniform modal fragments of such logics: the previously-proposed, step-wise semantics and a new semantics akin to those of path-based logics. We prove that the two semantics are equivalent, and show that the canonical choice made for resolving branching in these logics is crucial for this property. We also state conditions under which similar, non-canonical logics enjoy the same property - this applies both to the choice of a branching modality and to the choice of linear time modalities. Our logics allow reasoning about linear time behaviour in systems with non-deterministic, probabilistic or weighted branching. In all these cases, the logics enhanced with propositional operators gain in expressiveness. Another contribution of our work is a reformulation of fixpoint semantics, which applies to any coalgebraic modal logic whose semantics arises from a one-step semantics.
Cite as
Corina Cirstea. Canonical Coalgebraic Linear Time Logics. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 66-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cirstea:LIPIcs.CALCO.2015.66,
author = {Cirstea, Corina},
title = {{Canonical Coalgebraic Linear Time Logics}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {66--85},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.66},
URN = {urn:nbn:de:0030-drops-55274},
doi = {10.4230/LIPIcs.CALCO.2015.66},
annote = {Keywords: coalgebra, linear time logic, fixpoint logic}
}
Document
An Intensionally Fully-abstract Sheaf Model for pi
Abstract
Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.
Cite as
Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An Intensionally Fully-abstract Sheaf Model for pi. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 86-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{eberhart_et_al:LIPIcs.CALCO.2015.86,
author = {Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},
title = {{An Intensionally Fully-abstract Sheaf Model for pi}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {86--100},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.86},
URN = {urn:nbn:de:0030-drops-55284},
doi = {10.4230/LIPIcs.CALCO.2015.86},
annote = {Keywords: concurrency, sheaves, causal models, games}
}
Document
Partial Higher-dimensional Automata
Abstract
We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time.
Cite as
Uli Fahrenberg and Axel Legay. Partial Higher-dimensional Automata. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 101-115, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fahrenberg_et_al:LIPIcs.CALCO.2015.101,
author = {Fahrenberg, Uli and Legay, Axel},
title = {{Partial Higher-dimensional Automata}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {101--115},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.101},
URN = {urn:nbn:de:0030-drops-55295},
doi = {10.4230/LIPIcs.CALCO.2015.101},
annote = {Keywords: higher-dimensional automata, bisimulation}
}
Document
A Recipe for State-and-Effect Triangles
Abstract
In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced 'state-and-effect' triangles which captures this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, both for the Boolean and probabilistic (quantitative) case.
Cite as
Bart Jacobs. A Recipe for State-and-Effect Triangles. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 116-129, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{jacobs:LIPIcs.CALCO.2015.116,
author = {Jacobs, Bart},
title = {{A Recipe for State-and-Effect Triangles}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {116--129},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.116},
URN = {urn:nbn:de:0030-drops-55301},
doi = {10.4230/LIPIcs.CALCO.2015.116},
annote = {Keywords: Duality, predicate transformer, state transformer, state-and-effect triangle}
}
Document
Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra
Abstract
While computer programs and logical theories begin by declaring the concepts of interest, be it as data types or as predicates, network computation does not allow such global declarations, and requires concept mining and concept analysis to extract shared semantics for different network nodes. Powerful semantic analysis systems have been the drivers of nearly all paradigm shifts on the web. In categorical terms, most of them can be described as bicompletions of enriched matrices, generalizing the Dedekind-MacNeille-style completions from posets to suitably enriched categories. Yet it has been well known for more than 40 years that ordinary categories themselves in general do not permit such completions. Armed with this new semantical view of Dedekind-MacNeille completions, and of matrix bicompletions, we take another look at this ancient mystery. It turns out that simple categorical versions of the limit superior and limit inferior operations characterize a general notion of Dedekind-MacNeille completion, that seems to be appropriate for ordinary categories, and boils down to the more familiar enriched versions when the limits inferior and superior coincide. This explains away the apparent gap among the completions of ordinary categories, and broadens the path towards categorical concept mining and analysis, opened in previous work.
Cite as
Toshiki Kataoka and Dusko Pavlovic. Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 130-155, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kataoka_et_al:LIPIcs.CALCO.2015.130,
author = {Kataoka, Toshiki and Pavlovic, Dusko},
title = {{Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {130--155},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.130},
URN = {urn:nbn:de:0030-drops-55317},
doi = {10.4230/LIPIcs.CALCO.2015.130},
annote = {Keywords: concept analysis, semantic indexing, category, completion, algebra}
}
Document
Codensity Liftings of Monads
Abstract
We introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the categorical >>-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We next study the liftings of algebraic operations to the codensity-lifted monads. We also give a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.
Cite as
Shin-ya Katsumata and Tetsuya Sato. Codensity Liftings of Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 156-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{katsumata_et_al:LIPIcs.CALCO.2015.156,
author = {Katsumata, Shin-ya and Sato, Tetsuya},
title = {{Codensity Liftings of Monads}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {156--170},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.156},
URN = {urn:nbn:de:0030-drops-55329},
doi = {10.4230/LIPIcs.CALCO.2015.156},
annote = {Keywords: Monads, Lifting, Fibration, Giry Monad}
}
Document
A First-order Logic for String Diagrams
Abstract
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes. In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic with conjunction, implication, and universal quantification over !-boxes. This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes. We then build a standard model for !L and give an example proof of a theorem for non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
Cite as
Aleks Kissinger and David Quick. A First-order Logic for String Diagrams. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 171-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kissinger_et_al:LIPIcs.CALCO.2015.171,
author = {Kissinger, Aleks and Quick, David},
title = {{A First-order Logic for String Diagrams}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {171--189},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.171},
URN = {urn:nbn:de:0030-drops-55335},
doi = {10.4230/LIPIcs.CALCO.2015.171},
annote = {Keywords: string diagrams, compact closed monoidal categories, abstract tensor systems, first-order logic}
}
Document
Presenting Morphisms of Distributive Laws
Abstract
A format for well-behaved translations between structural operational specifications is derived from a notion of distributive law morphism, previously studied by Power and Watanabe.
Cite as
Bartek Klin and Beata Nachyla. Presenting Morphisms of Distributive Laws. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 190-204, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{klin_et_al:LIPIcs.CALCO.2015.190,
author = {Klin, Bartek and Nachyla, Beata},
title = {{Presenting Morphisms of Distributive Laws}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {190--204},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.190},
URN = {urn:nbn:de:0030-drops-55343},
doi = {10.4230/LIPIcs.CALCO.2015.190},
annote = {Keywords: coalgebra, bialgebra, distributive law, structural operational semantics}
}
Document
Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
Abstract
The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.
Cite as
Alexander Kurz, Alberto Pardo, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 205-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kurz_et_al:LIPIcs.CALCO.2015.205,
author = {Kurz, Alexander and Pardo, Alberto and Petrisan, Daniela and Severi, Paula and de Vries, Fer-Jan},
title = {{Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {205--220},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.205},
URN = {urn:nbn:de:0030-drops-55351},
doi = {10.4230/LIPIcs.CALCO.2015.205},
annote = {Keywords: coalgebra, Bekic lemma, infinite data, functional programming, type theory}
}
Document
Final Coalgebras from Corecursive Algebras
Abstract
We give a technique to construct a final coalgebra in which each element is a set of formulas of modal logic. The technique works for both the finite and the countable powerset functors. Starting with an injectively structured, corecursive algebra, we coinductively obtain a suitable subalgebra called the "co-founded part". We see—first with an example, and then in the general setting of modal logic on a dual adjunction—that modal theories form an injectively structured, corecursive algebra, so that this construction may be applied. We also obtain an initial algebra in a similar way.
We generalize the framework beyond Set to categories equipped with a suitable factorization system, and look at the examples of Poset and Set-op .
Cite as
Paul Blain Levy. Final Coalgebras from Corecursive Algebras. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 221-237, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{levy:LIPIcs.CALCO.2015.221,
author = {Levy, Paul Blain},
title = {{Final Coalgebras from Corecursive Algebras}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {221--237},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.221},
URN = {urn:nbn:de:0030-drops-55365},
doi = {10.4230/LIPIcs.CALCO.2015.221},
annote = {Keywords: coalgebra, modal logic, bisimulation, category theory, factorization system}
}
Document
Uniform Interpolation for Coalgebraic Fixpoint Logic
Abstract
We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e., functors with quasifunctorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.
Cite as
Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform Interpolation for Coalgebraic Fixpoint Logic. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 238-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{marti_et_al:LIPIcs.CALCO.2015.238,
author = {Marti, Johannes and Seifan, Fatemeh and Venema, Yde},
title = {{Uniform Interpolation for Coalgebraic Fixpoint Logic}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {238--252},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.238},
URN = {urn:nbn:de:0030-drops-55379},
doi = {10.4230/LIPIcs.CALCO.2015.238},
annote = {Keywords: mu-calculus, uniform interpolation, coalgebra, automata}
}
Document
Generic Trace Semantics and Graded Monads
Abstract
Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. In the present paper, we refine this abstraction to use graded monads, which come with a notion of depth that corresponds, e.g., to trace length or bisimulation depth. We introduce a notion of graded algebras and show how they play the role of formulas in trace logics.
Cite as
Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic Trace Semantics and Graded Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 253-269, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{milius_et_al:LIPIcs.CALCO.2015.253,
author = {Milius, Stefan and Pattinson, Dirk and Schr\"{o}der, Lutz},
title = {{Generic Trace Semantics and Graded Monads}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {253--269},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.253},
URN = {urn:nbn:de:0030-drops-55389},
doi = {10.4230/LIPIcs.CALCO.2015.253},
annote = {Keywords: transition systems, monads, coalgebra, trace logics}
}
Document
Open System Categorical Quantum Semantics in Natural Language Processing
Abstract
Originally inspired by categorical quantum mechanics (Abramsky and Coecke, LiCS'04), the categorical compositional distributional model of natural language meaning of Coecke, Sadrzadeh and Clark provides a conceptually motivated procedure to compute the meaning of a sentence, given its grammatical structure within a Lambek pregroup and a vectorial representation of the meaning of its parts. Moreover, just like CQM allows for varying the model in which we interpret quantum axioms, one can also vary the model in which we interpret word meaning.
In this paper we show that further developments in categorical quantum mechanics are relevant to natural language processing too. Firstly, Selinger's CPM-construction allows for explicitly taking into account lexical ambiguity and distinguishing between the two inherently different notions of homonymy and polysemy. In terms of the model in which we interpret word meaning, this means a passage from the vector space model to density matrices. Despite this change of model, standard empirical methods for comparing meanings can be easily adopted, which we demonstrate by a small-scale experiment on real-world data. Secondly, commutative classical structures as well as their non-commutative counterparts that arise in the image of the CPM-construction allow for encoding relative pronouns, verbs and adjectives, and finally, iteration of the CPM-construction, something that has no counterpart in the quantum realm, enables one to accommodate both entailment and ambiguity.
Cite as
Robin Piedeleu, Dimitri Kartsaklis, Bob Coecke, and Mehrnoosh Sadrzadeh. Open System Categorical Quantum Semantics in Natural Language Processing. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 270-289, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{piedeleu_et_al:LIPIcs.CALCO.2015.270,
author = {Piedeleu, Robin and Kartsaklis, Dimitri and Coecke, Bob and Sadrzadeh, Mehrnoosh},
title = {{Open System Categorical Quantum Semantics in Natural Language Processing}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {270--289},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.270},
URN = {urn:nbn:de:0030-drops-55398},
doi = {10.4230/LIPIcs.CALCO.2015.270},
annote = {Keywords: category theory, density matrices, distributional models, semantics}
}
Document
Modules Over Monads and Their Algebras
Abstract
Modules over monads (or: actions of monads on endofunctors) are structures in which a monad interacts with an endofunctor, composed either on the left or on the right. Although usually not explicitly identified as such, modules appear in many contexts in programming and semantics. In this paper, we investigate the elementary theory of modules. In particular, we identify the monad freely generated by a right module as a generalisation of Moggi's resumption monad and characterise its algebras, extending previous results by Hyland, Plotkin and Power, and by Filinski and Stovring. Moreover, we discuss a connection between modules and algebraic effects: left modules have a similar feeling to Eilenberg–Moore algebras, and can be seen as handlers that are natural in the variables, while right modules can be seen as functions that run effectful computations in an appropriate context (such as an initial state for a stateful computation).
Cite as
Maciej Pirog, Nicolas Wu, and Jeremy Gibbons. Modules Over Monads and Their Algebras. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 290-303, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{pirog_et_al:LIPIcs.CALCO.2015.290,
author = {Pirog, Maciej and Wu, Nicolas and Gibbons, Jeremy},
title = {{Modules Over Monads and Their Algebras}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {290--303},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.290},
URN = {urn:nbn:de:0030-drops-55404},
doi = {10.4230/LIPIcs.CALCO.2015.290},
annote = {Keywords: monad, module over monad, algebraic data types, resumptions, free object}
}
Document
Revisiting the Institutional Approach to Herbrand’s Theorem
Abstract
More than a decade has passed since Herbrand’s theorem was first generalized to arbitrary institutions, enabling in this way the development of the logic-programming paradigm over formalisms beyond the conventional framework of relational first-order logic. Despite the mild assumptions of the original theory, recent developments have shown that the institution-based approach cannot capture constructions that arise when service-oriented computing is presented as a form of logic programming, thus prompting the need for a new perspective on Herbrand’s theorem founded instead upon a concept of generalized substitution system. In this paper, we formalize the connection between the institution- and the substitution-system-based approach to logic programming by investigating a number of features of institutions, like the existence of a quantification space or of representable substitutions, under which they give rise to suitable generalized substitution systems. Building on these results, we further show how the original institution independent versions of Herbrand’s theorem can be obtained as concrete instances of a more general result.
Cite as
Ionut Tutu and José Luiz Fiadeiro. Revisiting the Institutional Approach to Herbrand’s Theorem. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 304-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{tutu_et_al:LIPIcs.CALCO.2015.304,
author = {Tutu, Ionut and Fiadeiro, Jos\'{e} Luiz},
title = {{Revisiting the Institutional Approach to Herbrand’s Theorem}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {304--319},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.304},
URN = {urn:nbn:de:0030-drops-55419},
doi = {10.4230/LIPIcs.CALCO.2015.304},
annote = {Keywords: Institution theory, Substitution systems, Herbrand’s theorem}
}
Document
Coalgebraic Infinite Traces and Kleisli Simulations
Abstract
Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various types of systems. A generic categorical theory behind Kleisli simulation has been developed and it guarantees the soundness of those simulations wrt. finite trace semantics. Moreover, those simulations can be aided by forward partial execution (FPE) - a categorical transformation of systems previously introduced by the authors.
In this paper, we give Kleisli simulation a theoretical foundation that assures its soundness also wrt. infinite trace. There, following Jacobs' work, infinite trace semantics is characterized as the "largest homomorphism." It turns out that soundness of forward simulations is rather straightforward; that of backward simulation holds too, although it requires certain additional conditions and its proof is more involved. We also show that FPE can be successfully employed in the infinite trace setting to enhance the applicability of Kleisli simulations as witnesses of trace inclusion. Our framework is parameterized in the monad for branching as well as in the functor for linear-time behaviors; for the former we use the powerset monad (for nondeterminism) as well as the sub-Giry monad (for probability).
Cite as
Natsuki Urabe and Ichiro Hasuo. Coalgebraic Infinite Traces and Kleisli Simulations. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 320-335, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{urabe_et_al:LIPIcs.CALCO.2015.320,
author = {Urabe, Natsuki and Hasuo, Ichiro},
title = {{Coalgebraic Infinite Traces and Kleisli Simulations}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {320--335},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.320},
URN = {urn:nbn:de:0030-drops-55424},
doi = {10.4230/LIPIcs.CALCO.2015.320},
annote = {Keywords: category theory, coalgebra, simulation, verification, trace semantics}
}
Document
Finitary Corecursion for the Infinitary Lambda Calculus
Abstract
Kurz et al. have recently shown that infinite lambda-trees with finitely many free variables modulo alpha-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational lambda-trees, i.e. those lambda-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational lambda-trees.
Cite as
Stefan Milius and Thorsten Wißmann. Finitary Corecursion for the Infinitary Lambda Calculus. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 336-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{milius_et_al:LIPIcs.CALCO.2015.336,
author = {Milius, Stefan and Wi{\ss}mann, Thorsten},
title = {{Finitary Corecursion for the Infinitary Lambda Calculus}},
booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
pages = {336--351},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-84-2},
ISSN = {1868-8969},
year = {2015},
volume = {35},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.336},
URN = {urn:nbn:de:0030-drops-55436},
doi = {10.4230/LIPIcs.CALCO.2015.336},
annote = {Keywords: rational trees, infinitary lambda calculus, coinduction}
}