No Arabic abstract
We introduce a general construction on 2-monads. We develop background on maps of 2-monads, their left semi-algebras, and colimits in 2-category. Then, we introduce the construction of a colimit induced by a map of 2-monads, show that we obtain the structure of a 2-monad and give a characterisation of its algebras. Finally, we apply the construction to the map of 2-monads between free symmetric monoidal and the free cartesian 2-monads and combine them into a linear-non-linear 2-monad.
We provide new categorical perspectives on Jacobs notion of hypernormalisation of sub-probability distributions. In particular, we show that a suitable general framework for notions of hypernormalisation is that of a symmetric monoidal category endowed with a linear exponential monad---a notion arising in the categorical semantics of Girards linear logic. We show that Jacobs original notion of hypernormalisation arises in this way from the finitely supported probability measure monad on the category of sets, which can be seen as a linear exponential monad with respect to a monoidal structure on sets arising from a quantum-algebraic object which we term the Giry tricocycloid. We give many other examples of hypernormalisation arising from other linear exponential monads.
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.
The Vietoris monad on the category of compact Hausdorff spaces is a topological analogue of the power-set monad on the category of sets. Exploiting Manes characterisation of the compact Hausdorff spaces as algebras for the ultrafilter monad on sets, we give precise form to the above analogy by exhibiting the Vietoris monad as induced by a weak distributive law, in the sense of Bohm, of the power-set monad over the ultrafilter monad.
We present an algorithm for approximating linear categories of partitions (of sets). We report on concrete computer experiments based on this algorithm which we used to obtain first examples of so-called non-easy linear categories of partitions. All of the examples that we constructed are proven to be indeed new and non-easy. We interpret some of the new categories in terms of quantum group anticommutative twists.
An adjunction is a pair of functors related by a pair of natural transformations, and relating a pair of categories. It displays how a structure, or a concept, projects from each category to the other, and back. Adjunctions are the common denominator of Galois connections, representation theories, spectra, and generalized quantifiers. We call an adjunction nuclear when its categories determine each other. We show that every adjunction can be resolved into a nuclear adjunction. The resolution is idempotent in a strict sense. The resulting nucleus displays the concept that was implicit in the original adjunction, just as the singular value decomposition of an adjoint pair of linear operators displays their canonical bases. [snip] In his seminal early work, Ross Street described an adjunction between monads and comonads in 2-categories. Lifting the nucleus construction, we show that the resulting Street monad on monads is strictly idempotent, and extracts the nucleus of a monad. A dual treatment achieves the same for comonads. This uncovers remarkably concrete applications behind a notable fragment of pure 2-category theory. The other way around, driven by the tasks and methods of machine learning and data analysis, the nucleus construction also seems to uncover remarkably pure and general mathematical content lurking behind the daily practices of network computation and data analysis.