Categorical quantum mechanics exploits the dagger compact closed structure of finite dimensional Hilbert spaces, and uses the graphical calculus of string diagrams to facilitate reasoning about finite dimensional processes. A significant portion of quantum physics, however, involves reasoning about infinite dimensional processes, and it is well-known that the category of all Hilbert spaces is not compact closed. Thus, a limitation of using dagger compact closed categories is that one cannot directly accommodate reasoning about infinite dimensional processes. A natural categorical generalization of compact closed categories, in which infinite dimensional spaces can be modelled, is *-autonomous categories and, more generally, linearly distributive categories. This article starts the development of this direction of generalizing categorical quantum mechanics. An important first step is to establish the behaviour of the dagger in these more general settings. Thus, these notes simultaneously develop the categorical semantics of multiplicative dagger linear logic. The notes end with the definition of a mixed unitary category. It is this structure which is subsequently used to extend the key features of categorical quantum mechanics.

The reverse derivative is a fundamental operation in machine learning and automatic differentiation. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by Cartesian differential categories for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.

Following the pattern from linear logic, the coKleisli category of a differential category is a Cartesian differential category. What then is the coEilenberg-Moore category of a differential category? The answer is a tangent category! A key example arises from the opposite of the category of Abelian groups with the free exponential modality. The coEilenberg-Moore category, in this case, is the opposite of the category of commutative rings. That the latter is a tangent category captures a fundamental aspect of both algebraic geometry and Synthetic Differential Geometry. The general result applies when there are no negatives and thus encompasses examples arising from combinatorics and computer science. This is an extended version of a conference paper for CSL2020.

Abstract The paper shows how the Scott–Koymans theorem for the untyped λ-calculus can be extended to the differential λ-calculus. The main result is that every model of the untyped differential λ-calculus may be viewed as a differential reflexive object in a Cartesian-closed differential category. This extension of the Scott–Koymans theorem depends critically on unraveling the somewhat subtle issue of which idempotents can be split so that differential structure lifts to the idempotent splitting. The paper uses (total) Turing categories with “canonical codes” as the basic categorical semantics for the λ-calculus. It develops the main result in a modular fashion by showing how to add left-additive structure to a Turing category, and then – on top of that – differential structure. For both levels of structure, it is necessary to identify how “canonical codes” must behave with respect to the added structure and, furthermore, how “universal objects” must behave. The latter is closely tied to the question – which is the crux of the paper – of which idempotents can be split while preserving the differential structure of the setting. This paper is the full version of a conference paper and includes the proofs which were omitted from that version due to page-length restrictions.

Differential categories are now an established abstract setting for differentiation. However, not much attention has been given to the process which is inverse to differentiation: integration. This paper presents the parallel development for integration by axiomatizing an integral transformation, sA: !A → !A ⊗ A, in a symmetric monoidal category with a coalgebra modality. When integration is combined with differentiation, the two fundamental theorems of calculus are expected to hold (in a suitable sense): a differential category with integration which satisfies these two theorems is called a calculus category. Modifying an approach to antiderivatives by T. Ehrhard, we define having antiderivatives as the demand that a certain natural transformation, K: !A → !A, is invertible. We observe that a differential category having antiderivatives, in this sense, is always a calculus category. When the coalgebra modality is monoidal, it is natural to demand an extra coherence between integration and the coalgebra modality. In the presence of this extra coherence, we show that a calculus category with a monoidal coalgebra modality has its integral transformation given by antiderivatives and, thus, that the integral structure is uniquely determined by the differential structure. The paper finishes by providing a suite of separating examples. Examples of differential categories, integral categories and calculus categories based on both monoidal and (mere) coalgebra modalities are presented. In addition, differential categories which are not integral categories are discussed and vice versa.

A restriction category is an abstract category of partial maps. A Boolean restriction category is a restriction category that supports classical (Boolean) reasoning. Such categories are models of loop-free dynamic logic that is deterministic in the sense that < α > Q ⊂ [α]Q. Classical restriction categories are restriction categories with a locally Boolean structure: it is shown that they are precisely full subcategories of Boolean restriction categories. In particular, a Boolean restriction category may be characterised as a classical restriction category with finite coproducts in which all restriction idempotents split. Every restriction category admits a restriction embedding into a Boolean restriction category. Thus, every abstract category of partial maps admits a conservative extension that supports classical reasoning. An explicit construction of the classical completion of a restriction category is given.

A restriction category is an abstract formulation for a category of partial maps, defined in terms of certain specified idempotents called the restriction idempotents. All categories of partial maps are restriction categories; conversely, a restriction category is a category of partial maps if and only if the restriction idempotents split. Restriction categories facilitate reasoning about partial maps as they have a purely algebraic formulation. In this paper we consider colimits and limits in restriction categories. As the notion of restriction category is not self-dual, we should not expect colimits and limits in restriction categories to behave in the same manner. The notion of colimit in the restriction context is quite straightforward, but limits are more delicate. The suitable notion of limit turns out to be a kind of lax limit, satisfying certain extra properties. Of particular interest is the behaviour of the coproduct, both by itself and with respect to partial products. We explore various conditions under which the coproducts are ‘extensive’ in the sense that the total category (of the related partial map category) becomes an extensive category. When partial limits are present, they become ordinary limits in the total category. Thus, when the coproducts are extensive we obtain as the total category a lextensive category. This provides, in particular, a description of the extensive completion of a distributive category.

Following work of Ehrhard and Regnier, we introduce the notion of a differential category: an additive symmetric monoidal category with a comonad (a ‘coalgebra modality’) and a differential combinator satisfying a number of coherence conditions. In such a category one should imagine the morphisms in the base category as being linear maps and the morphisms in the coKleisli category as being smooth (infinitely differentiable). Although such categories do not necessarily arise from models of linear logic, one should think of this as replacing the usual dichotomy of linear vs. stable maps established for coherence spaces.After establishing the basic axioms, we give a number of examples. The most important example arises from a general construction, a comonad -calculus.

This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics that contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the ‘noncommutative logic’ of Abrusci and Ruet, a variant of linear logic that has both commutative and noncommutative connectives. Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasise the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, in order to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality.

We continue our study of the negation-free structure of multiplicative linear logic, as represented by the structure of weakly distributive categories, to consider the ‘exponentials’! and ? in the weakly distributive context. In addition to the usual triple and cotriple structure that one would expect on each of the two operators, there must be some connection between them to replace the de Morgan relationship found in the linear logic context. This turns out to be the notion of tensorial strength. We analyze coherence for this situation, using a modification of the usual nets due to Danos, which is a form suitable for linear logic with exponentials but without negation.

Distributive category theory is the study of categories with two monoidal structures, one of which “distributes” over the other in some manner. When these are the product and coproduct, this distribution is taken to be the law which asserts that the obvious canonical map has an inverse. A distributive category is here taken to mean a category with finite products and binary coproducts such that this law is satisfied. In any distributive category the coproduct of the final object with itself, 1 + 1, forms a boolean algebra. Thus, maps into 1 + 1 provide a boolean logic: if each such map recognizes a unique subobject, the category is a recognizable distributive category. If, furthermore, the category is such that these recognizers classify detachable subobjects (coproduct embeddings), it is an extensive distributive category. Extensive distributive categories can be approached in various ways. For example, recognizable distributive categories, in which coproducts are disjoint or all preinitials are isomorphic, are extensive. Also, a category X having finite products and binary coproducts satisfying the slice equation (due to Schanuel and Lawvere) is extensive. This paper describes a series of embedding theorems. Any distributive category has a full faithful embedding into a recognizable distributive category. Any recognizable distributive category can be "solidified" faithfully to produce an extensive distributive category. Any extensive distributive category can be embedded into a topos. A peculiar source of extensive distributive categories is the coproduct completion of categories with familial finite products. In particular, this includes the coproduct completion of cartesian categories, which is serendipitously, therefore, also the distributive completion. Familial distributive categories can be characterized as distributive categories for which every object has a finite decomposition into indecomposables.

The reduction algorithm is a technique for improving a decision tree in the abseence of aproecise cost criterion. The result of applying the algorithm is an irreducible tree that is no less efficient than the original, and may be more efficient. Irreducible trees arise in discrete decision theory as an algebraic form for decision trees. This form has significant computational properties. In fact, every irreducible is optimal with respect to some expected testing cost criterion and is strictly better than any given distinct tree with respect to some criterion. Many irreducibles are decision equivalent to a given tree; onely some of these are reductions of the tree. The reduction algorithm is a particular way of finding one of these. It tends to preserve the overall structure of the tree by reducing the subtrees first. A bound on the complexity of this algorithm with input tree t is O (hgt9 t ) 2 ). usize( t ) is the uniform size of the tree (the number of leaves less one) and hgt( t ) is the height of the tree. This means that decision tree reduction has the same worst-case order of complexity as most heuristic methods for building suboptimal trees. While the purpose of using heuristics is often rather different, such comparisons are an indication of the efficiency of the reduction algorithms.

The use of rule-based methodologies in the development of Expert Systems is widespread. In order to provide good explanations in these systems it is desirable that the rules be prime. The difficulty of expressing control in such rules, and thus arriving at a desirable sequencing of events, has led to pragmatic additions to the basic methodology. Recent developments in the theory of decision processes have provided new insight into the form of a desirable sequencing. Prime rules, even when augmented by sophisticated control strategies, cannot generate from backward chaining all these desirable sequencings. Furthermore, if one of these desirable sequencings happens to be generated from prime rules it may be by luck rather than design.