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öbius 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öbius 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.
翻译:从幺半群、群或范畴等结构到半环、环或域的映射上的卷积代数在数学与科学领域中广泛存在。在计算领域特别受关注的是基于克林代数变体的卷积代数,即配备克林星的加法幂等半环。然而,迄今为止,在广泛的结构类上构建卷积克林代数的一个障碍在于如何定义合适的星运算。我们证明,广义莫比乌斯范畴与形式幂级数星运算的经典定义的推广相结合,使得此类构造成为可能。我们讨论了该构造在广义莫比乌斯范畴上的若干实例:带测试的卷积克林代数、模态卷积克林代数、并发卷积克林代数以及高阶卷积克林代数(例如在严格高阶范畴与高阶关系幺半群上)。这些代数对于使用定量霍尔逻辑或谓词转换子代数进行加权及概率性顺序与并发程序的验证,以及在高维重写中的代数推理具有重要意义。我们还将卷积克林代数构造适配于康威半环,该结构在加权自动机背景下已被广泛研究。最后,我们将卷积克林代数构造与先前的卷积量格构造进行比较,并展示具体的示例结构,为未来的应用做准备。