Special Festschrift Issue in Honor of Jiří Adámek

Editors: Stefan Milius and Lawrence Moss

This Festschrift celebrates the 70th birthday of Jiří Adámek, the founding editor of Logical Methods in Computer Science and its executive editor until 2015. It contains a large variety of papers attributed to him and a PSSL 99 (aka. JirkaFest), featuring a diverse range of speakers, held in Braunschweig in March 2016. Both the Fest and Festschrift come with a great deal of love for Jiří and in acknowledgement of what he has taught us in the past, present, and future.

We would like to thank all the authors for their contribution to this Festschrift and also for their help in the reviewing and publication process. We are also thankful to the additional reviewers. In addition, our gratitude goes to the managing editors and the editor-in-chief, Lars Birkedal, for their support of this Festschrift. Last but not least, Katja Barkowski, Jürgen Koslowski, Frank Rust and Henning Urbat deserve our special thanks for organizing JirkaFest, the PSSL meeting in honor of.

Stefan Milius and Larry Moss
Festschrift Editors

For a full version of the preface containing more on Jiří, short statements of his students, and a group photo from JirkaFest press the following button.

1. Hopf and Lie algebras in semi-additive Varieties

We study Hopf monoids in entropic semi-additive varieties with an emphasis on adjunctions related to the enveloping monoid functor and the primitive element functor. These investigations are based on the concept of the abelian core of a semi-additive variety variety and its monoidal structure in case the variety is entropic.

2. Hanf numbers via accessible images

We present several new model-theoretic applications of the fact that, under the assumption that there exists a proper class of almost strongly compact cardinals, the powerful image of any accessible functor is accessible. In particular, we generalize to the context of accessible categories the recent Hanf number computations of Baldwin and Boney, namely that in an abstract elementary class (AEC) if the joint embedding and amalgamation properties hold for models of size up to a sufficiently large cardinal, then they hold for models of arbitrary size. Moreover, we prove that, under the above-mentioned large cardinal assumption, every metric AEC is strongly d-tame, strengthening a result of Boney and Zambrano and pointing the way to further generalizations.

3. Aspects of algebraic Algebras

In this paper we investigate important categories lying strictly between the Kleisli category and the Eilenberg-Moore category, for a Kock-Zöberlein monad on an order-enriched category. Firstly, we give a characterisation of free algebras in the spirit of domain theory. Secondly, we study the existence of weighted (co)limits, both on the abstract level and for specific categories of domain theory like the category of algebraic lattices. Finally, we apply these results to give a description of the idempotent split completion of the Kleisli category of the filter monad on the category of topological spaces.

4. A Note on the Topologicity of Quantale-Valued Topological Spaces

For a quantale ${\sf{V}}$, the category $\sf V$-${\bf Top}$ of ${\sf{V}}$-valued topological spaces may be introduced as a full subcategory of those ${\sf{V}}$-valued closure spaces whose closure operation preserves finite joins. In generalization of Barr's characterization of topological spaces as the lax algebras of a lax extension of the ultrafilter monad from maps to relations of sets, for ${\sf{V}}$ completely distributive, ${\sf{V}}$-topological spaces have recently been shown to be characterizable by a lax extension of the ultrafilter monad to ${\sf{V}}$-valued relations. As a consequence, ${\sf{V}}$-$\bf Top$ is seen to be a topological category over $\bf Set$, provided that ${\sf{V}}$ is completely distributive. In this paper we give a choice-free proof that ${\sf{V}}$-$\bf Top$ is a topological category over $\bf Set$ under the considerably milder provision that ${\sf{V}}$ be a spatial coframe. When ${\sf{V}}$ is a continuous lattice, that provision yields complete distributivity of ${\sf{V}}$ in the constructive sense, hence also in the ordinary sense whenever the Axiom of Choice is granted.

5. Some remarks on connectors and groupoids in Goursat categories

We prove that connectors are stable under quotients in any (regular) Goursat category. As a consequence, the category $\mathsf{Conn}(\mathbb{C})$ of connectors in $\mathbb{C}$ is a Goursat category whenever $\mathbb C$ is. This implies that Goursat categories can be characterised in terms of a simple property of internal groupoids.

6. Hyper Normalisation and Conditioning for Discrete Probability Distributions

Normalisation in probability theory turns a subdistribution into a proper distribution. It is a partial operation, since it is undefined for the zero subdistribution. This partiality makes it hard to reason equationally about normalisation. A novel description of normalisation is given as a mathematically well-behaved total function. The output of this `hyper' normalisation operation is a distribution of distributions. It improves reasoning about normalisation. After developing the basics of this theory of (hyper) normalisation, it is put to use in a similarly new description of conditioning, producing a distribution of conditional distributions. This is used to give a clean abstract reformulation of refinement in quantitative information flow.

7. On some categorical-algebraic conditions in S-protomodular categories

In the context of protomodular categories, several additional conditions have been considered in order to obtain a closer group-like behavior. Among them are locally algebraic cartesian closedness and algebraic coherence. The recent notion of S-protomodular category, whose main examples are the category of monoids and, more generally, categories of monoids with operations and Joónsson-Tarski varieties, raises a similar question: how to get a description of S-protomodular categories with a strong monoid-like behavior. In this paper we consider relative versions of the conditions mentioned above, in order to exhibit the parallelism with the "absolute" protomodular context and to obtain a hierarchy among S-protomodular categories.

8. Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective

Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehensively studied by Lynch and Vaandrager for nondeterministic and timed systems; for Büchi automata the notion of fair simulation has been introduced by Henzinger, Kupferman and Rajamani. We contribute to a generalization of fair simulation in two different directions: one for nondeterministic tree automata previously studied by Bomhard; and the other for probabilistic word automata with finite state spaces, both under the Büchi acceptance condition. The former nondeterministic definition is formulated in terms of systems of fixed-point equations, hence is readily translated to parity games and is then amenable to Jurdzi\'{n}ski's algorithm; the latter probabilistic definition bears a strong ranking-function flavor. These two different-looking definitions are derived from one source, namely our coalgebraic modeling of Büchi automata. Based on these coalgebraic observations, we also prove their soundness: a simulation indeed witnesses language inclusion.

9. Lax orthogonal factorisations in monad-quantale-enriched categories

We show that, for a quantale $V$ and a $\mathsf{Set}$-monad $\mathbb{T}$ laxly extended to $V$-$\mathsf{Rel}$, the presheaf monad on the category of $(\mathbb{T},V)$-categories is simple, giving rise to a lax orthogonal factorisation system (lofs) whose corresponding weak factorisation system has embeddings as left part. In addition, we present presheaf submonads and study the LOFSs they define. This provides a method of constructing weak factorisation systems on some well-known examples of topological categories over $\mathsf{Set}$.

10. An enriched view on the extended finitary monad--Lawvere theory correspondence

We give a new account of the correspondence, first established by Nishizawa--Power, between finitary monads and Lawvere theories over an arbitrary locally finitely presentable base. Our account explains this correspondence in terms of enriched category theory: the passage from a finitary monad to the corresponding Lawvere theory is exhibited as an instance of free completion of an enriched category under a class of absolute colimits. This extends work of the first author, who established the result in the special case of finitary monads and Lawvere theories over the category of sets; a novel aspect of the generalisation is its use of enrichment over a bicategory, rather than a monoidal category, in order to capture the monad--theory correspondence over all locally finitely presentable bases simultaneously.

11. A coalgebraic treatment of conditional transition systems with upgrades

We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branching type of the coalgebra and investigate the resulting behavioural equivalence. Furthermore we show how an existing algorithm for coalgebra minimisation can be instantiated to derive behavioural equivalences in this setting.

12. Model Theory and Proof Theory of Coalgebraic Predicate Logic

We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, both in comparison with coalgebraic hybrid logics and with existing first-order proposals for special classes of Set-coalgebras (apart from relational structures, also neighbourhood frames and topological spaces). Basic model-theoretic constructions and results, in particular ultraproducts, obtain for the two classes that allow completeness---and in some cases beyond that. Finally, we discuss a basic sequent system, for which we establish a syntactic cut-elimination result.

13. Computability in Basic Quantum Mechanics

The basic notions of quantum mechanics are formulated in terms of separable infinite dimensional Hilbert space $\mathcal{H}$. In terms of the Hilbert lattice $\mathcal{L}$ of closed linear subspaces of $\mathcal{H}$ the notions of state and observable can be formulated as kinds of measures as in [21]. The aim of this paper is to show that there is a good notion of computability for these data structures in the sense of Weihrauch's Type Two Effectivity (TTE) [26]. Instead of explicitly exhibiting admissible representations for the data types under consideration we show that they do live within the category $\mathbf{QCB}_0$ which is equivalent to the category $\mathbf{AdmRep}$ of admissible representations and continuously realizable maps between them. For this purpose in case of observables we have to replace measures by valuations which allows us to prove an effective version of von Neumann's Spectral Theorem.

14. A Ghost at $\omega_1$

In the final chain of the countable powerset functor, we show that the set at index $\omega_1$, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at each successor index is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of other subfunctors of the powerset functor. This leads to a precise description of which sets in these final chains are strongly extensional.

15. Natural Transformations as Rewrite Rules and Monad Composition

Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and only if $T$ is a terminal object in a certain category of strings and rewrite rules, and that this fact can be established by proving confluence of the rewrite system. We illustrate the technique on the monad composition problem. We also give a characterization of adjunctions in terms of rewrite categories.