-
Interacting Monoidal Structures with Applications in Computing
Authors:
James Cranch,
Georg Struth
Abstract:
With a view on applications in computing, in particular concurrency theory and higher-dimensional rewriting, we develop notions of $n$-fold monoid and comonoid objects in $n$-fold monoidal categories and bicategories. We present a series of examples for these structures from various domains, including a categorical model for a communication protocol and a lax $n$-fold relational monoid, which has…
▽ More
With a view on applications in computing, in particular concurrency theory and higher-dimensional rewriting, we develop notions of $n$-fold monoid and comonoid objects in $n$-fold monoidal categories and bicategories. We present a series of examples for these structures from various domains, including a categorical model for a communication protocol and a lax $n$-fold relational monoid, which has previously been used implicitly for higher-dimensional rewriting and which specialises in a natural way to strict $n$-categories. A special set of examples is built around modules and algebras of the boolean semiring, which allows us to deal with semilattices, additively idempotent semirings and quantales using tools from classical algebra.
△ Less
Submitted 6 November, 2024;
originally announced November 2024.
-
Presheaf automata
Authors:
Georg Struth,
Krzysztof Ziemiański
Abstract:
We introduce presheaf automata as a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and vector addition systems. We develop the foundations of a language theory for them based on notions of paths and track objects. We also define open maps for presheaf automata, extending the standard notions of simulation and bisimulatio…
▽ More
We introduce presheaf automata as a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and vector addition systems. We develop the foundations of a language theory for them based on notions of paths and track objects. We also define open maps for presheaf automata, extending the standard notions of simulation and bisimulation for transition systems. Apart from these conceptual contributions, we show that certain finite-type presheaf automata subsume all Petri nets, generalising a previous result by van Glabbeek, which applies to higher-dimensional automata and safe Petri nets.
△ Less
Submitted 6 September, 2024;
originally announced September 2024.
-
Single-set cubical categories and their formalisation with a proof assistant (extended version)
Authors:
Philippe Malbos,
Tanguy Massacrier,
Georg Struth
Abstract:
We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabe…
▽ More
We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation.
△ Less
Submitted 4 July, 2024; v1 submitted 19 January, 2024;
originally announced January 2024.
-
Kleene Theorem for Higher-Dimensional Automata
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as preshe…
▽ More
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.
△ Less
Submitted 8 December, 2024; v1 submitted 8 February, 2022;
originally announced February 2022.
-
lr-Multisemigroups and Modal Convolution Algebras
Authors:
Uli Fahrenberg,
Christian Johnsen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We show how modal quantales arise as convolution algebras of functions from lr-multisemigroups that is, multisemigroups with a source map l and a target map r, into modal quantales which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in the three algebras. The class of lr-multisemigroups introduced…
▽ More
We show how modal quantales arise as convolution algebras of functions from lr-multisemigroups that is, multisemigroups with a source map l and a target map r, into modal quantales which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in the three algebras. The class of lr-multisemigroups introduced in this article generalises Schweizer and Sklar's function systems and object-free categories to a setting isomorphic to algebras of ternary relations as used in boolean algebras with operators and in substructural logics. Our results provide a generic construction recipe for weighted modal quantales from such multisemigroups. This is illustrated by many examples, ranging from modal algebras of weighted relations as used in fuzzy mathematics, category quantales in the tradition of category algebras or group rings, incidence algebras over partial orders, discrete and continuous weighted path algebras, weighted languages of pomsets with interfaces, and weighted languages associated with presimplicial and precubical sets. We also discuss how these results can be combined with previous ones for concurrent quantales and generalised to a setting that supports reasoning with stochastic matrices or probabilistic predicate transformers.
△ Less
Submitted 1 May, 2021;
originally announced May 2021.
-
Algebraic coherent confluence and higher globular Kleene algebras
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos,
Georg Struth
Abstract:
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We ins…
▽ More
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.
△ Less
Submitted 24 November, 2022; v1 submitted 29 June, 2020;
originally announced June 2020.
-
Generating Posets Beyond N
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Ratan Bahadur Thapa
Abstract:
We introduce iposets---posets with interfaces---equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem mor…
▽ More
We introduce iposets---posets with interfaces---equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modelling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semirings and Kleene algebras that allow compositional reasoning about such systems.
△ Less
Submitted 14 October, 2019;
originally announced October 2019.
