6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands
CALCO 2015
June 24-26, 2015
Nijmegen, The Netherlands
Conference on Algebra and Coalgebra in Computer Science
CALCO
https://coalg.org/
https://dblp.org/db/conf/calco
Leibniz International Proceedings in Informatics
LIPIcs
https://www.dagstuhl.de/dagpub/1868-8969
https://dblp.org/db/series/lipics
1868-8969
Lawrence S.
Moss
Lawrence S. Moss
Pawel
Sobocinski
Pawel Sobocinski
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
35
2015
978-3-939897-84-2
https://www.dagstuhl.de/dagpub/978-3-939897-84-2
Front Matter, Table of Contents, Preface, List of Authors
Front Matter, Table of Contents, Preface, List of Authors
Front Matter
Table of Contents
Preface
List of Authors
i-xii
Front Matter
Lawrence S.
Moss
Lawrence S. Moss
Pawel
Sobocinski
Pawel Sobocinski
10.4230/LIPIcs.CALCO.2015.i
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Syntactic Monoids in a Category
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.
Syntactic monoid
transition monoid
algebraic automata theory
duality
coalgebra
algebra
symmetric monoidal closed category
commutative variety
1-16
Regular Paper
Jiri
Adamek
Jiri Adamek
Stefan
Milius
Stefan Milius
Henning
Urbat
Henning Urbat
10.4230/LIPIcs.CALCO.2015.1
Jiř\'ıAdámek, Stefan Milius, , and Henning Urbat. Syntactic monoids in a category. Extended version. http://arxiv.org/abs/1504.02694, 2015.
http://arxiv.org/abs/1504.02694
Jiř\'ıAdámek, Stefan Milius, Robert S. R. Myers, and Henning Urbat. Generalized Eilenberg Theorem I: Local Varieties of Languages. In Anca Muscholl, editor, Proc. Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412 of Lecture Notes Comput. Sci., pages 366-380. Springer, 2014.
Jiř\'ıAdámek, Stefan Milius, Robert S. R. Myers, and Henning Urbat. On continuous nondeterminism and state minimality. In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, Proc. Mathematical Foundations of Programming Science (MFPS XXX), volume 308 of Electron. Notes Theor. Comput. Sci., pages 3-23. Elsevier, 2014.
Jiř\'ıAdámek, Stefan Milius, Robert S. R. Myers, and Henning Urbat. Varieties of Languages in a Category. Accepted for LICS 2015. http://arxiv.org/abs/1501.05180, 2015.
http://arxiv.org/abs/1501.05180
A. Ballester-Bolinches, E. Cosme-Llopez, and J.J.M.M. Rutten. The dual equivalence of equations and coequations for automata. Technical report, CWI, 2014.
Bernhard Banaschweski and Evelyn Nelson. Tensor products and bimorphisms. Canad. Math. Bull., 19:385-402, 1976.
Nick Bezhanishvili, Clemens Kupke, and Prakash Panangaden. Minimization via duality. In Luke Ong and Ruy de Queiroz, editors, Logic, Language, Information and Computation, volume 7456 of Lecture Notes in Computer Science, pages 191-205. Springer Berlin Heidelberg, 2012.
Mikołaj Bojánczyk. Recognisable languages over monads. Preprint: http://arxiv.org/abs/1502.04898, 2015.
http://arxiv.org/abs/1502.04898
Mikołaj Bojánczyk and Igor Walukiewicz. Forest algebras. In Automata and Logic: History and Perspectives, pages 107-132, 2006.
Marcello M. Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14(1:7), 2013.
Mai Gehrke, Serge Grigorieff, and Jean-Éric Pin. Duality and equational theory of regular languages. In Proc. ICALP 2008, Part II, volume 5126 of Lecture Notes Comput. Sci., pages 246-257. Springer, 2008.
Joseph A. Goguen. Discrete-time machines in closed monoidal categories. I. J. Comput. Syst. Sci., 10(1):1-43, 1975.
Anders Kock. Monads on symmetric monoidal closed categories. Arch. Math., 21:1-10, 1970.
Saunders Mac Lane. Categories for the working mathematician. Springer, 2nd edition, 1998.
Fred Linton. Autonomous equational categories. J. Math. Mech., 15:637-642, 166.
Robert S. R. Myers, Jiř\'ıAdámek, Stefan Milius, and Henning Urbat. Canonical nondeterministic automata. In Marcello M. Bonsangue, editor, Proc. Coalgebraic Methods in Computer Science (CMCS'14), volume 8446 of Lecture Notes Comput. Sci., pages 189-210. Springer, 2014.
Jean-Éric Pin. Mathematical foundations of automata theory. available at http://www.liafa.jussieu.fr/~jep/PDF/MPRI/MPRI.pdf, January 2015.
http://www.liafa.jussieu.fr/~jep/PDF/MPRI/MPRI.pdf
Libor Polák. Syntactic semiring of a language. In Jiř\'ıSgall, Aleš Pultr, and Petr Kolman, editors, Proc. International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 2136 of Lecture Notes Comput. Sci., pages 611-620. Springer, 2001.
Michael O. Rabin and Dana S. Scott. Finite automata and their decision problems. IBM J. Res. Dev., 3(2):114-125, April 1959.
Christophe Reutenauer. Séries formelles et algèbres syntactiques. J. Algebra, 66:448-483, 1980.
Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000.
Thomas Wilke. An Eilenberg Theorem for Infinity-Languages. In Proc. ICALP 91, pages 588-599. Springer, 1991.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Extensions of Functors From Set to V-cat
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.
enriched category
quantale
final coalgebra
17-34
Regular Paper
Adriana
Balan
Adriana Balan
Alexander
Kurz
Alexander Kurz
Jiri
Velebil
Jiri Velebil
10.4230/LIPIcs.CALCO.2015.17
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Towards Trace Metrics via Functor Lifting
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.
trace metric
monad lifting
pseudometric
coalgebra
35-49
Regular Paper
Paolo
Baldan
Paolo Baldan
Filippo
Bonchi
Filippo Bonchi
Henning
Kerstan
Henning Kerstan
Barbara
König
Barbara König
10.4230/LIPIcs.CALCO.2015.35
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On the total variation distance of semi-markov chains. In Foundations of Software Science and Computation Structures (FOSSACS 2015), volume 9034 of Lecture Notes in Computer Science. Springer, 2015.
Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pages 403-415. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.
Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up to in a fibrational setting. In Proc. of CSL-LICS'14, 2014.
Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In CONCUR 2014 - Concurrency Theory, Lecture Notes in Computer Science, pages 32-46, 2014.
Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quantitative transition systems. In Proc. of ICALP'04, volume 3142 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004.
Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Transactions on Software Engineering, 25(2), 2009.
Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, 2004.
Uli Fahrenberg, Axel Legay, and Claus Thrane. The quantitative linear-time-branching-time spectrum. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), volume 13 of Leibniz International Proceedings in Informatics (LIPIcs), pages 103-114. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011.
Daniel Gebler and Simone Tini. Compositionality of approximate bisimulation for probabilistic systems. In Proc. of EXPRESS/SOS'13, pages 32-46, 2013.
Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, pages 443-458. North-Holland, 1990.
Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3 (4:11):1-36, November 2007.
Bart Jacobs. Introduction to coalgebra. Towards mathematics of states and observations, 2012. Draft.
Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, volume 7399 of Lecture Notes in Computer Science, pages 109-129. Springer Berlin Heidelberg, 2012.
Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. Journal of Computer and System Sciences, 81(5):859-879, 2015. 11th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2012 (Selected Papers).
Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011.
E.G. Manes and M.A. Arbib. Algebraic approaches to program semantics. Texts and Monographs in Computer Science, 1986.
John Power and Daniele Turi. A coalgebraic foundation for linear time semantics. Electronic Notes in Theoretical Computer Science, 29:259-274, 1999.
J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3-80, 2000.
Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2-3):230-247, 2008.
Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013.
Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proc. of LICS'97, pages 280-291, 1997.
Franck van Breugel. The metric monad for probabilistic nondeterminism, April 2005.
Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331:115-142, 2005.
Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theoretical Computer Science, 360(1):373-385, 2006.
Cédric Villani. Optimal Transport - Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics. Springer, 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A Fibrational Approach to Automata Theory
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.
Eilenberg’s variety theorem
duality
coalgebra
Grothendieck fibration
50-65
Regular Paper
Liang-Ting
Chen
Liang-Ting Chen
Henning
Urbat
Henning Urbat
10.4230/LIPIcs.CALCO.2015.50
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Canonical Coalgebraic Linear Time Logics
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.
coalgebra
linear time logic
fixpoint logic
66-85
Regular Paper
Corina
Cirstea
Corina Cirstea
10.4230/LIPIcs.CALCO.2015.66
Corina Cîrstea. From branching to linear time, coalgebraically. In Proceedings, FICS 2013, pages 11-27, 2013.
Corina Cîrstea. A coalgebraic approach to linear-time logics. In Proceedings, FOSSACS 2014, pages 426-440, 2014.
Corina Cîrstea and Dirk Pattinson. Modular construction of complete coalgebraic logics. Theor. Comput. Sci., 388(1-3):83-108, 2007.
Dion Coumans and Bart Jacobs. Scalars, monads, and categories. In Quantum Physics and Linguistics. A Compositional, Diagrammatic Discourse, pages 184-216. Oxford Univ. Press, 2013.
B.A. Davey and H.A. Priestley. Introduction to Lattices and Order (2. ed.). Cambridge University Press, 2002.
Ichiro Hasuo. Generic weakest precondition semantics from monads enriched with order. In Proceedings, CMCS 2014, pages 10-32, 2014.
Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4), 2007.
Michael Huth and Marta Z. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, LICS 1997, pages 111-122, 1997.
Bart Jacobs. Introduction to coalgebra. Towards mathematics of states and observations. Draft.
Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Proceedings, CMCS 2012, pages 109-129, 2012.
Christian Kissig and Alexander Kurz. Generic trace logics. CoRR, abs/1103.3239, 2011.
Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. In Proceedings, FOSSACS 2015, pages 151-166, 2015.
Anders Kock. Monads and extensive quantities, 2011. arXiv:1103.6009.
Anders Kock. Commutative monads as a theory of distributions. Theory and Applications of Categories, 26(4):97-131, 2012.
Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Algebraic semantics for coalgebraic logics. Electr. Notes Theor. Comput. Sci., 106:219-241, 2004.
Clemens Kupke, Alexander Kurz, and Yde Venema. Stone coalgebras. Theor. Comput. Sci., 327(1-2):109-134, 2004.
Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. This volume.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
An Intensionally Fully-abstract Sheaf Model for pi
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.
concurrency
sheaves
causal models
games
86-100
Regular Paper
Clovis
Eberhart
Clovis Eberhart
Tom
Hirschowitz
Tom Hirschowitz
Thomas
Seiller
Thomas Seiller
10.4230/LIPIcs.CALCO.2015.86
Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409-470, 2000.
Gérard Berry and Gérard Boudol. The chemical abstract machine. In POPL, pages 81-94, 1990.
Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, and Alexandra Silva. Deriving syntax and axioms for quantitative regular behaviours. In CONCUR, volume 5710 of LNCS, pages 146-162. Springer, 2009.
Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the π-calculus. Acta Informatica, 35(5):353-400, 1998.
Ed Brinksma, Arend Rensink, and Walter Vogler. Fair testing. In CONCUR, volume 962 of LNCS, pages 313-327. Springer, 1995.
Nadia Busi and Roberto Gorrieri. Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs. Journal of Logic and Algebraic Programming, 78(3):138-162, 2009.
Diletta Cacciagrano, Flavio Corradini, and Catuscia Palamidessi. Explicit fairness in testing semantics. Logical Methods in Computer Science, 5(2), 2009.
Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of pcf. In LICS. IEEE Computer Society, 2015.
Gian Luca Cattani and Peter Sewell. Models for name-passing processes: Interleaving and causal. In LICS, pages 322-333. IEEE Computer Society, 2000.
Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. Event structure semantics of parallel extrusion in the pi-calculus. In FoSSaCS, volume 7213 of LNCS, pages 225-239. Springer, 2012.
Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984.
Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. A πlayground. http://lama.univ-smb.fr/~hirschowitz/papers/pilayground.pdf, 2015.
http://lama.univ-smb.fr/~hirschowitz/papers/pilayground.pdf
Joost Engelfriet. A multiset semantics for the pi-calculus with replication. Theoretical Computer Science, 153(1&2):65-94, 1996.
Marcelo P. Fiore, Eugenio Moggi, and Davide Sangiorgi. A fully-abstract model for the pi-calculus (extended abstract). In LICS, pages 43-54. IEEE Computer Society, 1996.
Peter Freyd and G. M. Kelly. Categories of continuous functors, I. Journal of Pure and Applied Algebra, 2:169-191, 1972.
Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, 2001.
Gregor Gößler, Daniel Le Métayer, and Jean-Baptiste Raclet. Causality analysis in contract violation. In Runtime Verification, volume 6418 of LNCS, pages 270-284. Springer, 2010.
Russell Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for innocent strategies. In LICS, pages 379-388. IEEE Computer Society, 2007.
Matthew Hennessy. A fully abstract denotational semantics for the π-calculus. Theoretical Computer Science, 278(1-2):53-89, 2002.
Thomas T. Hildebrandt. Towards categorical models for fairness: fully abstract presheaf semantics of SCCS with finite delay. Theoretical Computer Science, 294(1/2):151-181, 2003.
Tom Hirschowitz. Full abstraction for fair testing in CCS. In CALCO, volume 8089 of LNCS, pages 175-190. Springer, 2013.
Tom Hirschowitz. Full abstraction for fair testing in CCS (expanded version). Logical Methods in Computer Science, 10(4), 2014.
Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive equivalences for CCS. In ICE, pages 2-24, 2011.
J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000.
Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999.
André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps. In LICS, pages 418-427. IEEE Computer Society, 1993.
James Laird. Game semantics for higher-order concurrency. In FSTTCS, volume 4337 of LNCS, pages 417-428. Springer, 2006.
Saunders Mac Lane. Duality for groups. Bulletin of the American Mathematical Society, 56, 1950.
Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer, 2nd edition, 1998.
Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. Springer, 1992.
Guy McCusker, John Power, and Cai Wingfield. A graphical foundation for schedules. Electronic Notes in Theoretical Computer Science, 286:273-289, 2012.
Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional linear logic. In LICS, pages 386-395. IEEE Computer Society, 2005.
Paul-André Melliès. Game semantics in string diagrams. In LICS, pages 481-490. IEEE, 2012.
Ugo Montanari and Marco Pistore. Concurrent semantics for the π-calculus. Electronic Notes in Theoretical Computer Science, 1:411-429, 1995.
V. Natarajan and Rance Cleaveland. Divergence and fair testing. In ICALP, volume 944 of LNCS, pages 648-659. Springer, 1995.
Hanno Nickau. Hereditarily sequential functionals. In LFCS, volume 813 of LNCS, pages 253-264. Springer, 1994.
M. Nielsen, G. Plotkin, and G. Winskel. Event structures and domains, part 1. Theoretical Computer Science, 13:65-108, 1981.
Arend Rensink and Walter Vogler. Fair testing. Information and Computation, 205(2):125-198, 2007.
Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, pages 409-418. IEEE Computer Society, 2011.
Ian Stark. A fully abstract domain model for the π-calculus. In LICS, pages 36-42. IEEE Computer Society, 1996.
Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In LICS. IEEE Computer Society, 2015.
Glynn Winskel. Event structure semantics for CCS and related languages. In Mogens Nielsen and Erik Meineche Schmidt, editors, ICALP, volume 140 of LNCS, pages 561-576. Springer, 1982.
Glynn Winskel. Strategies as profunctors. In FoSSaCS, volume 7794 of LNCS, pages 418-433. Springer, 2013.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Partial Higher-dimensional Automata
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.
higher-dimensional automata
bisimulation
101-115
Regular Paper
Uli
Fahrenberg
Uli Fahrenberg
Axel
Legay
Axel Legay
10.4230/LIPIcs.CALCO.2015.101
Marek A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, UK, 1987.
Jan A. Bergstra and Jan W. Klop. Process algebra for synchronous communication. Inf. Cont., 60(1-3):109-137, 1984.
Ronald Brown and Philip J. Higgins. \afirstOn the algebra of cubes. J. Pure Appl. Alg., 21:233-260, 1981.
Uli Fahrenberg. A category of higher-dimensional automata. In FOSSACS, volume 3441 of Lect. Notes Comput. Sci., pages 187-201. Springer, 2005.
Uli Fahrenberg. Higher-Dimensional Automata from a Topological Viewpoint. PhD thesis, Aalborg University, Denmark, 2005.
Uli Fahrenberg and Axel Legay. History-preserving bisimilarity for higher-dimensional automata via open maps. Electr. Notes Theor. Comput. Sci., 298:165-178, 2013.
Uli Fahrenberg and Axel Legay. Homotopy bisimilarity for higher-dimensional automata. CoRR, abs/1409.5865, 2014.
Lisbeth Fajstrup. Dipaths and dihomotopies in a cubical complex. Adv. Appl. Math., 35(2):188-206, 2005.
Lisbeth Fajstrup, Éric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raußen. Trace spaces: An efficient new technique for state-space reduction. In Helmut Seidl, editor, ESOP, volume 7211 of Lecture Notes in Computer Science, pages 274-294. Springer, 2012.
Lisbeth Fajstrup, Martin Raussen, and Éric Goubault. Algebraic topology and concurrency. Theor. Comput. Sci., 357(1-3):241-278, 2006.
Philippe Gaucher. Homotopical interpretation of globular complex by multipointed d-space. Theory Appl. Categories, 22:588-621, 2009.
Philippe Gaucher. Towards a homotopy theory of higher dimensional transition systems. Theory Appl. Categories, 25:295-341, 2011.
Éric Goubault. Geometry and concurrency: A user’s guide. Math. Struct. Comput. Sci., 10(4):411-425, 2000.
Éric Goubault and Thomas P. Jensen. Homology of higher dimensional automata. In Rance Cleaveland, editor, CONCUR, volume 630 of Lect. Notes Comput. Sci., pages 254-268. Springer, 1992.
Éric Goubault and Samuel Mimram. Formal relationships between geometrical and classical models for concurrency. Electronic Notes in Theoretical Computer Science, 283:77-109, 2012.
Marco Grandis. Directed algebraic topology: models of non-reversible worlds. New mathematical monographs. Cambridge Univ. Press, 2009.
André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Inf. Comput., 127(2):164-185, 1996.
Dexter Kozen. Automata and Computability. Undergraduate Texts in Computer Science. Springer, 1997.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. Theor. Comput. Sci., 13:85-108, 1981.
David M.R. Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, IFIP TCS, volume 104 of Lect. Notes Comput. Sci., pages 167-183. Springer, 1981.
Carl A. Petri. Kommunikation mit Automaten. Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 2, 1962.
Vaughan Pratt. Modeling concurrency with geometry. In POPL, pages 311-322. ACM Press, 1991.
Cristian Prisacariu. The glory of the past and geometrical concurrency. In Andrei Voronkov, editor, Turing-100, volume 10 of EPiC, pages 252-267. EasyChair, 2012.
Alexander M. Rabinovich and Boris A. Trakhtenbrot. Behavior structures and nets. Fund. Inf., 11(4):357-403, 1988.
Jean-Pierre Serre. Homologie singulière des espaces fibrés. PhD thesis, Ecole Normale Supérieure, 1951.
Mike W. Shields. Concurrent machines. The Computer Journal, 28(5):449-465, 1985.
Colin Stirling. Modal and temporal logics for processes. In Proc. Banff Higher Order Workshop, volume 1043 of Lect. Notes Comput. Sci., pages 149-237. Springer, 1995.
Rob J. van Glabbeek. Bisimulations for higher dimensional automata. Email message, June 1991. URL: http://theory.stanford.edu/~rvg/hda.
http://theory.stanford.edu/~rvg/hda
Rob J. van Glabbeek. \afirstOn the expressiveness of higher dimensional automata. Theor. Comput. Sci., 356(3):265-290, 2006.
Rob J. van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Inf., 37(4/5):229-327, 2001.
Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures, event structures and petri nets. Theor. Comput. Sci., 410(41):4111-4159, 2009.
Rob J. van Glabbeek and Frits W. Vaandrager. Petri net models for algebraic theories of concurrency. In J. W. de Bakker, A. J. Nijman, and Philip C. Treleaven, editors, PARLE (2), volume 259 of Lect. Notes Comput. Sci., pages 224-242. Springer, 1987.
Rob J. van Glabbeek and Frits W. Vaandrager. The difference between splitting in n and n+1. Inf. Comput., 136(2):109-142, 1997.
Glynn Winskel and Mogens Nielsen. Models for concurrency. In Samson Abramsky, Dov M. Gabbay, and Thomas S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4. Clarendon Press, Oxford, 1995.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A Recipe for State-and-Effect Triangles
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.
Duality
predicate transformer
state transformer
state-and-effect triangle
116-129
Regular Paper
Bart
Jacobs
Bart Jacobs
10.4230/LIPIcs.CALCO.2015.116
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra
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.
concept analysis
semantic indexing
category
completion
algebra
130-155
Regular Paper
Toshiki
Kataoka
Toshiki Kataoka
Dusko
Pavlovic
Dusko Pavlovic
10.4230/LIPIcs.CALCO.2015.130
Yossi Azar, Amos Fiat, Anna Karlin, Frank McSherry, and Jared Saia. Spectral analysis of data. In Proceedings of the thirty-third annual ACM Symposium on Theory of Computing, STOC'01, pages 619-626, New York, NY, USA, 2001. ACM.
Bernhard Banaschewski and Gunter Bruns. Categorical characterization of the MacNeille completion. Archiv der Mathematik, 18(4):369-377, September 1967.
Michael Barr and Charles Wells. Toposes, Triples, and Theories. Number 278 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.
Claudio Carpineto and Giovanni Romano. Concept Data Analysis: Theory and Applications. John Wiley & Sons, 2004.
Richard O. Duda, Peter E. Hart, and David G. Stork. Pattern Classification. Wiley-Interscience, 2000.
Bernhard Ganter, Gerd Stumme, and Rudolf Wille, editors. Formal Concept Analysis, Foundations and Applications, volume 3626 of Lecture Notes in Computer Science. Springer, 2005.
Bernhard Ganter and Rudolf Wille. Formal Concept Analysis: Mathematical Foundations. Springer, Berlin/Heidelberg, 1999.
Peter Gärdenfors. The Geometry of Meaning: Semantics Based on Conceptual Spaces. MIT Press, 2014.
Alexander Grothendieck. Revêtements étales et groupe fondamental (SGA 1), volume 224 of Lecture notes in mathematics. Springer-Verlag, 1971.
John R. Isbell. Small subcategories and completeness. Mathematical Systems Theory, 2(1):27-50, 1968.
Nicolas Jardine and Robin Sibson. Mathematical Taxonomy. John Wiley & Sons, Ltd, 1971.
Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.
Ian T. Jolliffe. Principal Component Analysis. Springer Series in Statistics. Springer, 2002.
Gregory Max Kelly. Basic Concepts of Enriched Category Theory. Number 64 in London Mathematical Society Lecture Notes. Cambridge University Press, 1982.
Joachim. Lambek. Completions of categories : seminar lectures given 1966 in Zurich. Number 24 in Springer Lecture Notes in Mathematics. Springer-Verlag, 1966.
Joachim Lambek and Philip Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1986.
Thomas K. Landauer, Danielle S. Mcnamara, Simon Dennis, and Walter Kintsch, editors. Handbook of Latent Semantic Analysis. Lawrence Erlbaum Associates, 2007.
F. William Lawvere. Metric spaces, generalised logic, and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43:135-166, 1973.
Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. Springer-Verlag, New York, 1992.
Saunders MacLane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.
Holbrook Mann MacNeille. Extensions of partially ordered sets. Proc. Nat. Acad. Sci. USA, 22(1):45-50, 1936.
Oded Maimon and Lior Rokach, editors. Data Mining and Knowledge Discovery Handbook, 2nd ed. Springer, 2010.
Dusko Pavlovic. Network as a computer: ranking paths to find flows. In Alexander Razborov and Anatol Slissenko, editors, Proceedings of CSR 2008, volume 5010 of Lecture Notes in Computer Science, pages 384-397. Springer Verlag, 2008. arxiv.org:0802.1306.
Dusko Pavlovic. On quantum statistics in data analysis. In Peter Bruza, editor, Quantum Interaction 2008. AAAI, 2008. arxiv.org:0802.1296.
Dusko Pavlovic. Quantifying and qualifying trust: Spectral decomposition of trust networks. In Pierpaolo Degano, Sandro Etalle, and Joshua Guttman, editors, Proceedings of FAST 2010, volume 6561 of Lecture Notes in Computer Science, pages 1-17. Springer Verlag, 2011. arxiv.org:1011.5696.
Dusko Pavlovic. Relating toy models of quantum computation: comprehension, complementarity and dagger autonomous categories. E. Notes in Theor. Comp. Sci., 270(2):121-139, 2011. arxiv.org:1006.1011.
Dusko Pavlovic. Quantitative Concept Analysis. In Florent Domenach, Dmitry I. Ignatov, and Jonas Poelmans, editors, Proceedings of ICFCA 2012, volume 7278 of Lecture Notes in Artificial Intelligence, pages 260-277. Springer Verlag, 2012. arXiv:1204.5802.
Dusko Pavlovic. Bicompletions of distance matrices. In Bob Coecke, Luke Ong, and Prakash Panangaden, editors, Computation, Logic, Games and Quantum Foundations. The Many Facets of Samson Abramsky, volume 7860 of Lecture Notes in Computer Science, pages 291-310. Springer Verlag, 2013.
Dusko Pavlovic and Samson Abramsky. Specifying interaction categories. In E. Moggi and G. Rosolini, editors, Category Theory and Computer Science 1997, volume 1290 of Lecture Notes in Computer Science, pages 147-158. Springer Verlag, 1997.
Duško Pavlović and Martín Escardó. Calculus in coinductive form. In V. Pratt, editor, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science, pages 408-417. IEEE Computer Society, 1998.
F. Ricci, L. Rokach, B. Shapira, and P.B. Kantor. Recommender Systems Handbook. Springer, 2010.
Ashok N. Srivastava and Mehran Sahami. Text Mining: Classification, Clustering, and Applications. Data Mining and Knowledge Discovery Series. CRC Press, 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Codensity Liftings of Monads
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.
Monads
Lifting
Fibration
Giry Monad
156-170
Regular Paper
Shin-ya
Katsumata
Shin-ya Katsumata
Tetsuya
Sato
Tetsuya Sato
10.4230/LIPIcs.CALCO.2015.156
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A First-order Logic for String Diagrams
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.
string diagrams
compact closed monoidal categories
abstract tensor systems
first-order logic
171-189
Regular Paper
Aleks
Kissinger
Aleks Kissinger
David
Quick
David Quick
10.4230/LIPIcs.CALCO.2015.171
John C. Baez and Jason Erbele. Categories in control. Technical report, arXiv:1405.6881, 2014.
F. Bonchi, P. Sobocinski, and F. Zanasi. A categorical semantics of signal flow graphs. In CONCUR'14: Concurrency Theory., volume 8704 of Lecture Notes in Computer Science, pages 435-450. Springer, 2014.
B. Coecke. Quantum picturalism. Contemporary Physics, 51:59-83, 2009. arXiv:0908.1787.
B. Coecke and R. Duncan. Interacting quantum observables. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, 2008.
B. Coecke, R. Duncan, A. Kissinger, and Q. Wang. Strong complementarity and non-locality in categorical quantum mechanics. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 2012. arXiv:1203.4988.
Lucas Dixon and Ross Duncan. Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation. AISC/MKM/Calculemus, pages 77-92, 2008.
Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer Berlin Heidelberg, 1999.
Andre Joyal and Ross Street. The geometry of tensor calculus I. Advances in Mathematics, 88:55-113, 1991.
D. Kartsaklis. Compositional Distributional Semantics with Compact Closed Categories and Frobenius Algebras. PhD thesis, University of Oxford, 2014.
Aleks Kissinger. Abstract tensor systems as monoidal categories. In C Casadio, B Coecke, M Moortgat, and P Scott, editors, Categories and Types in Logic, Language, and Physics: Festschrift on the occasion of Jim Lambek’s 90th birthday, volume 8222 of Lecture Notes in Computer Science. Springer, 2014. arXiv:1308.3586 [math.CT].
Aleks Kissinger, Alex Merry, and Matvey Soloviev. Pattern graph rewrite systems. In Proceedings of DCM 2012, volume 143 of EPTCS, 2012. arXiv:1204.6695 [math.CT].
Aleks Kissinger and David Quick. Tensors, !-graphs, and non-commutative quantum structures. In Proceedings of the 11th workshop on Quantum Physics and Logic, QPL 2014, Kyoto, Japan, 4-6th June 2014., pages 56-67, 2014. arXiv:1412.8552 [cs.LO].
Aleks Kissinger and David Quick. Tensors, !-graphs, and non-commutative quantum structures (extended version), 2015. arXiv:1503.01348.
Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning, 2015. arXiv:1503.01034.
Alexander Merry. Reasoning with !-Graphs. PhD thesis, University of Oxford, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Presenting Morphisms of Distributive Laws
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.
coalgebra
bialgebra
distributive law
structural operational semantics
190-204
Regular Paper
Bartek
Klin
Bartek Klin
Beata
Nachyla
Beata Nachyla
10.4230/LIPIcs.CALCO.2015.190
L. Aceto, W. J. Fokkink, and C. Verhoef. Structural operational semantics. In J. A. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 197-292. Elsevier, 2002.
F. Bartels. On Generalised Coinduction and Probabilistic Specification Formats. PhD dissertation, CWI, Amsterdam, 2004.
B. Bloom, S. Istrail, and A. Meyer. Bisimulation can't be traced. Journal of the ACM, 42:232-268, 1995.
M. Bonsangue, H. H. Hansen, A. Kurz, and J. Rot. Presenting distributive laws. In Procs. CALCO'13, volume 8089 of LNCS, pages 95-109, 2013.
M. Hennessy, W. Li, and G. D. Plotkin. A first attempt at translating CSP into CCS. In Proc. Second International Conference on Distributed Systems, pages 105-115, 1981.
B. Klin. Bialgebraic methods and modal logic in structural operational semantics. Information and Computation, 207:237-257, 2009.
B. Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. CMCS Tenth Anniversary Meeting.
B. Klin and B. Nachyła. Distributive laws and decidable properties of SOS specifications. In Procs. EXPRESS/SOS'14, volume 160 of ENTCS, pages 79-93, 2014.
M. Lenisa, J. Power, and H. Watanabe. Category theory for operational semantics. Theoretical Computer Science, 327(1-2):135-154, 2004.
G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004.
J. Power and H. Watanabe. Combining a monad and a comonad. Theor. Comput. Sci., 280:137-162, 2002.
J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3-80, 2000.
D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In Proc. LICS'97, pages 280-291. IEEE Computer Society Press, 1997.
H. Watanabe. Well-behaved translations between structural operational semantics. ENTCS, 65, 2002.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
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.
coalgebra
Bekic lemma
infinite data
functional programming
type theory
205-220
Regular Paper
Alexander
Kurz
Alexander Kurz
Alberto
Pardo
Alberto Pardo
Daniela
Petrisan
Daniela Petrisan
Paula
Severi
Paula Severi
Fer-Jan
de Vries
Fer-Jan de Vries
10.4230/LIPIcs.CALCO.2015.205
R. Atkey and C. McBride. Productive coprogramming with guarded recursion. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25-27, 2013, pages 197-208, 2013.
R. C. Backhouse, M. Bijsterveld, R. van Geldrop, and J. van der Woude. Categorical fixed point calculus. In Category Theory and Computer Science, 1995.
M. Barr. Terminal coalgebras for endofunctors on sets. Theoretical Computer Science, 114(2):299-315, 1999.
R. S. Bird and O. de Moor. Algebra of programming. Prentice Hall, 1997.
R. S. Bird. Introduction to Functional Programming using Haskell (second edition). Prentice Hall, 1998.
R. S. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Asp. Comput., 11(2), 1999.
S.L. Bloom, Z. Ésik, A. Labella, and E. G. Manes. Iteration 2-theories. Applied Categorical Structures, 9(2):173-216, 2001.
F. Borceux. Handbook of Categorical Algebra I. Cambridge University Press, 1994.
A. Cave, F. Ferreira, P. Panangaden, and B. Pientka. Fair reactive programming. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14, San Diego, CA, USA, January 20-21, 2014, pages 361-372, 2014.
R. A. Eisenberg and S. Weirich. Dependently typed programming with singletons. In Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Copenhagen, pages 117-130, 2012.
Z. Ésik and A. Labella. Equational properties of iteration in algebraically complete categories. Theoretical Computer Science, 195(1):61-89, 1998.
M. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994.
P. Freyd. Remarks on algebraically compact categories. In Applications of Categories in Computer Science, volume 77 of London Math. Soc. Lecture Notes Series, pages 95–-106. Cambridge University Press, 1992.
Haskell Chasing Bottoms Package: For testing partial and infinite values. http://hackage.haskell.org/package/ChasingBottoms. Online: accessed March 2015.
http://hackage.haskell.org/package/ChasingBottoms
G. Hutton and J. Gibbons. The generic approximation lemma. Inf. Process. Lett., 79(4):197-201, 2001.
C. B. Jones, editor. Programming Languages and Their Definition - Hans Bekic (1936-1982), LNCS 177. Springer, 1984.
G. M. Kelly and R. Street. Review of the elements of 2-categories. In Category Seminar (Proc. Sem. Sydney 1972/73), LNM 420, pages 75-103. Springer, 1974.
A. Kurz, D. Petrişan, A. Pardo, P. Severi, and F.-J. de Vries. Haskell code for this paper. http://www.cs.le.ac.uk/people/ps56/code.xml, 2015.
http://www.cs.le.ac.uk/people/ps56/code.xml
R. Lämmel and S. L. Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In TLDI'03, 2003.
D. J. Lehmann and M. B. Smyth. Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, 14:97-139, 1981.
C. E. Martin, J. Gibbons, and I. Bayley. Disciplined, efficient, generalised folds for nested datatypes. Formal Asp. Comput., 16(1):19-35, 2004.
A. Pitts. An elementary calculus of approximations. Unpublished note.
Haskell Regular: Generic programming library for regular datatypes. http://hackage.haskell.org/package/regular. Online accessed: March 2015.
http://hackage.haskell.org/package/regular
A. Rodriguez, S. Holdermans, A. Löh, and J. Jeuring. Generic programming with fixed points for mutually recursive datatypes. In ICFP, 2009.
T. van Noort, A. Rodriguez Yakushev, S. Holdermans, J. Jeuring, B. Heeren, and J.P. Magalhães. A lightweight approach to datatype-generic rewriting. J. Funct. Program., 20(3-4):375-413, 2010.
B. A. Yorgey, S. Weirich, J. Cretin, S. L. Peyton Jones, D. Vytiniotis, and J. P. Magalhães. Giving Haskell a promotion. In TLDI 2012, pages 53-66, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Final Coalgebras from Corecursive Algebras
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 .
coalgebra
modal logic
bisimulation
category theory
factorization system
221-237
Regular Paper
Paul Blain
Levy
Paul Blain Levy
10.4230/LIPIcs.CALCO.2015.221
Samson Abramsky. A cook’s tour of the finitary non-well-founded sets. In Sergei N. Artëmov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 1-18. College Publications, 2005.
Jiří Adámek, Mahdieh Haddadi, and Stefan Milius. Corecursive algebras, corecursive monads and bloom monads. Logical Methods in Computer Science, 10(3), 2014.
Jiří Adamek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories - The Joy of Cats. Wiley, 1990.
Jiř\'ıAdámek, Paul B. Levy, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. On final coalgebras of power-set functors and saturated trees. Applied Categorical Structures, June 2014.
Alexandru Baltag. A logic for coalgebraic simulation. Electronic Nptes in Theoretical Computer Science, 33, 2000.
Nick Bezhanishvili, Clemens Kupke, and Prakash Panangaden. Minimization via duality, volume 7456 LNCS of Lecture notes in computer science / Theoretical Computer Science and General Issues, pages 191-205. Springer, 2012.
Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2002.
Filippo Bonchi, Marcello M. Bonsangue, Helle H. Hansen, Prakash Panangaden, Jan J. M. M. Rutten, and Alexandra Silva. Algebra-coalgebra duality in Brzozowski’s minimization algorithm. ACM Transactions on Computational Logic, 15(1):3:1-3:29, March 2014.
Marcello Bonsangue and Alexander Kurz. Duality for logics of transition systems. In FOSSACS: International Conference on Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, 2005.
Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. INFCTRL: Information and Computation (formerly Information and Control), 204, 2006.
Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Corecursive algebras: A study of general structured corecursion. In M. Oliveira and J. Woodcock, editors, Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, Revised Selected Papers, volume 5902 of LNCS, pages 84-100. Springer, 2009.
Liang-Ting Chen and Achim Jung. On a categorical framework for coalgebraic modal logic. Electronic Notes in Theoretical Computer Science, 308:109-128, 2014.
Corina Cîrstea. A modular approach to defining and characterising notions of simulation. Information and Computation, 204(4):469-502, 2006.
Adam Eppendahl. Coalgebra-to-algebra morphisms. Electronic Notes in Theoretical Computer Science, 29:42-49, 1999.
Robert Goldblatt. Final coalgebras and the hennessy-milner property. Annals of Pure and Applied Logic, 138(1-3):77-93, 2006.
Wim H. Hesselink and Albert Thijs. Fixpoint semantics and simulation. Theoretical Computer Science, 238(1-2):275-311, 2000.
Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. Conjugate hylomorphisms - or: The mother of all structured recursion schemes. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 527-538. ACM, 2015.
Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theoretical Computer Science, 327(1-2):71-108, 2004.
Bart Jacobs and Ana Sokolova. Exemplaric expressivity of modal logics. Journal of Logic and Computation, 20(5):1041-1068, 2010.
Bartek Klin. Coalgebraic modal logic beyond sets. Electronic Notes in Theoretical Computer Science, 173:177-201, 2007.
Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 151-166. Springer, 2015.
Clemens Kupke and Raul Andres Leal. Characterising behavioural equivalence: Three sides of one coin. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 97-112. Springer, 2009.
Alexander Kurz and Dirk Pattinson. Coalgebraic modal logic of finite rank. Mathematical Structures in Computer Science, 15(3):453-473, 2005.
Paul B. Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Proceedings, 14th International Conference on Foundations of Software Science and Computational Structures, Saarbrücken, Germany, volume 6604 of Lecture Notes in Computer Science, pages 27-41. Springer, 2011.
Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.
Pierluigi Minari. Infinitary modal logic and generalized Kripke semantics. Annali del Dipartimento di Filosofia, 17(1), 2012.
Dusko Pavlovic, Michael W. Mislove, and James Worrell. Testing semantics: Connecting processes and process logics. In Michael Johnson and Varmo Vene, editors, Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006, Proceedings, volume 4019 of Lecture Notes in Computer Science, pages 308-322. Springer, 2006.
Slavian Radev. Infinitary propositional normal modal logic. Studia Logica, 46(4):291-309, 1987.
Jan J. M. M. Rutten. A calculus of transition systems (towards universal coalgebra). In 97, page 25. Centrum voor Wiskunde en Informatica (CWI), ISSN 0169-118X, January 31 1995. CS-R9503.
Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In S. Albers and J.-Y. Marion, editors, Proc. STACS 2009, volume 09001 of Dagstuhl Seminar Proceedings, pages 673-684. Schloss Dagstuhl, 2009.
Yoshihito Tanaka and Hiroakira Ono. Rasiowa-Sikorski lemma, Kripke completeness of predicate and infinitary modal logics. In Michael Zakharyaschev, Krister Segerberg, Maarten de Rijke, and Heinrich Wansing, editors, Advances in Modal Logic, pages 401-420. CSLI Publications, 1998.
Paul Taylor. Towards a unified treatment of induction i: the general recursion theorem. preprint, 1996.
Paul Taylor. Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1999.
Vera Trnková, Jiří Adámek, Václav Koubek, and Jan Reiterman. Free algebras, input processes and free monads. Commentationes Mathematicae Universitatis Carolinae, 016(2):339-351, 1975.
Toby Wilkinson. A characterisation of expressivity for coalgebraic bisimulation and simulation. Electronic Notes in Theoretical Computer Science, 286:323-336, 2012.
James Worrell. Coinduction for recursive data types: partial orders, metric spaces and ω-categories. Electronic Notes in Theoretical Computer Science, 33, 2000.
James Worrell. On the final sequence of a finitary set functor. Theoretical Computer Science, 338(1-3):184-199, June 2005.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Uniform Interpolation for Coalgebraic Fixpoint Logic
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.
mu-calculus
uniform interpolation
coalgebra
automata
238-252
Regular Paper
Johannes
Marti
Johannes Marti
Fatemeh
Seifan
Fatemeh Seifan
Yde
Venema
Yde Venema
10.4230/LIPIcs.CALCO.2015.238
Jiří Adámek and Věra Trnková. Automata and algebras in categories, volume 37 of Mathematics and its Applications (East European Series). Kluwer Academic Publishers Group, Dordrecht, 1990.
A. Arnold and D. Niwiński. Rudiments of μ-calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 2001.
J. Richard Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math., 6:66-92, 1960.
William Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic, 22:269-285, 1957.
Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: interpolation, Lyndon and Łoś-Tarski. J. Symbolic Logic, 65(1):310-332, 2000.
Calvin C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21-51, 1961.
Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Logic, 71(3):189-245, 1995.
Silvio Ghilardi and Marek Zawadowski. Undefinability of propositional quantifiers in the modal system S4. Studia Logica, 55(2):259-271, 1995.
Leon Henkin. An extension of the Craig-Lyndon interpolation theorem. J. Symbolic Logic, 28:201-216, 1963.
David Janin and Igor Walukiewicz. Automata for the modal μ-calculus and related results. In Mathematical foundations of computer science 1995 (Prague), volume 969 of Lecture Notes in Comput. Sci., pages 552-562. Springer, Berlin, 1995.
Christian Kissig and Yde Venema. Complementation of coalgebra automata. In Algebra and coalgebra in computer science, volume 5728 of Lecture Notes in Comput. Sci., pages 81-96. Springer, Berlin, 2009.
Clemens Kupke and Yde Venema. Coalgebraic automata theory: basic results. Log. Methods Comput. Sci., 4(4):4:10, 43, 2008.
Johannes Marti. Relation liftings in coalgebraic modal logic. Master’s thesis, Universiteit van Amsterdam, 2011.
Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. System Sci., 81(5):880-900, 2015.
Lawrence S. Moss. Coalgebraic logic. Ann. Pure Appl. Logic, 96(1-3):277-317, 1999. Festschrift on the occasion of Professor Rohit Parikh’s 60th birthday.
Dirk Pattinson. The logic of exact covers: Completeness and uniform interpolation. In Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on, pages 418-427. IEEE, 2013.
Andrew M. Pitts. On an interpretation of second-order quantification in first-order intuitionistic propositional logic. J. Symbolic Logic, 57(1):33-52, 1992.
Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1-35, 1969.
J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. Modern algebra and its applications (Nashville, TN, 1996).
Luigi Santocanale and Yde Venema. Uniform interpolation for monotone modal logic. In Advances in modal logic. Volume 8, pages 350-370. Coll. Publ., London, 2010.
Vladimir Yurievich Shavrukov. Adventures in diagonalizable algebras. ILLC Publications, 1994.
Yde Venema. Automata and fixed point logics for coalgebras. In Proceedings of the Workshop on Coalgebraic Methods in Computer Science, volume 106 of Electron. Notes Theor. Comput. Sci., pages 355-375 (electronic). Elsevier, Amsterdam, 2004.
Albert Visser. Uniform interpolation and layered bisimulation. In Gödel'96 (Brno, 1996), volume 6 of Lecture Notes Logic, pages 139-164. Springer, Berlin, 1996.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Generic Trace Semantics and Graded Monads
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.
transition systems
monads
coalgebra
trace logics
253-269
Regular Paper
Stefan
Milius
Stefan Milius
Dirk
Pattinson
Dirk Pattinson
Lutz
Schröder
Lutz Schröder
10.4230/LIPIcs.CALCO.2015.253
Luca Aceto, Anna Ingólfsdóttir, Kim Larsen, and Jiři Srba. Reactive systems: modelling, specification and verification. Cambridge Univ. Press, 2007.
Jiř\'ıAdámek, Jiř\'ıRosický, and Enrico Vitale. Algebraic Theories. Cambridge Univ. Press, 2011.
Marco Bernardo and Stefania Botta. A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math. Struct. Comput. Sci., 18:29-55, 2008.
Nick Bezhanishvili and Silvio Ghilardi. The bounded proof property via step algebras and step frames. Ann. Pure Appl. Logic, 165:1832-1863, 2014.
Marcello Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14, 2013.
Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Theories of Concurrency, CONCUR 1990, volume 458 of LNCS, pages 126-140. Springer, 1990.
Corina Cîrstea. A coalgebraic approach to linear-time logics. In Foundations of Software Science and Computation Structures, FoSSaCS 2014, volume 8412 of LNCS, pages 426-440. Springer, 2014.
Corina Cîrstea. Canonical coalgebraic linear time logics. In Proc. CALCO, 2015. This volume.
Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Logic, 71:189-245, 1995.
Valentin Goranko and Martin Otto. Model theory of modal logic. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, pages 249-329. Elsevier, 2006.
Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013.
Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Meth. Comput. Sci., 3, 2007.
Antony Hoare. Communicating sequential processes. Prentice Hall, 1985.
Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Coalgebraic Methods in Computer Science, CMCS 2012, volume 7399 of LNCS, pages 109-129. Springer, 2012.
Peter Johnstone. Adjoint lifting theorems for categories of algebras. Bull. London Math. Soc., 7:294-297, 1975.
Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Principles of Programming Languages, POPL 2014, pages 633-646. ACM, 2014.
Christian Kissig and Alexander Kurz. Generic trace logics. arXiv preprint 1103.3239, 2011.
Bartek Klin and Juriaan Rot. Coalgebraic trace semantics via forgetful logics. In Foundations of Software Science and Computation Structures, FoSSaCS'15, 2015.
Alexander Kurz, Stefan Milius, Dirk Pattinson, and Lutz Schröder. Simplified coalgebraic trace equivalence. In Software, Services, and Systems, volume 8950 of LNCS, pages 75-90. Springer, 2015.
A. Mazurkiewicz. Concurrent Program Schemes and Their Interpretation. Aarhus University, Comp. Sci. Depart., DAIMI PB-78, July 1977.
P.-A. Mellies. The parametric continuation monad. Preprint, 2015.
Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991.
Philip Mulry. Lifting theorems for Kleisli categories. In Mathematical Foundations of Programming Semantics, MFPS 1993, volume 802 of LNCS, pages 304-319. Springer, 1994.
D. Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic, 45:19-33, 2004.
J. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000.
L. Schröder and D. Pattinson. PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log., 10:13:1-13:33, 2009.
L. Schröder and D. Pattinson. Rank-1 modal logics are coalgebraic. J. Log. Comput., 20, 2010.
Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390:230-247, 2008.
Lutz Schröder and Dirk Pattinson. Coalgebraic correspondence theory. In Foundations of Software Structures and Computer Science, FoSSaCS 2010, volume 6014 of LNCS, pages 328-342. Springer, 2010.
Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, and Jan Rutten. Generalizing determinization from automata to coalgebras. Log. Meth. Comput. Sci, 9(1:9), 2013.
A. Smirnov. Graded monads and rings of polynomials. J. Math. Sci., 151:3032-3051, 2008.
Sam Staton. Relating coalgebraic notions of bisimulation. Log. Meth. Comput. Sci., 7, 2011.
Rob van Glabbeek. The linear time-branching time spectrum (extended abstract). In Theories of Concurrency, CONCUR'90, volume 458 of LNCS, pages 278-297. Springer, 1990.
James Worrell. On the final sequence of a finitary set functor. Theor. Comput. Sci., 338:184-199, 2005.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Open System Categorical Quantum Semantics in Natural Language Processing
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.
category theory
density matrices
distributional models
semantics
270-289
Regular Paper
Robin
Piedeleu
Robin Piedeleu
Dimitri
Kartsaklis
Dimitri Kartsaklis
Bob
Coecke
Bob Coecke
Mehrnoosh
Sadrzadeh
Mehrnoosh Sadrzadeh
10.4230/LIPIcs.CALCO.2015.270
Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. In 19th Annual IEEE Symposium on Logic in Computer Science, pages 415-425, 2004.
Esma Balkır. Using density matrices in a compositional distributional model of meaning. Master’s thesis, University of Oxford, 2014.
William Blacoe, Elham Kashefi, and Mirella Lapata. A quantum-theoretic approach to distributional semantics. In Proceedings of NACL 2013, pages 847-857. Association for Computational Linguistics, June 2013.
A. Carboni and R.F.C. Walters. Cartesian Bicategories I. Journal of Pure and Applied Algebra, 49, 1987.
B. Coecke and K. Martin. A partial order on classical and quantum states. In B. Coecke, editor, New Structures for Physics, Lecture Notes in Physics, pages 593-683. Springer, 2011.
B. Coecke, D. Pavlovic, and J. Vicary. A New Description of Orthogonal Bases. Mathematical Structures in Computer Science, 1, 2008.
B. Coecke, M. Sadrzadeh, and S. Clark. Mathematical Foundations for a Compositional Distributional Model of Meaning. Lambek Festschrift. Linguistic Analysis, 36:345-384, 2010.
Bob Coecke, Chris Heunen, and Aleks Kissinger. Categories of quantum and classical channels. arXiv preprint arXiv:1305.3821, 2013.
Bob Coecke and Robert W Spekkens. Picturing classical and quantum Bayesian inference. Synthese, 186(3):651-696, 2012.
E. Grefenstette and M. Sadrzadeh. Experimental support for a categorical compositional distributional model of meaning. In Proceedings of the EMNLP 2011, 2011.
Z. Harris. Mathematical Structures of Language. Wiley, 1968.
D. Kartsaklis, M. Sadrzadeh, S. Pulman, and B. Coecke. Reasoning about meaning in natural language with compact closed categories and Frobenius algebras. arXiv preprint arXiv:1401.5980, 2014.
Dimitri Kartsaklis and Mehrnoosh Sadrzadeh. Prior disambiguation of word tensors for constructing sentence vectors. In Proceedings of EMNLP 2013, pages 1590-1601, 2013.
G. M. Kelly and M. L. Laplaza. Coherence for compact closed categories. Journal of Pure and Applied Algebra, 19:193-213, 1980.
J. Lambek. From Word to Sentence. Polimetrica, Milan, 2008.
Joachim Lambek. The mathematics of sentence structure. American mathematical monthly, pages 154-170, 1958.
A. Preller and M. Sadrzadeh. Bell states and negative sentences in the distributed model of meaning. In P. Selinger B. Coecke, P. Panangaden, editor, Electronic Notes in Theoretical Computer Science, Proceedings of the 6th QPL Workshop on Quantum Physics and Logic. University of Oxford, 2010.
Anne Preller and Joachim Lambek. Free compact 2-categories. Mathematical Structures in Computer Science, 17(02):309-340, 2007.
M. Sadrzadeh, S. Clark, and B. Coecke. The Frobenius anatomy of word meanings I: subject and object relative pronouns. Journal of Logic and Computation, Advance Access, October 2013.
H. Schütze. Automatic Word Sense Discrimination. Computational Linguistics, 24:97-123, 1998.
Peter Selinger. Dagger compact closed categories and completely positive maps. Electronic Notes in Theoretical Computer Science, 170:139-163, 2007.
Peter Selinger. A survey of graphical languages for monoidal categories. In Bob Coecke, editor, New structures for physics, pages 289-355. Springer, 2011.
Peter D Turney and Patrick Pantel. From frequency to meaning: Vector space models of semantics. Journal of artificial intelligence research, 37(1):141-188, 2010.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Modules Over Monads and Their Algebras
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).
monad
module over monad
algebraic data types
resumptions
free object
290-303
Regular Paper
Maciej
Pirog
Maciej Pirog
Nicolas
Wu
Nicolas Wu
Jeremy
Gibbons
Jeremy Gibbons
10.4230/LIPIcs.CALCO.2015.290
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Revisiting the Institutional Approach to Herbrand’s Theorem
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.
Institution theory
Substitution systems
Herbrand’s theorem
304-319
Regular Paper
Ionut
Tutu
Ionut Tutu
José Luiz
Fiadeiro
José Luiz Fiadeiro
10.4230/LIPIcs.CALCO.2015.304
Jiri Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories: The Joy of Cats. Dover Publications, 2009. reprint.
Mihai Codescu. The model theory of higher order logic. Master’s thesis, Şcoala Normală Superioară Bucureşti, 2007.
Răzvan Diaconescu. Category-based constraint logic. Mathematical Structures in Computer Science, 10(3):373-407, 2000.
Răzvan Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticae, 55(3-4):321-348, 2003.
Răzvan Diaconescu. Herbrand theorems in arbitrary institutions. Information Processing Letters, 90(1):29-37, 2004.
Răzvan Diaconescu. Institution-Independent Model Theory. Birkhäuser, 2008.
Răzvan Diaconescu. Quasi-Boolean encodings and conditionals in algebraic specification. Journal of Logic and Algebraic Programming, 79(2):174-188, 2010.
Răzvan Diaconescu. Institutional semantics for many-valued logics. Fuzzy Sets and Systems, 218:32-52, 2013.
Daniel Găină. Forcing, Downward Löwenheim-Skolem and Omitting Types theorems, institutionally. Logica Universalis, 8(3-4):469-498, 2014.
Daniel Găină. Foundations of logic programming in hybridised logics. In Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science. Springer, \arip2015.
Joseph A. Goguen and Rod M. Burstall. Institutions: abstract model theory for specification and programming. Journal of the \acntextACM, 39(1):95-146, 1992.
Joseph A. Goguen, Grant Malcolm, and Tom Kemp. A hidden Herbrand theorem: combining the object and logic paradigms. Journal of Logic and Algebraic Programming, 51(1):1-41, 2002.
Joseph A. Goguen and José Meseguer. \acntextEQLOG: Equality, types, and generic modules for logic programming. In Logic Programming: Functions, Relations, and Equations, pages 295-363. Prentice Hall, 1986.
Joseph A. Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, and Ugo Montanari, editors, Theory and Practice of Software Development, volume 250 of Lecture Notes in Computer Science, pages 1-22. Springer, 1987.
Jacques Herbrand. Investigations in proof theory. In From Frege to Gödel: A Source Book in Mathematical Logic, pages 525-581. Harvard University Press, 1967.
John W. Lloyd. Foundations of Logic Programming. Springer, 1987.
Manuel A. Martins, Alexandre Madeira, Răzvan Diaconescu, and Luís Soares Barbosa. Hybridization of institutions. In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, Algebra and Coalgebra in Computer Science, volume 6859 of Lecture Notes in Computer Science, pages 283-297. Springer, 2011.
José Meseguer. General logics. In Heinz-Dieter Ebbinghaus, José Fernández-Prida, Manuel Garrido, Daniel Lascar, and Mario Rodriquez-Artalejo, editors, Logic Colloquium 1987, volume 129, pages 275-329. Elsevier, 1989.
José Meseguer. Multiparadigm logic programming. In Hélène Kirchner and Giorgio Levi, editors, Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 158-200. Springer, 1992.
Bernhard Möller, Andrzej Tarlecki, and Martin Wirsing. Algebraic specifications of reachable higher-order algebras. In Donald Sannella and Andrzej Tarlecki, editors, Abstract Data Types, volume 332 of Lecture Notes in Computer Science, pages 154-169. Springer, 1987.
Till Mossakowski, Ulf Krumnack, and Tom Maibaum. What is a derived signature morphism? In Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science. Springer, \arip2015.
Fernando Orejas, Elvira Pino, and Hartmut Ehrig. Institutions for logic programming. Theoretical Computer Science, 173(2):485-511, 1997.
Wieslaw Pawlowski. Context institutions. In Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors, Specification of Abstract Data Types, volume 1130 of Lecture Notes in Computer Science, pages 436-457. Springer, 1995.
Donald Sannella and Andrzej Tarlecki. Building specifications in an arbitrary institution. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 337-356. Springer, 1984.
Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Springer, 2011.
Traian Florin Şerbănuţă. Institutional concepts in first-order logic, parameterized specification, and logic programming. Master’s thesis, University of Bucharest, 2004.
Andrzej Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences, 33(3):333-360, 1986.
Ionuţ Ţuţu. Comorphisms of structured institutions. Information Processing Letters, 113(22-24):894-900, 2013.
Ionuţ Ţuţu and José L. Fiadeiro. From conventional to institution-independent logic programming. Journal of Logic and Computation, \arip2015.
Ionuţ Ţuţu and José L. Fiadeiro. Service-oriented logic programming. Logical Methods in Computer Science, \arip2015.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Coalgebraic Infinite Traces and Kleisli Simulations
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).
category theory
coalgebra
simulation
verification
trace semantics
320-335
Regular Paper
Natsuki
Urabe
Natsuki Urabe
Ichiro
Hasuo
Ichiro Hasuo
10.4230/LIPIcs.CALCO.2015.320
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Finitary Corecursion for the Infinitary Lambda Calculus
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.
rational trees
infinitary lambda calculus
coinduction
336-351
Regular Paper
Stefan
Milius
Stefan Milius
Thorsten
Wißmann
Thorsten Wißmann
10.4230/LIPIcs.CALCO.2015.336
Jiř\'ıAdámek. Introduction to coalgebra. Theory Appl. Categ., 14:157-199, 2005.
Jiř\'ıAdámek, Stefan Milius, and Jiri Velebil. Iterative algebras at work. Math. Structures Comput. Sci, 16(6):1085-1131, 2006.
Jiř\'ıAdámek, Stefan Milius, and Jiri Velebil. Semantics of higher-order recursion schemes. Log. Methods Comput. Sci., 7(1), 2011.
Jiř\'ıAdámek and Jiř\'ıRosický. Locally presentable and accessible categories. Cambridge University Press, 1994.
André Arnold and Maurice Nivat. The metric space of infinite trees. algebraic and topological properties. Fundam. Inform., 3(4):445-476, 1980.
Hendrik Pieter Barendregt. The Lambda calculus: Its syntax and semantics. North-Holland, Amsterdam, 1984.
Marcello M. Bonsangue, Stefan Milius, and Jurriaan Rot. On the specification of operations on the rational behaviour of systems. In Proc. EXPRESS/SOS'12, volume 89 of Electron. Proc. Theoret. Comput. Sci., pages 3-18, 2012.
Marcello M. Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14(1:7), 2013.
Bruno Courcelle. Fundamental properties of infinite trees. Theoret. Comput. Sci., 25:95-169, 1983.
Calvin C. Elgot. Monadic computation and iterative algebraic theories. In H. E. Rose and J. C. Sheperdson, editors, Logic Colloquium 1973, volume 80, pages 175-230, Amsterdam, 1975. North-Holland Publishers.
Marcelo Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proc. Logic in Computer Science 1999, pages 193-202. IEEE Press, 1999.
Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Proc. LICS'99, pages 214-224. IEEE Computer Society Press, 1999.
Peter Gabriel and Friedrich Ulmer. Lokal präsentierbare Kategorien, volume 221 of Lecture Notes Math. Springer-Verlag, 1971.
Fabio Gaducci, Marino Miculan, and Ugo Montanari. About permutation algebras, (pre)sheaved and names sets. Higher-Order Symb. Comput., 19:283-304, 2006.
Susanna Ginali. Regular trees and the free iterative theory. J. Comput. System Sci., 18:228-242, 1979.
Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:62-222, 1997.
Richard Kennaway, Jan Willem Klop, Ronan Sleep, and Fer-Jan de Vries. Infinitary Lambda Calculus. Theoret. Comput. Sci., 175(1):93-125, 1997.
Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Nominal coalgebraic data types with applications to lambda calculus. Log. Methods Comput. Sci., 9(4), 2013.
Joachim Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151-161, 1968.
Stefan Milius. A sound and complete calculus for finite stream circuits. In Proc. LICS'10, pages 449-458. IEEE Computer Society, 2010.
Stefan Milius, Marcello M. Bonsangue, Robert S.R. Myers, and Jurriaan Rot. Rational operation models. In Proc. MFPS XXIX, volume 298 of Electron. Notes Theor. Comput. Sci., pages 257-282, 2013.
Stefan Milius and Thorsten Wißmann. Finitary corecursion for the infinitary lambda calculus. full version; available at http://arxiv.org/abs/1505.07736, 2015.
http://arxiv.org/abs/1505.07736
Daniela Petrişan. Investigations into Algebra and Topology over Nominal Sets. dissertation, University of Leicester, 2011.
Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013.
Gordon D. Plotkin and Daniele Turi. Towards a mathematical operational semantics. In Proc. Logic in Computer Science (LICS'97), pages 280-291, 1997.
Jan Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000.
Jan Rutten. Rational streams coalgebraically. Log. Methods Comput. Sci., 4(3:9):22 pp., 2008.
Thorsten Wiß mann. The rational fixed point in nominal sets and its application to infinitary lambda-calculus. Project report, available at http://thorsten-wissmann.de/theses/project-wissmann.pdf, October 2014.
http://thorsten-wissmann.de/theses/project-wissmann.pdf
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode