No Arabic abstract
There are different notions of computation, the most popular being monads, applicative functors, and arrows. In this article we show that these three notions can be seen as monoids in a monoidal category. We demonstrate that at this level of abstraction one can obtain useful results which can be instantiated to the different notions of computation. In particular, we show how free constructions and Cayley representations for monoids translate into useful constructions for monads, applicative functors, and arrows. Moreover, the uniform presentation of all three notions helps in the analysis of the relation between them.
We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete.
We give a leisurely introduction to our abstract framework for operational semantics based on cellular monads on transition categories. Furthermore, we relate it for the first time to an existing format, by showing that all Positive GSOS specifications generate cellular monads whose free algebras are all compositional. As a consequence, we recover the known result that bisimilarity is a congruence in the generated labelled transition system.
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.
Game semantics has provided adequate models for a variety of programming languages, in which types are interpreted as two-player games and programs as strategies. Melli`es (2018) suggested that such categories of games and strategies may be obtained as instances of a simple abstract construction on weak double categories. However, in the particular case of simple games, his construction slightly differs from the standard category. We refine the abstract construction using factorisation systems, and show that the new construction yields the standard category of simple games and strategies. Another perhaps surprising instance is Days convolution monoidal structure on the category of presheaves over a strict monoidal category.
Five algebraic notions of termination are formalised, analysed and compared: wellfoundedness or Noetherity, Lobs formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additively idempotent semirings with forward and backward modal operators. To model infinite behaviours, idempotent semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite dynamics of programs and transition systems.