Search

Triangulated surfaces provide a three-dimensional generalization of polygons in two dimensions. Surfaces are usually stored on computers in the form of triangulated surfaces, and these are the kinds of objects that must be handled in practical applications.

Models of iterated computation, such as completely iterative monads, often depend on a notion of guardedness, which guarantees unique solvability of recursive equations and requires roughly that recursive calls happen only under certain guarding operations. On the other hand, many models of iteration do admit unguarded iteration. Solutions are then no longer unique, and in general not even determined as least or greatest fixpoints, being instead governed by quasi-equational axioms. Monads that support unguarded iteration in this sense are called complete Elgot monads. Here, we propose to equip monads with an abstract notion of guardedness and then require solvability of abstractly guarded recursive equations; examples of such abstractly guarded pre-iterative monads include both iterative monads and Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting unique solutions of abstractly guarded recursive equations; in other words, models of unguarded iteration come about by quotienting models of guarded iteration.

The framework of Categorical Compositional Distributional models of meaning [3], inspired by category theory, allows one to compute the meaning of natural language phrases, given basic meaning entities assigned to words. Composing word meanings is the result of a functorial passage from syntax to semantics. To keep one from drowning in technical details, diagrammatic reasoning is used to represent the information flow of sentences that exists independently of the concrete instantiation of the model. Not only does this serve the purpose of clarification, it moreover offers computational benefits as complex diagrams can be transformed into simpler ones, which under coherence can simplify computation on the semantic side. Until now, diagrams for compact closed categories and monoidal closed categories have been used (see [2, 3]). These correspond to the use of pregroup grammar [12] and the Lambek calculus [9] for syntactic structure, respectively. Unfortunately, the diagrammatic language of Baez and Stay [1] has not been proven coherent. In this paper, we develop a graphical language for the (categorical formulation of) the nonassociative Lambek calculus [10]. This has the benefit of modularity where extension of the system are easily incorporated in the graphical language. Moreover, we show the language is coherent with monoidal closed categories without associativity, in the style of Selinger’s survey paper [17].

We give a general description of the transition from qualitative models of programming languages to quantitative ones, as a change of base for enriched categories. This is induced by a monoidal functor from the category of coherence spaces to the category of modules over a complete semiring $${\mathcal {R}}$$. Using the properties of this functor, we characterise the requirements for the change of base to preserve the structure of a Lafont category model of linear type theory with free exponential, and thus to give an adequate semantics of erratic PCF with scalar weights from $${\mathcal {R}}$$. Moreover, this model comes with a meaning-preserving functor from the original, qualitative one, which we may use to interpret side-effects such as state. As an example, we show that the game semantics of Idealized Algol bears a natural enrichment over the category of coherence spaces, and thus gives rise by change of base to a $${\mathcal {R}}$$-weighted model, which is fully abstract. We relate this to existing categories of probabilistic games and slot games.

Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman’s theorem states that they precisely specify pseudovarieties, i.e. classes of finite algebras closed under finite products, subalgebras and quotients. In this paper Reiterman’s theorem is generalised to finite Eilenberg-Moore algebras for a monad \(\mathbf {T}\) on a variety \(\mathscr {D}\) of (ordered) algebras: a class of finite \(\mathbf {T}\)-algebras is a pseudovariety iff it is presentable by profinite (in-)equations. As an application, quasivarieties of finite algebras are shown to be presentable by profinite implications. Other examples include finite ordered algebras, finite categories, finite \(\infty \)-monoids, etc.

We prove that a trace monoid embeds into the queue monoid if and only if it embeds into the direct product of two free monoids. We also give a decidable characterization of these trace monoids.

Some dependency treebanks use special sequences of dependencies where main arguments are mixed with separators. Classical Categorial Dependency Grammars (CDG) do not allow this construction because iterative dependency types only introduce the iterations of the same dependency. An extension of CDG is defined here that introduces a new construction for repeatable sequences of one or several dependency names. The learnability properties of the extended CDG when grammars are infered from a dependency treebank is also studied. It leads to the definition of new classes of grammars that are learnable in the limit from dependency structures.

We initiate a formal theory of graded monads whose purpose is to adapt and to extend the formal theory of monads developed by Street in the early 1970’s. We establish in particular that every graded monad can be factored in two different ways as a strict action transported along a left adjoint functor. We also explain in what sense the first construction generalizes the Eilenberg-Moore construction while the second construction generalizes the Kleisli construction. Finally, we illustrate the Eilenberg-Moore construction on the graded state monad induced by any object V in a symmetric monoidal closed category \(\mathscr {C}\).

The Schutzenberger product of monoids is a key tool for the algebraic treatment of language concatenation. In this paper we generalize the Schutzenberger product to the level of monoids in an algebraic category $$\mathscr {D}$$, leading to a uniform view of the corresponding constructions for monoids Schutzenberger, ordered monoids Pin, idempotent semirings Klima and Polak, and algebras over a field Reutenauer. In addition, assuming that $$\mathscr {D}$$ is part of a Stone-type duality, we derive a characterization of the languages recognized by Schutzenberger products.

This paper contributes to a theory of the behaviour of “finite-state” systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adamek, Milius and Velebil). Moreover, we show that the LFF is characterized by two universal properties: 1. as the final locally finitely generated coalgebra, and 2. as the initial fg-iterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal power-series, regular trees etc. And we obtain a number of new examples, e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (and any other instance of the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten) and the monad of Courcelle’s algebraic trees.

Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modelling reversible functional programming, notably morphism schemes for reversible recursion, a \(\dagger \)-trace, and algebraic \(\omega \)-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

In this paper, we study several sublogics of monadic second-order logic over countable linear orderings, such as first-order logic, first-order logic on cuts, weak monadic second-order logic, weak monadic second-order logic with cuts, as well as fragments of monadic second-order logic in which sets have to be well ordered or scattered. We give decidable algebraic characterizations of all these logics and compare their respective expressive power.

We express the classical p-adic integers \(\hat{\mathbb {Z}}_p\), as a metric space, as the final coalgebra to a certain endofunctor. We realize the addition and the multiplication on \(\hat{\mathbb {Z}}_p\) as the coalgebra maps from \(\hat{\mathbb {Z}}_p\times \hat{\mathbb {Z}}_p\).

Several fixed point models share the equational properties of iteration theories, or iteration categories, which are cartesian categories equipped with a fixed point or dagger operation subject to certain axioms. After discussing some of the basic models, we provide equational bases for iteration categories and offer an analysis of the axioms. Although iteration categories have no finite base for their identities, there exist finitely based implicational theories that capture their equational theory. We exhibit several such systems. Then we enrich iteration categories with an additive structure and exhibit interesting cases where the interaction between the iteration category structure and the additive structure can be captured by a finite number of identities. This includes the iteration category of monotonic or continuous functions over complete lattices equipped with the least fixed point operation and the binary supremum operation as addition, the categories of simulation, bisimulation, or language equivalence classes of processes, context-free languages, and others. Finally, we exhibit a finite equational system involving residuals, which is sound and complete for monotonic or continuous functions over complete lattices in the sense that it proves all of their identities involving the operations and constants of cartesian categories, the least fixed point operation and binary supremum, but not involving residuals.

In this chapter, we introduce adhesive and \(\mathcal{M}\)-adhesive categories as the categorical foundation of graph and model transformations and present various constructions and properties. In Sect. 4.1, we introduce \(\mathcal{M}\)-adhesive categories based on the notion of van Kampen squares. Different versions of adhesive categories are compared to the one we use in this book in Sect. 4.2. In Sect. 4.3, we introduce some additional properties which are needed for results in \(\mathcal{M}\)-adhesive categories, as well as derive results that hold in any such category.

State spaces in probabilistic and quantum computation are convex sets, that is, Eilenberg–Moore algebras of the distribution monad. This article studies some computationally relevant properties of convex sets. We introduce the term effectus for a category with suitable coproducts (so that predicates, as arrows of the shape X → 1 + 1, form effect modules, and states, arrows of the shape 1 → X, form convex sets). One main result is that the category of cancellative convex sets is such an effectus. A second result says that the state functor is a “map of effecti”. We also define ‘normalisation of states’ and show how this property is closed related to conditional probability. This is elaborated in an example of probabilistic Bayesian inference.

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.

Homotopy Type Theory is a new, homotopical interpretation of constructive type theory. It forms the basis of the recently proposed Univalent Foundations of Mathematics program. Combined with a computational proof assistant, and including a new foundational axiom – the Univalence Axiom – this program has the potential to shift the theoretical foundations of mathematics and computer science, and to affect the practice of working scientists. This talk will survey the field and report on some of the recent developments.

In this paper we prove that the Lambek calculus allowing empty antecedents and enriched with a unary connective corresponding to language reversal is complete with respect to the class of models on subsets of free monoids (L-models).

The purpose of this paper is to discuss the universal algebra theory of hom-algebras. This kind of algebra involves a linear map which twists the usual identities. We focus on hom-associative algebras and hom-Lie algebras for which we review the main results. We discuss the envelopment problem, operads, and the Diamond Lemma; the usual tools have to be adapted to this new situation. Moreover we study Hilbert series for the hom-associative operad and free algebra, and describe them up to total degree equal 8 and 9 respectively.

The Baues–Wirsching cohomology is one of the cohomologies of a small category. Our aim is to describe the first Baues–Wirsching cohomology of the small category generated by a finite quiver freely. We consider the case where the coefficient is a natural system obtained by the composition of a functor and the target functor. We give an algorithm to obtain generators of the vector space of inner derivations. It is known that there exists a surjection from the vector space of derivations of the small category to the first Baues–Wirsching cohomology whose kernel is the vector space of inner derivations.

We prove that every symmetric residuated groupoid is embeddable in a boolean double residuated groupoid. Analogous results are obtained for other classes of algebras, e.g. (commutative) symmetric residuated semigroups, symmetric residuated unital groupoids, cyclic bilinear algebras. We also show that powerset algebras constructed in the paper preserve some Grishin axioms.

On any set X may be defined the free algebra R〈X〉 (respectively, free commutative algebra R[X]) with coefficients in a ring R. It may also be equivalently described as the algebra of the free monoid X * (respectively, free commutative monoid . Furthermore, the algebra of differential polynomials R{X} with variables in X may be constructed. The main objective of this contribution is to provide a functorial description of this kind of objects with their relations (including abelianization and unitarization) in the category of differential algebras, and also to introduce new structures such as the differential algebra of a semigroup, of a monoid, or the universal differential envelope of an algebra.

The purpose of this article is to show that the associative Lambek calculus extended with basic proper axioms can be simulated by the usual associative Lambek calculus, with the same number of types per word in a grammar. An analogue result had been shown for pregroups grammars [1]. We consider Lambek calculus with product, as well as the product-free version.

From a differential geometric approach parallel transport on path spaces has been addressed. Integral version establishes the category theoretic frame work. We have glossed over the topic of representations of categorical groups and its relation with categorical framework of path space parallel transport.

This is a survey on spherical Hopf algebras. We give criteria to decide when a Hopf algebra is spherical and collect examples. We discuss tilting modules as a mean to obtain a fusion subcategory of the non-degenerate quotient of the category of representations of a suitable Hopf algebra.

Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a monoidal comonad. Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language $\ell \mathcal{R}$ PCF inspired by a generalized interpretation of the exponential modality. In $\ell \mathcal{R}$ PCF the exponential modality carries a label--an element of a semiring $\mathcal{R}$ --that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.

In 2013 Sorokin proved that the criterion of type conjoinability in 1-discontinuous Lambek calculus is the equality of interpretations in the free abelian group generated by primitive types. We extend the method to obtain the analogous result in full discontinuous Lambek calculus. It holds that the criterion is exactly the same as in 1-discontinuous Lambek calculus.

In the first part of the paper we recall the coalgebraic approach to handling the so-called invisible transitions that appear in different state-based systems semantics. We claim that these transitions are always part of the unit of a certain monad. Hence, coalgebras with internal moves are exactly coalgebras over a monadic type. The rest of the paper is devoted to supporting our claim by studying two important behavioural equivalences for state-based systems with internal moves, namely: weak bisimulation and trace semantics. We continue our research on weak bisimulations for coalgebras over order enriched monads. The key notions used in this paper and proposed by us in our previous work are the notions of an order saturation monad and a saturator. A saturator operator can be intuitively understood as a reflexive, transitive closure operator. There are two approaches towards defining saturators for coalgebras with internal moves. Here, we give necessary conditions for them to yield the same notion of weak bisimulation. Finally, we propose a definition of trace semantics for coalgebras with silent moves via a uniform fixed point operator. We compare strong and weak bisimilation together with trace semantics for coalgebras with internal steps.

The set of natural integers is fundamental for at least two reasons: it is the free induction algebra over the empty set (and at such allows definitions of maps by primitive recursion) and it is the free monoid over a one-element set, the latter structure being a consequence of the former. In this contribution, we study the corresponding structure in the linear setting, i.e. in the category of modules over a commutative ring rather than in the category of sets, namely the free module generated by the integers. It also provides free structures of induction algebra and of monoid (in the category of modules). Moreover we prove that each of its linear endomorphisms admits a unique normal form, explicitly constructed, as a non-commutative formal power series.

We are interested in monoids and its applications. If every element x in a monoid has a quasi-inverse y in the sense of von Neumann, that satisfies x ·y ·x = x and y ·x ·y = y, the monoid is regular. Our purpose is to use regular monoids to build two abstract algebraic public key cryptosystems: key exchange protocol and public key encryption with keyword search scheme. In addition to illustrating how the two cryptosystems work, we provide instances of these abstract algebraic models and analyse them in terms of cryptanalysis security.

In this paper we construct a new trace model of delay-insensitive asynchronous circuits inspired by Ebergen’s model in such a way that it satisfies the compositional properties of a category, with additional monoidal structure and further algebraic properties. These properties taken together lay a solid mathematical foundation for a diagrammatic approach to reasoning about asynchronous circuits, which represents a formalisation of common intuitions about asynchronous circuits and their properties.

A new text categorization algorithm based on Hidden Markov Model is proposed. At first, semantic clusters are obtained from training data set. The association between semantic clusters is modeled as Hidden Markov Model. Combining with the forward algorithm, the strategy could realize automatic text categorization. From the simulation, the proposed text categorization algorithm is better in categorization precision. Moreover, it works well independent of the number of considered categories compared to the priori art algorithms.

The main idea in the topos formulation of quantum theory it to have logic as a fundamental concept and try and derive other concepts in terms of it. This is what is done in the case of probabilities.

When analysing the origin of the twisted presheaves, it is clear that the reason we do get a twist is because the group moves the abelian algebras around, i.e. the group action is defined on the base category itself. Thus a possible way of avoiding the occurrence of twists is by imposing that the group does not act on the base category. The category of abelian von-Neumann sub-algebras with no group acting on it will be denoted \(\mathcal{V}_{f}(\mathcal{H})\), where we have added the subscript f (for fixed) to distinguish this situation from the case in which the group does act. Obviously, if one just defined sheaves over \(\mathcal{V}_{f}(\mathcal{H})\), then there would be no group action at all, therefore something extra is needed. As we will see this ‘extra’ will be the introduction of an intermediate category which will be used as an intermediate base category. On such an intermediate category the group is allowed to act, thus the sheaves defined over it will admit a group action. Once this is done, everything is “pushed down” to the fixed category \(\mathcal{V}_{f}(\mathcal{H})\). As we will see, the sheaves defined in this way will admit a group action which now takes place at an intermediate stage, but will not produce any twists since the final base category stays fixed.

The notion of relation lifting can be generalised to work with many-valued relations while retaining many vital properties of the “classical” relation lifting. We show that polynomial endofunctors of the category of sets and mappings admit \(\mathcal{V}\)-relation lifting for relations taking values from a commutative quantale \(\mathcal{V}\). Using the technique of functor presentations, we then show that every finitary weak pullback preserving functor admits a \(\mathcal{V}\)-relation lifting for \(\mathcal{V}\) being a complete Heyting algebra. As an application of the many-valued lifting we inspect the notion of many-valued bisimulation and we introduce an expressive many-valued variant of Moss’ logic for T-coalgebras, parametric in the functor T.

This paper describes a generalization of the usual category in which coalgebras are considered, and its application to modelling quantum systems and their physical symmetries. Following the programme of work initiated in [1], [2], we aim to model systems described by the laws of quantum physics using coalgebraic techniques. A broader notion of the morphisms of coalgebras is given, in which diagrams are allowed to commute only up to appropriate natural isomorphism. This relaxed setting is then shown to have analogues of coalgebraic notions such as bisimulations, with properties that parallel the usual coalgebraic ones closely. This new setting is then exploited to give coalgebraic models of quantum systems in which the conceptually important physical symmetries are given as automorphisms of a suitable coalgebra.

We seek universal categorical conditions ensuring the representability of all partial recursive functions. In the category Pfn of sets and partial functions, the natural numbers provide both an initial algebra and a final coalgebra for the functor 1 + −. We recount how finality yields closure of the partial functions on natural numbers under Kleene’s μ-recursion scheme. Noting that Pfn is not cartesian, we then build on work of Paré and Román, obtaining weak initiality and finality conditions on natural numbers algebras in monoidal categories that ensure the (weak) representability of all partial recursive functions. We further obtain some positive results on strong representability. All these results adapt to Kleisli categories of cartesian categories with natural numbers algebras. However, in general, not all partial recursive functions need be strongly representable.

The concept of a morphism determined by an object provides a method to construct or classify morphisms in a fixed category. We show that this works particularly well for triangulated categories having Serre duality. Another application of this concept arises from a reformulation of Freyd’s generating hypothesis.

Given that the justified belief in support of exactness of the primary category of logical reality is accepted, we still have a problem of establishing the exactness of logical transformations among epistemic categories as well as to establish the conversion chain of derived categories by the method of constructionism. Let us keep in mind that the acceptance of exactness of the primary category means that the defective information structure over the epistemic space is due to incompleteness and free from defectiveness due to vagueness and ambiguities. In this way the possibility space is assumed to be exact and so also the incomplete information in the probability space. The first step is to present an exact representation of the elements in the primary category that is empirically or axiomatically defined on which the laws of thought will be applied. The representation involves a language presentation of ideas and meanings through words or symbols for analysis and synthesis to arrive at the derived logical categories. Examples of the primary and the derived categories in mathematics are that the advanced mathematical levels are derivative from the basic number system which is a derivative from our linguistic number system.

Kolmogorov complexity theory is used to tell what the algorithmic informational content of a string is. It is defined as the length of the shortest program that describes the string. We present a programming language that can be used to describe categories, functors, and natural transformations. With this in hand, we define the informational content of these categorical structures as the shortest program that describes such structures. Some basic consequences of our definition are presented including the fact that equivalent categories have equal Kolmogorov complexity. We also prove different theorems about what can and cannot be described by our programming language.

For an arbitrary category \(\mathcal{C}\), the category \(Sets^{\mathcal{C}^{op}}\) of presheaves is actually a topos. This topos is important since, for a particular choice of \(\mathcal{C}\), it will be the topos we will utilise to express quantum theory.

This paper offers a short discussion of the property of local finiteness for t-norm monoids and bimonoids. Such bimonoids are of interest in the context of weighted automata. The paper shows that, perhaps unexpectedly, the situation is more complex in the bimonoidal case than it is for monoids: there there are more possibilities for local finiteness.

A new characterization of nondeterministic concurrent strategies exhibits strategies as certain discrete fibrations--or equivalently presheaves--over configurations of the game. This leads to a lax functor from the bicategory of strategies to the bicategory of profunctors. The lax functor expresses how composition of strategies is obtained from that of profunctors by restricting to 'reachable' elements, which gives an alternative formulation of the composition of strategies. It provides a fundamental connection--and helps explain the mismatches--between two generalizations of domain theory to forms of intensional domain theories, one based on games and strategies, and the other on presheaf categories and profunctors. In particular cases, on the sub-bicategory of rigid strategies which includes 'simple games' (underlying AJM and HO games), and stable spans (specializing to Berry's stable functions, in the deterministic case), the lax functor becomes a pseudo functor. More generally, the laxness of the functor suggests what structure is missing from categories and profunctors in order that they can be made to support the operations of games and strategies. By equipping categories with the structure of a 'rooted' factorization system and ensuring all elements of profunctors are 'reachable,' we obtain a pseudo functor embedding the bicategory of strategies in the bicategory of reachable profunctors. This shift illuminates early work on bistructures and bidomains, where the Scott order and Berry's stable order are part of a factorization system, giving a sense in which bidomains are games.

This paper presents a first step towards completeness-via-canonicity results for coalgebraic modal logics. Specifically, we consider the relationship between classes of coalgebras for ω-accessible endofunctors and logics defined by Sahlqvist-like frame conditions. Our strategy is based on conjoining two well-known approaches: we represent accessible functors as (equational) quotients of polynomial functors and then use canonicity results for boolean algebras with operators to transport completeness to the coalgebraic setting.

This paper assumes the concept of a predicate lifting from coalgebraic modal logic, and associates with every set Λ of predicate liftings for a set functor T a category \(\mathbb{C}^\Lambda_T\) of T-coalgebras and socalled Λ-homomorphisms. From this construction, some natural constructions on models such as products of models and submodels can be defined. A relationship with simulations of coalgebras arising from lax extensions is established, and the main technical result gives a condition under which the category \(\mathbb{C}^\Lambda_T\) is both complete and cocomplete.

From previous paragraphs we have understood what a category is, how to define maps between categories, namely functors, and finally how to define maps between functors, which are natural transformations. It is now possible to group all these definitions in a coherent way and define the category of functors.

In the design of concurrent and distributed systems, modularity and refinement are basic conceptual tools. We propose a notion of refinement/abstraction of local states for a basic class of Petri Nets, associated with a class of morphisms. The morphisms, from a refined system to an abstract one, associate suitable subnets to abstract local states. We define an operation of composition ruled by morphisms of that class. The main results concern behavioural properties preserved and reflected by the morphisms. In particular, we focus on the conditions under which reachable markings are preserved or reflected, and the conditions under which a morphism induces a weak bisimulation between net systems.

We pursue the principles of duality and symmetry building upon Pratt’s idea of the Stone Gamut and Abramsky’s representations of quantum systems. In the first part of the paper, we first observe that the Chu space representation of quantum systems leads us to an operational form of state-observable duality, and then show via the Chu space formalism enriched with a generic concept of closure conditions that such operational dualities (which we call “T1-type” as opposed to “sober-type”) actually exist in fairly diverse contexts (topology, measurable spaces, and domain theory, to name but a few). The universal form of T1-type dualities between point-set and point-free spaces is described in terms of Chu spaces and closure conditions. From the duality-theoretical perspective, in the second part, we improve upon Abramsky’s “fibred” coalgebraic representation of quantum symmetries, thereby obtaining a finer, “purely” coalgebraic representation: our representing category is properly smaller than Abramsky’s, but still large enough to accommodate the quantum symmetry groupoid. Among several features, our representation reduces Abramsky’s two-step construction of his representing category into a simpler one-step one, thus rendering the Grothendieck construction redundant. Our purely coalgebraic representation stems from replacing the category of sets in Abramsky’s representation with the category of closure spaces in the light of the state-observable duality telling us that closure is a right perspective on quantum state spaces.

In this paper we present a double effect version of the simply typed λ-calculus where we can represent both pure and impure quantum computations. The double effect calculus comprises a quantum arrow layer defined over a quantum monadic layer. In previous works we have developed the quantum arrow calculus, a calculus where we can consider just impure (or mixed) quantum computations. Technically, here we extend the quantum arrow calculus with a construct (and equations) that allows the communication of the monadic layer with the arrow layer of the calculus. That is, the quantum arrow is defined over a monadic instance enabling to consider pure and impure quantum computations in the same framework. As a practical contribution, the calculus allows to express quantum algorithms including reversible operations over pure states and measurements in the middle of the computation using a traditional style of functional programming and reasoning. We also define equations for algebraic reasoning of computations involving measurements.