Generalised Möbius Categories and Convolution Kleene Algebras
By: James Cranch, Georg Struth, Jana Wagemaker
Potential Business Impact:
Helps check computer programs for errors.
Convolution algebras on maps from structures such as monoids, groups or categories into semirings, rings or fields abound in mathematics and the sciences. Of special interest in computing are convolution algebras based on variants of Kleene algebras, which are additively idempotent semirings equipped with a Kleene star. Yet an obstacle to the construction of convolution Kleene algebras on a wide class of structures has so far been the definition of a suitable star. We show that a generalisation of M\"obius categories combined with a generalisation of a classical definition of a star for formal power series allow such a construction. We discuss several instances of this construction on generalised M\"obius categories: convolution Kleene algebras with tests, modal convolution Kleene algebras, concurrent convolution Kleene algebras and higher convolution Kleene algebras (e.g. on strict higher categories and higher relational monoids). These are relevant to the verification of weighted and probabilistic sequential and concurrent programs, using quantitative Hoare logics or predicate transformer algebras, as well as for algebraic reasoning in higher-dimensional rewriting. We also adapt the convolution Kleene algebra construction to Conway semirings, which is widely studied in the context of weighted automata. Finally, we compare the convolution Kleene algebra construction with a previous construction of convolution quantales and present concrete example structures in preparation for future applications.
Similar Papers
Kleene Algebrae, Kleene Modules, and Morita Equivalence
Logic in Computer Science
Unlocks new ways to understand computer programs.
Computational Exploration of Finite Semigroupoids
Formal Languages and Automata Theory
Makes computers understand how to do tasks better.
Between Markov and restriction: Two more monads on categories for relations
Logic in Computer Science
Organizes math ideas about how things connect.