The costructure–cosemantics adjunction for comodels for computational effects

It is well established that equational algebraic theories and the monads they generate can be used to encode computational effects. An important insight of Power and Shkaravska is that comodels of an algebraic theory $\mathbb{T}$ – i.e., models in the opposite category $\mathcal{S}\mathrm{et}^{\mathrm{op}}$ – provide a suitable environment for evaluating the computational effects encoded by $\mathbb{T}$ . As already noted by Power and Shkaravska, taking comodels yields a functor from accessible monads to accessible comonads on $\mathcal{S}\mathrm{et}$ . In this paper, we show that this functor is part of an adjunction – the “costructure–cosemantics adjunction” of the title – and undertake a thorough investigation of its properties. We show that, on the one hand, the cosemantics functor takes its image in what we term the presheaf comonads induced by small categories; and that, on the other, costructure takes its image in the presheaf monads induced by small categories. In particular, the cosemantics comonad of an accessible monad will be induced by an explicitly-described category called its behaviour category that encodes the static and dynamic properties of the comodels. Similarly, the costructure monad of an accessible comonad will be induced by a behaviour category encoding static and dynamic properties of the comonad coalgebras. We tie these results together by showing that the costructure–cosemantics adjunction is idempotent, with fixpoints to either side given precisely by the presheaf monads and comonads. Along the way, we illustrate the value of our results with numerous examples drawn from computation and mathematics.

On generalized algebraic theories and categories with families

We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.

Contextual modal types for algebraic effects and handlers

Programming languages with algebraic effects often track the computations’ effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a computation as a variable context; consequently, we propose to track algebraic effects of a computation with contextual modal types . We develop ECMTT, a novel calculus which tracks algebraic effects by a contextualized variant of the modal □ (necessity) operator, that it inherits from Contextual Modal Type Theory (CMTT). Whereas type-and-effect systems add effect annotations on top of a prior programming language, the effect annotations in ECMTT are inherent to the language, as they are managed by programming constructs corresponding to the logical introduction and elimination forms for the □ modality. Thus, the type-and-effect system of ECMTT is actually just a type system. Our design obtains the properties of local soundness and completeness, and determines the operational semantics solely by β-reduction, as customary in other logic-based calculi. In this view, effect handlers arise naturally as a witness that one context (i.e., algebraic theory) can be reached from another, generalizing explicit substitutions from CMTT. To the best of our knowledge, ECMTT is the first system to relate algebraic effects to modal types. We also see it as a step towards providing a correspondence in the style of Curry and Howard that may transfer a number of results from the fields of modal logic and modal type theory to that of algebraic effects.

On the Solvability and Number of Solutions of Production-Logical Equations in a Fuzzy LP-Structure

For the construction and study of formal models of intelligent information systems, algebraic methods are useful. One of the topical directions here is the production-type logical systems, which are widespread in computer science. In recent years, the author and his followers have been developing the algebraic theory of LP-structures (lattice production structures). It is designed to formalize and solve a number of knowledge management problems in production systems. The method of relevant backward inference (LP-inference) was also introduced and investigated, which significantly reduces the number of calls to external information sources in comparison with classical inference. Subsequently, the theory was generalized to speed up inference in distributed production systems. At the same time, modern intelligent systems are characterized by fuzzy knowledge and fuzzy reasoning. There­fore, there is a need to extend the theory of LP-structures to fuzzy production systems. This research was initiated in previous articles by the author. Some concepts are introduced that impart fuzziness to LP-structures, and certain properties of fuzzy LP-inference are established. In recent works, research results are presented that systematically generalize the theory of LP-structures to the case of fuzzy knowledge bases. The terminology of FLP-structures with fuzzy logical relation (Fuzzy LP-structures) is introduced, the main standard properties are proved. The present work complements the FLP-structure model by investigating a class of production-logical equations. Relevant inference ideas are based on it, reducing the number of calls to external sources of information. Methods for solving these equations are formulated. For the first time, questions about the existence and number of solutions have been resolved. Finding a solution to a production-logical equation corresponds to the backward fuzzy inference in a production system. The proved theorems can be used for software implementation of fuzzy LP-structures and corresponding optimization of fuzzy inference. Some ideas for this implementation are discussed.

Topological Methods of Analysis in Behavioral Analytics Systems

Purpose of the article: development of a methodology for the application of methods for analyzing big data based on topological constructions in relation to behavioral analytics systems to ensure corporate and cyber-physical security. Method: the technique is based on the algebraic theory of persistent homology. Along with algebraic topology, embedology (Takens-Mane embedding theory) and the theory of metric spaces are used. Result: the necessary concepts of algebraic topology are given, which underlie the analysis of user / entity behavior profiles: Vietoris-Rips simplicial complex, filtering by a set of cloud points, homology groups, persistence modules, topological characteristics and dependencies. At the first stage of the technique, the time series that describe the time-varying behavior of the user / entity are transformed into a cloud of points in the topological space. For this transformation, the methods of the Takens-Mane embedding theory and the algorithm of the method of false neighbors are used. At the subsequent stages of the methodology for the base and current point clouds, topological dependencies, diagrams (persistence, bar codes) characterizing the base and current behavior profiles, respectively, are built. At the final stage, the deviation of the current behavior profile from the baseline is revealed. To estimate the deviation, the Wasserstein, Chebyshev, bottleneck metrics and scaling based on the generalized Harrington desirability function are used. The results of practical testing of the proposed method of applying topological algorithms to the data of the monitoring system for the work of corporate network users with information resources are presented

Combining Semilattices and Semimodules

We describe the canonical weak distributive law $$\delta :\mathcal S\mathcal P\rightarrow \mathcal P\mathcal S$$ δ : S P → P S of the powerset monad $$\mathcal P$$ P over the S-left-semimodule monad $$\mathcal S$$ S , for a class of semirings S. We show that the composition of $$\mathcal P$$ P with $$\mathcal S$$ S by means of such $$\delta $$ δ yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs’s monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of $$\mathcal P$$ P to $$\mathbb {EM}(\mathcal S)$$ EM ( S ) as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad $$\mathcal P_f$$ P f .