Showing 1–35 of 35 results for author: Cockett, R

Drazin Inverses in Categories

Authors: Robin Cockett, Jean-Simon Pacaud Lemay, Priyaa Varshinee Srinivasan

Abstract: Drazin inverses are a fundamental algebraic structure which have been extensively deployed in semigroup theory and ring theory. Drazin inverses can also be defined for endomorphisms in any category. However, beyond a paper by Puystjens and Robinson from 1987, not much has been done with Drazin inverses in category theory. As such, here we provide a survey of the theory of Drazin inverses from a ca… ▽ More Drazin inverses are a fundamental algebraic structure which have been extensively deployed in semigroup theory and ring theory. Drazin inverses can also be defined for endomorphisms in any category. However, beyond a paper by Puystjens and Robinson from 1987, not much has been done with Drazin inverses in category theory. As such, here we provide a survey of the theory of Drazin inverses from a categorical perspective. We introduce Drazin categories, in which every endomorphism has a Drazin inverse, and provide various examples including the category of matrices over a field, the category of finite length modules over a ring, and finite set enriched categories. We also introduce the notion of expressive rank and prove that a category with expressive rank is Drazin. Moreover, we study Drazin inverses in mere categories, in additive categories, and in dagger categories. In an arbitrary category, we show how a Drazin inverse corresponds to an isomorphism in the idempotent splitting, as well as explain how Drazin inverses relate to Leinster's notion of eventual image duality. In additive categories, we explore the consequences of the core-nilpotent decomposition and the image-kernel decomposition, which we relate back to Fitting's famous results. We then develop the notion of Drazin inverses for pairs of opposing maps, generalizing the usual notion of Drazin inverse for endomorphisms. As an application of this new kind of Drazin inverse, for dagger categories, we provide a novel characterization of the Moore-Penrose inverse in terms of being a Drazin inverse of the pair of a map and its adjoint. △ Less

Submitted 28 February, 2024; originally announced February 2024.

Moore-Penrose Dagger Categories

Authors: Robin Cockett, Jean-Simon Pacaud Lemay

Abstract: The notion of a Moore-Penrose inverse (M-P inverse) was introduced by Moore in 1920 and rediscovered by Penrose in 1955. The M-P inverse of a complex matrix is a special type of inverse which is unique, always exists, and can be computed using singular value decomposition. In a series of papers in the 1980s, Puystjens and Robinson studied M-P inverses more abstractly in the context of dagger cate… ▽ More The notion of a Moore-Penrose inverse (M-P inverse) was introduced by Moore in 1920 and rediscovered by Penrose in 1955. The M-P inverse of a complex matrix is a special type of inverse which is unique, always exists, and can be computed using singular value decomposition. In a series of papers in the 1980s, Puystjens and Robinson studied M-P inverses more abstractly in the context of dagger categories. Despite the fact that dagger categories are now a fundamental notion in categorical quantum mechanics, the notion of a M-P inverse has not (to our knowledge) been revisited since their work. One purpose of this paper is, thus, to renew the study of M-P inverses in dagger categories. Here we introduce the notion of a Moore-Penrose dagger category and provide many examples including complex matrices, finite Hilbert spaces, dagger groupoids, and inverse categories. We also introduce generalized versions of singular value decomposition, compact singular value decomposition, and polar decomposition for maps in a dagger category, and show how, having such a decomposition is equivalent to having M-P inverses. This allows us to provide precise characterizations of which maps have M-P inverses in a dagger idempotent complete category, a dagger kernel category with dagger biproducts (and negatives), and a dagger category with unique square roots. △ Less

Submitted 31 August, 2023; originally announced August 2023.

Comments: In Proceedings QPL 2023, arXiv:2308.15489

ACM Class: F.4.1; G.1.3;

Journal ref: EPTCS 384, 2023, pp. 171-186

Classical Distributive Restriction Categories

Authors: Robin Cockett, Jean-Simon Pacaud Lemay

Abstract: In the category of sets and partial functions, $\mathsf{PAR}$, while the disjoint union $\sqcup$ is the usual categorical coproduct, the Cartesian product $\times$ becomes a restriction categorical analogue of the categorical product: a restriction product. Nevertheless, $\mathsf{PAR}$ does have a usual categorical product as well in the form $A \& B := A \sqcup B \sqcup (A \times B)$. Surprisingl… ▽ More In the category of sets and partial functions, $\mathsf{PAR}$, while the disjoint union $\sqcup$ is the usual categorical coproduct, the Cartesian product $\times$ becomes a restriction categorical analogue of the categorical product: a restriction product. Nevertheless, $\mathsf{PAR}$ does have a usual categorical product as well in the form $A \& B := A \sqcup B \sqcup (A \times B)$. Surprisingly, asking that a distributive restriction category (a restriction category with restriction products $\times$ and coproducts $\oplus$) has $A \& B$ a categorical product is enough to imply that the category is a classical restriction category. This is a restriction category which has joins and relative complements and, thus, supports classical Boolean reasoning. The first and main observation of the paper is that a distributive restriction category is classical if and only if $A \& B := A \oplus B \oplus (A \times B)$ is a categorical product in which case we call $\&$ the ''classical'' product. In fact, a distributive restriction category has a categorical product if and only if it is a classified restriction category. This is in the sense that every map $A \to B$ factors uniquely through a total map $A \to B \oplus \mathsf{1}$, where $\mathsf{1}$ is the restriction terminal object. This implies the second significant observation of the paper, namely, that a distributive restriction category has a classical product if and only if it is the Kleisli category of the exception monad $\_ \oplus \mathsf{1}$ for an ordinary distributive category. Thus having a classical product has a significant structural effect on a distributive restriction category. In particular, the classical product not only provides an alternative axiomatization for being classical but also for being the Kleisli category of the exception monad on an ordinary distributive category. △ Less

Submitted 21 September, 2023; v1 submitted 25 May, 2023; originally announced May 2023.

Comments: We would like to dedicate this paper to Pieter Hofstra (1975-2022). Accepted in a special issue of Theory and Applications of Categories dedicated to Pieter Hofstra

Normalizing Resistor Networks

Authors: Robin Cockett, Amolak Ratan Kalra, Priyaa Varshinee Srinivasan

Abstract: Star to mesh transformations are well-known in electrical engineering, and are reminiscent of local complementation for graph states in qudit stabilizer quantum mechanics. This paper describes a rewriting system for resistor circuits over any positive division rig using general star to mesh transformations. We show how these transformations can be organized into a confluent and terminating rewriti… ▽ More Star to mesh transformations are well-known in electrical engineering, and are reminiscent of local complementation for graph states in qudit stabilizer quantum mechanics. This paper describes a rewriting system for resistor circuits over any positive division rig using general star to mesh transformations. We show how these transformations can be organized into a confluent and terminating rewriting system on the category of resistor circuits. Furthermore, based on the recently established connections between quantum and electrical circuits, this paper pushes forward the quest for approachable normal forms for stabilizer quantum circuits. △ Less

Submitted 14 December, 2023; v1 submitted 19 March, 2023; originally announced March 2023.

Comments: In Proceedings ACT 2023, arXiv:2312.08138

Journal ref: EPTCS 397, 2023, pp. 70-83

Extending Resource Monotones using Kan Extensions

Authors: Robin Cockett, Isabelle Jianing Geng, Carlo Maria Scandolo, Priyaa Varshinee Srinivasan

Abstract: In this paper we generalize the framework proposed by Gour and Tomamichel regarding extensions of monotones for resource theories. A monotone for a resource theory assigns a real number to each resource in the theory signifying the utility or the value of the resource. Gour and Tomamichel studied the problem of extending monotones using set-theoretical framework when a resource theory embeds fully… ▽ More In this paper we generalize the framework proposed by Gour and Tomamichel regarding extensions of monotones for resource theories. A monotone for a resource theory assigns a real number to each resource in the theory signifying the utility or the value of the resource. Gour and Tomamichel studied the problem of extending monotones using set-theoretical framework when a resource theory embeds fully and faithfully into the larger theory. One can generalize the problem of computing monotone extensions to scenarios when there exists a functorial transformation of one resource theory to another instead of just a full and faithful inclusion. In this article, we show that (point-wise) Kan extensions provide a precise categorical framework to describe and compute such extensions of monotones. To set up monotone extensions using Kan extensions, we introduce partitioned categories (pCat)as a framework for resource theories and pCat functors to formalize relationship between resource theories. We describe monotones as pCat functors into the preorder of non-negative real numbers, and describe extending monotones along any pCat functor using Kan extensions. We show how our framework works by applying it to extend entanglement monotones for bipartite pure states to bipartite mixed states, to extend classical divergences to the quantum setting, and to extend a non-uniformity monotone from classical probabilistic theory to quantum theory. △ Less

Submitted 31 July, 2023; v1 submitted 20 June, 2022; originally announced June 2022.

Comments: In Proceedings ACT 2022, arXiv:2307.15519

Journal ref: EPTCS 380, 2023, pp. 203-223

Categories of Kirchhoff relations

Authors: Robin Cockett, Amolak Ratan Kalra, Shiroman Prakash

Abstract: It is known that the category of affine Lagrangian relations, AffLagRel_F, over a field, F, of integers modulo a prime p (with p > 2) is isomorphic to the category of stabilizer quantum circuits for p-dits. Furthermore, it is known that electrical circuits (generalized for the field F) occur as a natural subcategory of AffLagRel_F. The purpose of this paper is to provide a characterization of the… ▽ More It is known that the category of affine Lagrangian relations, AffLagRel_F, over a field, F, of integers modulo a prime p (with p > 2) is isomorphic to the category of stabilizer quantum circuits for p-dits. Furthermore, it is known that electrical circuits (generalized for the field F) occur as a natural subcategory of AffLagRel_F. The purpose of this paper is to provide a characterization of the relations in this subcategory -- and in important subcategories thereof -- in terms of parity-check and generator matrices as used in error detection. In particular, we introduce the subcategory consisting of Kirchhoff relations to be (affinely) those Lagrangian relations that conserve total momentum or equivalently satisfy Kirchhoff's current law. Maps in this subcategory can be generated by electrical components (generalized for the field F): namely resistors, current dividers, and current and voltage sources. The "source" electrical components deliver the affine nature of the maps while current dividers add an interesting quasi-stochastic aspect. We characterize these Kirchhoff relations in terms of parity-check matrices and in addition, characterizes two important subcategories: the deterministic Kirchhoff relations and the lossless relations. The category of deterministic Kirchhoff relations as electrical circuits are generated by resistors circuits. Lossless relations, which are deterministic Kirchhoff, provide exactly the basic hyper-categorical structure of these settings. △ Less

Submitted 7 July, 2022; v1 submitted 11 May, 2022; originally announced May 2022.

Comments: 36 pages

Exponential Modalities and Complementarity (extended abstract)

Authors: Robin Cockett, Priyaa Varshinee Srinivasan

Abstract: The exponential modalities of linear logic have been used by various authors to model infinite-dimensional quantum systems. This paper explains how these modalities can also give rise to the complementarity principle of quantum mechanics. The paper uses a formulation of quantum systems based on dagger-linear logic, whose categorical semantics lies in mixed unitary categories, and a formulatio… ▽ More The exponential modalities of linear logic have been used by various authors to model infinite-dimensional quantum systems. This paper explains how these modalities can also give rise to the complementarity principle of quantum mechanics. The paper uses a formulation of quantum systems based on dagger-linear logic, whose categorical semantics lies in mixed unitary categories, and a formulation of measurement therein. The main result exhibits a complementary system as the result of measurements on free exponential modalities. Recalling that, in linear logic, exponential modalities have two distinct but dual components, ! and ?, this shows how these components under measurement become "compacted" into the usual notion of complementary Frobenius algebras from categorical quantum mechanics. △ Less

Submitted 3 November, 2022; v1 submitted 8 March, 2021; originally announced March 2021.

Comments: In Proceedings ACT 2021, arXiv:2211.01102. A full version of this paper, containing all proofs, appears at arXiv:2103:05191

Journal ref: EPTCS 372, 2022, pp. 207-220

Linearizing Combinators

Authors: Robin Cockett, Jean-Simon Pacaud Lemay

Abstract: In 2017, Bauer, Johnson, Osborne, Riehl, and Tebbe (BJORT) showed that the Abelian functor calculus provides an example of a Cartesian differential category. The definition of a Cartesian differential category is based on a differential combinator which directly formalizes the total derivative from multivariable calculus. However, in the aforementioned work the authors used techniques from Goodwil… ▽ More In 2017, Bauer, Johnson, Osborne, Riehl, and Tebbe (BJORT) showed that the Abelian functor calculus provides an example of a Cartesian differential category. The definition of a Cartesian differential category is based on a differential combinator which directly formalizes the total derivative from multivariable calculus. However, in the aforementioned work the authors used techniques from Goodwillie's functor calculus to establish a linearization process from which they then derived a differential combinator. This raised the question of what the precise relationship between linearization and having a differential combinator might be. In this paper, we introduce the notion of a linearizing combinator which abstracts linearization in the Abelian functor calculus. We then use it to provide an alternative axiomatization of a Cartesian differential category. Every Cartesian differential category comes equipped with a canonical linearizing combinator obtained by differentiation at zero. Conversely, a differential combinator can be constructed à la BJORT when one has a system of partial linearizing combinators in each context. Thus, while linearizing combinators do provide an alternative axiomatization of Cartesian differential categories, an explicit notion of partial linearization is required. This is in contrast to the situation for differential combinators where partial differentiation is automatic in the presence of total differentiation. The ability to form a system of partial linearizing combinators from a total linearizing combinator, while not being possible in general, is possible when the setting is Cartesian closed. △ Less

Submitted 18 February, 2022; v1 submitted 29 October, 2020; originally announced October 2020.

Comments: Final version. This paper has been accepted and will be published in Theory and Applications of Categories

MSC Class: 18F40; 18F50

Latent Fibrations: Fibrations for Categories of Partial Maps

Authors: Robin Cockett, Geoff Cruttwell, Jonathan Gallagher, Dorette Pronk

Abstract: Latent fibrations are an adaptation, appropriate for categories of partial maps (as presented by restriction categories), of the usual notion of fibration. The paper initiates the development of the basic theory of latent fibrations and explores some key examples. Latent fibrations cover a wide variety of examples, some of which are partial versions of standard fibrations, and some of which are pa… ▽ More Latent fibrations are an adaptation, appropriate for categories of partial maps (as presented by restriction categories), of the usual notion of fibration. The paper initiates the development of the basic theory of latent fibrations and explores some key examples. Latent fibrations cover a wide variety of examples, some of which are partial versions of standard fibrations, and some of which are particular to partial map categories (particularly those that arise in computational settings). Latent fibrations with various special properties are identified: hyperconnected latent fibrations, in particular, are shown to support the construction of a fibrational dual; this is important to reverse differential programming and, more generally, in the theory of lenses. △ Less

Submitted 28 October, 2020; originally announced October 2020.

Comments: 65 pages, submitted to "Theory and Applications of Categories"

MSC Class: 18B99 18D30

Generalising the étale groupoid--complete pseudogroup correspondence

Authors: Robin Cockett, Richard Garner

Abstract: We prove a generalisation of the correspondence, due to Resende and Lawson--Lenz, between étale groupoids---which are topological groupoids whose source map is a local homeomorphisms---and complete pseudogroups---which are inverse monoids equipped with a particularly nice representation on a topological space. Our generalisation improves on the existing functorial correspondence in four ways. Fi… ▽ More We prove a generalisation of the correspondence, due to Resende and Lawson--Lenz, between étale groupoids---which are topological groupoids whose source map is a local homeomorphisms---and complete pseudogroups---which are inverse monoids equipped with a particularly nice representation on a topological space. Our generalisation improves on the existing functorial correspondence in four ways. Firstly, we enlarge the classes of maps appearing to each side. Secondly, we generalise on one side from inverse monoids to inverse categories, and on the other side, from étale groupoids to what we call partite étale groupoids. Thirdly, we generalise from étale groupoids to source-étale categories, and on the other side, from inverse monoids to restriction monoids. Fourthly, and most far-reachingly, we generalise from topological étale groupoids to étale groupoids internal to any join restriction category C with local glueings; and on the other side, from complete pseudogroups to ``complete C-pseudogroups'', i.e., inverse monoids with a nice representation on an object of C. Taken together, our results yield an equivalence, for a join restriction category C with local glueings, between join restriction categories with a well-behaved functor to C, and partite source-étale internal categories in C. In fact, we obtain this by cutting down a larger adjunction between arbitrary restriction categories over C, and partite internal categories in C. Beyond proving this main result, numerous applications are given, which reconstruct and extend existing correspondences in the literature, and provide general formulations of completion processes. △ Less

Submitted 20 April, 2020; originally announced April 2020.

Comments: 65 pages

Differential equations in a tangent category I: Complete vector fields, flows, and exponentials

Authors: J. R. B. Cockett, G. S. H. Cruttwell, J. -S. P. Lemay

Abstract: This paper describes how to define and work with differential equations in the abstract setting of tangent categories. The key notion is that of a curve object which is, for differential geometry, the structural analogue of a natural number object. A curve object is a preinitial object for dynamical systems; dynamical systems may, in turn, be viewed as determining systems of differential equations… ▽ More This paper describes how to define and work with differential equations in the abstract setting of tangent categories. The key notion is that of a curve object which is, for differential geometry, the structural analogue of a natural number object. A curve object is a preinitial object for dynamical systems; dynamical systems may, in turn, be viewed as determining systems of differential equations. The unique map from the curve object to a dynamical system is a solution of the system, and a dynamical system is said to be complete when for all initial conditions there is a solution. A subtle issue concerns the question of when a dynamical system is complete, and the paper provides abstract conditions for this. This abstract formulation also allows new perspectives on topics such as commutative vector fields and flows. In addition, the stronger notion of a differential curve object, which is the centrepiece of the last section of the paper, has exponential maps and forms a differential exponential rig. This rig then, somewhat surprisingly, has an action on every differential object and bundle in the setting. In this manner, in a very strong sense, such a curve object plays the role of the real numbers in standard differential geometry. △ Less

Submitted 8 February, 2021; v1 submitted 27 November, 2019; originally announced November 2019.

Reverse derivative categories

Authors: Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, Dorette Pronk

Abstract: 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.… ▽ More 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. △ Less

Submitted 15 October, 2019; originally announced October 2019.

Comments: Extended version of paper to appear at CSL 2020

ACM Class: F.3.2; D.3.1

Tangent Categories from the Coalgebras of Differential Categories

Authors: Robin Cockett, Jean-Simon Pacaud Lemay, Rory B. B. Lucyshyn-Wright

Abstract: 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 opp… ▽ More 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. △ Less

Submitted 12 October, 2019; originally announced October 2019.

Comments: This is an extended version of a conference paper for CSL2020

Compact inverse categories

Authors: Robin Cockett, Chris Heunen

Abstract: The Ehresmann-Schein-Nambooripad theorem gives a structure theorem for inverse monoids: they are inductive groupoids. A particularly nice case due to Jarek is that commutative inverse monoids become semilattices of abelian groups. It has also been categorified by DeWolf-Pronk to a structure theorem for inverse categories as locally complete inductive groupoids. We show that in the case of compact… ▽ More The Ehresmann-Schein-Nambooripad theorem gives a structure theorem for inverse monoids: they are inductive groupoids. A particularly nice case due to Jarek is that commutative inverse monoids become semilattices of abelian groups. It has also been categorified by DeWolf-Pronk to a structure theorem for inverse categories as locally complete inductive groupoids. We show that in the case of compact inverse categories, this takes the particularly nice form of a semilattice of compact groupoids. Moreover, one-object compact inverse categories are exactly commutative inverse monoids. Compact groupoids, in turn, are determined in particularly simple terms of 3-cocycles by Baez-Lauda. △ Less

Submitted 10 June, 2019; originally announced June 2019.

Comments: 15 pages

Complete Positivity for Mixed Unitary Categories

Authors: Robin Cockett, Priyaa Varshinee Srinivasan

Abstract: Coecke and Heunen described completely positive maps in dagger monoidal categories and the {\sf CP}-infinity construction on these categories in order to construct a category of arbitrary dimensional quantum processes. This article generalizes the ${\sf CP}$-infinity construction of dagger monoidal categories to mixed unitary categories. Mixed unitary categories, on the one hand, generalize the (c… ▽ More Coecke and Heunen described completely positive maps in dagger monoidal categories and the {\sf CP}-infinity construction on these categories in order to construct a category of arbitrary dimensional quantum processes. This article generalizes the ${\sf CP}$-infinity construction of dagger monoidal categories to mixed unitary categories. Mixed unitary categories, on the one hand, generalize the (compact) dagger monoidal categories, and on the other hand, accommodate arbitrary dimensional quantum processes, both without sacrificing the notion of dual objects. This means that the ${\sf CP}$-infinity construction for mixed unitary categories provides a suitable semantics for higher-order quantum programming languages which employ arbitrary dimensional structures. The existing results for the ${\sf CP}$-infinity construction are shown to generalize to the new setting. In particular, the notion of environment structures generalizes to mixed unitary categories and it is shown that the ${\sf CP}$-infinity construction for mixed unitary categories is characterized by this generalized environment structure. △ Less

Submitted 23 June, 2023; v1 submitted 21 May, 2019; originally announced May 2019.

Comments: Lots of figures

3D electromagnetic modelling and inversion: A case for open-source

Authors: Douglas W. Oldenburg, Lindsey J. Heagy, Seogi Kang, Rowan Cockett

Abstract: Electromagnetics has an important role to play in solving the next generation of geoscience problems. These problems are multidisciplinary, complex, and require collaboration. This is especially true at the base scientific level where the underlying physical equations need to be solved, and data, associated with physical experiments, need to be inverted. In this paper, we present arguments for ado… ▽ More Electromagnetics has an important role to play in solving the next generation of geoscience problems. These problems are multidisciplinary, complex, and require collaboration. This is especially true at the base scientific level where the underlying physical equations need to be solved, and data, associated with physical experiments, need to be inverted. In this paper, we present arguments for adopting an open-source methodology for geophysics and provide some background about open-source software for electromagnetics. Immediate benefits are the reduced time required to carry out research, being able to collaborate, having reproducible results, and being able to disseminate results quickly. To illustrate the use of an open-source methodology in electromagnetics, we present two challenges. The first is to simulate data from a time domain airborne system over a conductive plate buried in a more resistive earth. The second is to jointly invert airborne TDEM and FDEM data with ground TDEM. SimPEG, Simulation and Parameter Estimation in Geophysics, (https://simpeg.xyz) is used for the open-source software. The figures in this paper can be reproduced by downloading the Jupyter Notebooks we provide with this paper (https://github.com/simpeg-research/oldenburg-2018-AEM). Access to the source code allows the researcher to explore the simulations and inversions by changing model and inversion parameters, plot fields and fluxes to gain further insight about the EM phenomena, and solve a new research problem by using open-source software as a base. By providing results in a manner that allows others to reproduce, further explore, and even extend them, we hope to demonstrate that an open-source paradigm has the potential to enable more rapid progress of the geophysics community as a whole. △ Less

Submitted 21 February, 2019; originally announced February 2019.

Journal ref: Exploration Geophysics, 51(1), 25-37 (2020)

Open source software for simulations and inversions of airborne electromagnetic data

Authors: Lindsey J. Heagy, Seogi Kang, Rowan Cockett, Douglas Oldenburg

Abstract: Inversions of airborne EM data are often an iterative process, not only requiring that the researcher be able to explore the impact of changing components such as the choice of regularization functional or model parameterization, but also often requiring that forward simulations be run and fields and fluxes visualized in order to build an understanding of the physical processes governing what we o… ▽ More Inversions of airborne EM data are often an iterative process, not only requiring that the researcher be able to explore the impact of changing components such as the choice of regularization functional or model parameterization, but also often requiring that forward simulations be run and fields and fluxes visualized in order to build an understanding of the physical processes governing what we observe in the data. In the hope of facilitating this exploration and promoting reproducibility of geophysical simulations and inversions, we have developed the open source software package, SimPEG. The software has been designed to be modular and extensible with the goal of allowing researchers to interrogate all of the components and to facilitate the exploration of new inversion strategies. We present an overview of the software in its application to airborne EM and demonstrate its use for visualizing fields and fluxes in a forward simulation as well as its flexibility in formulating and solving the inverse problem. We invert a line of airborne TDEM data over a conductive vertical plate using a 1D voxel-inversion, a 2D voxel inversion and a parametric inversion, where all of the forward modelling is done on a 3D grid. The results in this paper can be reproduced by using the provided Jupyter notebooks. The Python software can also be modified to allow users to experiment with parameters and explore the physics of the electromagnetics and intricacies of inversion. △ Less

Submitted 21 February, 2019; originally announced February 2019.

Journal ref: Exploration Geophysics, 51(1), 38-44 (2020)

Dagger linear logic for categorical quantum mechanics

Authors: Robin Cockett, Cole Comfort, Priyaa Srinivasan

Abstract: 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… ▽ More 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. △ Less

Submitted 15 November, 2021; v1 submitted 1 September, 2018; originally announced September 2018.

MSC Class: 18b99; 81P10; 03G12 ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (November 16, 2021) lmcs:7030

Differential Categories Revisited

Authors: R. F. Blute, J. R. B. Cockett, J-S. Pacaud Lemay, R. A. G. Seely

Abstract: Differential categories were introduced to provide a minimal categorical doctrine for differential linear logic. Here we revisit the formalism and, in particular, examine the two different approaches to defining differentiation which were introduced. The basic approach used a deriving transformation, while a more refined approach, in the presence of a bialgebra modality, used a codereliction. The… ▽ More Differential categories were introduced to provide a minimal categorical doctrine for differential linear logic. Here we revisit the formalism and, in particular, examine the two different approaches to defining differentiation which were introduced. The basic approach used a deriving transformation, while a more refined approach, in the presence of a bialgebra modality, used a codereliction. The latter approach is particularly relevant to linear logic settings, where the coalgebra modality is monoidal and the Seely isomorphisms give rise to a bialgebra modality. Here, we prove that these apparently distinct notions of differentiation, in the presence of a monoidal coalgebra modality, are completely equivalent. Thus, for linear logic settings, there is only one notion of differentiation. This paper also presents a number of separating examples for coalgebra modalities including examples which are and are not monoidal, as well as examples which do and do not support differential structure. Of particular interest is the observation that -- somewhat counter-intuitively -- differential algebras never induce a differential category although they provide a monoidal coalgebra modality. On the other hand, Rota-Baxter algebras -- which are usually associated with integration -- provide an example of a differential category which has a non-monoidal coalgebra modality. △ Less

Submitted 7 May, 2019; v1 submitted 12 June, 2018; originally announced June 2018.

Comments: This is an extended version of "There is only one notion of differentiation." Cockett, R., & Lemay, J-S., 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Finiteness spaces and generalized power series

Authors: Richard Blute, Robin Cockett, Pierre-Alain Jacqmin, Philip Scott

Abstract: We consider Ribenboim's construction of rings of generalized power series. Ribenboim's construction makes use of a special class of partially ordered monoids and a special class of their subsets. While the restrictions he imposes might seem conceptually unclear, we demonstrate that they are precisely the appropriate conditions to represent such monoids as internal monoids in an appropriate categor… ▽ More We consider Ribenboim's construction of rings of generalized power series. Ribenboim's construction makes use of a special class of partially ordered monoids and a special class of their subsets. While the restrictions he imposes might seem conceptually unclear, we demonstrate that they are precisely the appropriate conditions to represent such monoids as internal monoids in an appropriate category of Ehrhard's finiteness spaces. Ehrhard introduced finiteness spaces as the objects of a categorical model of classical linear logic, where a set is equipped with a class of subsets to be thought of as finitary. Morphisms are relations preserving the finitary structure. The notion of finitary subset allows for a sharper analysis of computational structure than is available in the relational model. For example, fixed point operators fail to be finitary. In the present work, we take morphisms to be partial functions preserving the finitary structure rather than relations. The resulting category is symmetric monoidal closed, complete and cocomplete. Any pair of an internal monoid in this category and a ring induces a ring of generalized power series by an extension of the Ribenboim construction based on Ehrhard's notion of linearization of a finiteness space. We thus further generalize Ribenboim's constructions. We give several examples of rings which arise from this construction, including the ring of Puiseux series and the ring of formal power series generated by a free monoid. △ Less

Submitted 24 May, 2018; originally announced May 2018.

MSC Class: 18D10; 18D35; 13J05

The Category TOF

Authors: J. R. B. Cockett, Cole Comfort

Abstract: We provide a complete set of identities for the symmetric monoidal category, TOF, generated by the Toffoli gate and computational ancillary bits. We do so by demonstrating that the functor which evaluates circuits on total points, is an equivalence into the full subcategory of sets and partial isomorphisms with objects finite powers of the two element set. The structure of the proof builds -- and… ▽ More We provide a complete set of identities for the symmetric monoidal category, TOF, generated by the Toffoli gate and computational ancillary bits. We do so by demonstrating that the functor which evaluates circuits on total points, is an equivalence into the full subcategory of sets and partial isomorphisms with objects finite powers of the two element set. The structure of the proof builds -- and follows the proof of Cockett et al.-- which provided a full set of identities for the cnot gate with computational ancillary bits. Thus, first it is shown that TOF is a discrete inverse category in which all of the identities for the cnot gate hold; and then a normal form for the restriction idempotents is constructed which corresponds precisely to subobjects of the total points of TOF. This is then used to show that TOF is equivalent to FPinj2, the full subcategory of sets and partial isomorphisms in which objects have cardinality a power of 2. △ Less

Submitted 29 January, 2019; v1 submitted 27 April, 2018; originally announced April 2018.

Comments: In Proceedings QPL 2018, arXiv:1901.09476

Journal ref: EPTCS 287, 2019, pp. 67-84

Integral Categories and Calculus Categories

Authors: J. R. B. Cockett, JS Lemay

Abstract: 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, $s_A: !A \to !A \otimes A$, in a symmetric monoidal category with a coalgebra modality. When integratio… ▽ More 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, $s_A: !A \to !A \otimes 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 theorem is called a {\em calculus category\/}. Modifying an approach to antiderivatives by T. Ehrhard, we define having antiderivatives as the demand that a certain natural transformation, $K: !A \to !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. △ Less

Submitted 19 December, 2017; v1 submitted 25 July, 2017; originally announced July 2017.

Comments: Preprint, Submitted to Mathematical Structures in Computer Science

MSC Class: 18D10; 03F52

Journal ref: Math. Struct. Comp. Sci. 29 (2019) 243-308

The Category CNOT

Authors: Robin Cockett, Cole Comfort, Priyaa Srinivasan

Abstract: We exhibit a complete set of identities for CNOT, the symmetric monoidal category generated by the controlled-not gate, the swap gate, and the computational ancillae. We prove that CNOT is a discrete inverse category. Moreover, we prove that CNOT is equivalent to the category of partial isomorphisms of finitely-generated non-empty commutative torsors of characteristic 2. Equivalently this is the c… ▽ More We exhibit a complete set of identities for CNOT, the symmetric monoidal category generated by the controlled-not gate, the swap gate, and the computational ancillae. We prove that CNOT is a discrete inverse category. Moreover, we prove that CNOT is equivalent to the category of partial isomorphisms of finitely-generated non-empty commutative torsors of characteristic 2. Equivalently this is the category of affine partial isomorphisms between finite-dimensional Z2 vector spaces. △ Less

Submitted 1 March, 2018; v1 submitted 5 July, 2017; originally announced July 2017.

Comments: In Proceedings QPL 2017, arXiv:1802.09737

Journal ref: EPTCS 266, 2018, pp. 258-293

A numerical method for efficient 3D inversions using Richards equation

Authors: Rowan Cockett, Lindsey J. Heagy, Eldad Haber

Abstract: Fluid flow in the vadose zone is governed by Richards equation; it is parameterized by hydraulic conductivity, which is a nonlinear function of pressure head. Investigations in the vadose zone typically require characterizing distributed hydraulic properties. Saturation or pressure head data may include direct measurements made from boreholes. Increasingly, proxy measurements from hydrogeophysics… ▽ More Fluid flow in the vadose zone is governed by Richards equation; it is parameterized by hydraulic conductivity, which is a nonlinear function of pressure head. Investigations in the vadose zone typically require characterizing distributed hydraulic properties. Saturation or pressure head data may include direct measurements made from boreholes. Increasingly, proxy measurements from hydrogeophysics are being used to supply more spatially and temporally dense data sets. Inferring hydraulic parameters from such datasets requires the ability to efficiently solve and deterministically optimize the nonlinear time domain Richards equation. This is particularly important as the number of parameters to be estimated in a vadose zone inversion continues to grow. In this paper, we describe an efficient technique to invert for distributed hydraulic properties in 1D, 2D, and 3D. Our algorithm does not store the Jacobian, but rather computes the product with a vector, which allows the size of the inversion problem to become much larger than methods such as finite difference or automatic differentiation; which are constrained by computation and memory, respectively. We show our algorithm in practice for a 3D inversion of saturated hydraulic conductivity using saturation data through time. The code to run our examples is open source and the algorithm presented allows this inversion process to run on modest computational resources. △ Less

Submitted 11 June, 2017; originally announced June 2017.

Comments: Computers and Geosciences (2018)

Connections in Tangent Categories

Authors: J. R. B. Cockett, G. S. H. Cruttwell

Abstract: Connections are an important tool of differential geometry. This paper investigates their definition and structure in the abstract setting of tangent categories. At this level of abstraction we derive several classically important results about connections, including the Bianchi identities, identities for curvature and torsion, almost complex structure, and parallel transport. Connections are an important tool of differential geometry. This paper investigates their definition and structure in the abstract setting of tangent categories. At this level of abstraction we derive several classically important results about connections, including the Bianchi identities, identities for curvature and torsion, almost complex structure, and parallel transport. △ Less

Submitted 27 July, 2017; v1 submitted 27 October, 2016; originally announced October 2016.

Comments: This version fixes a number of typos and small errors in an earlier version. To be published in Theory and Applications of Categories

MSC Class: 18D99; 53B05; 53B15; 51K10

A framework for simulation and inversion in electromagnetics

Authors: Lindsey J. Heagy, Rowan Cockett, Seogi Kang, Gudni K. Rosenkjaer, Douglas W. Oldenburg

Abstract: Simulations and inversions of electromagnetic geophysical data are paramount for discerning meaningful information about the subsurface from these data. Depending on the nature of the source electromagnetic experiments may be classified as time-domain or frequency-domain. Multiple heterogeneous and sometimes anisotropic physical properties, including electrical conductivity and magnetic permeabili… ▽ More Simulations and inversions of electromagnetic geophysical data are paramount for discerning meaningful information about the subsurface from these data. Depending on the nature of the source electromagnetic experiments may be classified as time-domain or frequency-domain. Multiple heterogeneous and sometimes anisotropic physical properties, including electrical conductivity and magnetic permeability, may need be considered in a simulation. Depending on what one wants to accomplish in an inversion, the parameters which one inverts for may be a voxel-based description of the earth or some parametric representation that must be mapped onto a simulation mesh. Each of these permutations of the electromagnetic problem has implications in a numerical implementation of the forward simulation as well as in the computation of the sensitivities, which are required when considering gradient-based inversions. This paper proposes a framework for organizing and implementing electromagnetic simulations and gradient-based inversions in a modular, extensible fashion. We take an object-oriented approach for defining and organizing each of the necessary elements in an electromagnetic simulation, including: the physical properties, sources, formulation of the discrete problem to be solved, the resulting fields and fluxes, and receivers used to sample to the electromagnetic responses. A corresponding implementation is provided as part of the open source simulation and parameter estimation project SimPEG (http://simpeg.xyz). The application of the framework is demonstrated through two synthetic examples and one field example. △ Less

Submitted 26 June, 2017; v1 submitted 3 October, 2016; originally announced October 2016.

Journal ref: Computers & Geosciences, 107(July), 1-19 (2017)

Differential bundles and fibrations for tangent categories

Authors: J. R. B. Cockett, G. S. H. Cruttwell

Abstract: Tangent categories are categories equipped with a tangent functor: an endofunctor with certain natural transformations which make it behave like the tangent bundle functor on the category of smooth manifolds. They provide an abstract setting for differential geometry by axiomatizing key aspects of the subject which allow the basic theory of these geometric settings to be captured. Importantly, the… ▽ More Tangent categories are categories equipped with a tangent functor: an endofunctor with certain natural transformations which make it behave like the tangent bundle functor on the category of smooth manifolds. They provide an abstract setting for differential geometry by axiomatizing key aspects of the subject which allow the basic theory of these geometric settings to be captured. Importantly, they have models not only in classical differential geometry and its extensions, but also in algebraic geometry, combinatorics, computer science, and physics. This paper develops the theory of "differential bundles" for such categories, considers their relation to "differential objects", and develops the theory of fibrations of tangent categories. Differential bundles generalize the notion of smooth vector bundles in classical differential geometry. However, the definition departs from the standard one in several significant ways: in general, there is no scalar multiplication in the fibres of these bundles, and in general these bundles need not be locally trivial. To understand how these differential bundles relate to differential objects, which are the generalization of vector spaces in smooth manifolds, requires some careful handling of the behaviour of pullbacks with respect to the tangent functor. This is captured by "transverse" and "display" systems for tangent categories, which leads one into the fibrational theory of tangent categories. A key example of a tangent fibration is provided by the "display" differential bundles of a tangent category with a display system. Strikingly, in such examples the fibres are Cartesian differential categories demonstrating a -- not unexpected -- tight connection between the theory of these categories and that of tangent categories. △ Less

Submitted 9 March, 2017; v1 submitted 27 June, 2016; originally announced June 2016.

Comments: Updated version, to be published in Cahiers de topologie et geometrie differentielle categoriques

MSC Class: 18D30; 18F15; 57R22

Cartesian Differential Storage Categories

Authors: Richard Blute, Robin Cockett, Robert Seely

Abstract: Cartesian differential categories were introduced to provide an abstract axiomatization of categories of differentiable functions. The fundamental example is the category whose objects are Euclidean spaces and whose arrows are smooth maps. Tensor differential categories provide the framework for categorical models of differential linear logic. The coKleisli category of any tensor differential ca… ▽ More Cartesian differential categories were introduced to provide an abstract axiomatization of categories of differentiable functions. The fundamental example is the category whose objects are Euclidean spaces and whose arrows are smooth maps. Tensor differential categories provide the framework for categorical models of differential linear logic. The coKleisli category of any tensor differential category is always a Cartesian differential category. Cartesian differential categories, besides arising in this manner as coKleisli categories, occur in many different and quite independent ways. Thus, it was not obvious how to pass from Cartesian differential categories back to tensor differential categories. This paper provides natural conditions under which the linear maps of a Cartesian differential category form a tensor differential category. This is a question of some practical importance as much of the machinery of modern differential geometry is based on models which implicitly allow such a passage, and thus the results and tools of the area tend to freely assume access to this structure. The purpose of this paper is to make precise the connection between the two types of differential categories. As a prelude to this, however, it is convenient to have available a general theory which relates the behaviour of "linear" maps in Cartesian categories to the structure of Seely categories. The latter were developed to provide the categorical semantics for (fragments of) linear logic which use a "storage" modality. The general theory of storage, which underlies the results mentioned above, is developed in the opening sections of the paper and is then applied to the case of differential categories. △ Less

Submitted 27 May, 2014; originally announced May 2014.

Restriction categories as enriched categories

Authors: Robin Cockett, Richard Garner

Abstract: Restriction categories were introduced to provide an axiomatic setting for the study of partially defined map**s; they are categories equipped with an operation called restriction which assigns to every morphism an endomorphism of its domain, to be thought of as the partial identity that is defined to just the same degree as the original map. In this paper, we show that restriction categories ca… ▽ More Restriction categories were introduced to provide an axiomatic setting for the study of partially defined map**s; they are categories equipped with an operation called restriction which assigns to every morphism an endomorphism of its domain, to be thought of as the partial identity that is defined to just the same degree as the original map. In this paper, we show that restriction categories can be identified with \emph{enriched categories} in the sense of Kelly for a suitable enrichment base. By varying that base appropriately, we are also able to capture the notions of join and range restriction category in terms of enriched category theory. △ Less

Submitted 26 November, 2012; originally announced November 2012.

Comments: 29 pages

Differential restriction categories

Authors: J. R. B. Cockett, G. S. H. Cruttwell, J. D. Gallagher

Abstract: We combine two recent ideas: cartesian differential categories, and restriction categories. The result is a new structure which axiomatizes the category of smooth maps defined on open subsets of $\R^n$ in a way that is completely algebraic. We also give other models for the resulting structure, discuss what it means for a partial map to be additive or linear, and show that differential restriction… ▽ More We combine two recent ideas: cartesian differential categories, and restriction categories. The result is a new structure which axiomatizes the category of smooth maps defined on open subsets of $\R^n$ in a way that is completely algebraic. We also give other models for the resulting structure, discuss what it means for a partial map to be additive or linear, and show that differential restriction structure can be lifted through various completion operations. △ Less

Submitted 20 August, 2012; originally announced August 2012.

Comments: 72 pages

MSC Class: 18D99

Journal ref: Theory Appl. Categ. 25 (2011), No. 21, pp 537--613

On the word problem for SP-categories, and the properties of two-way communication

Authors: Luigi Santocanale, Robin Cockett

Abstract: The word problem for categories with free products and coproducts (sums), SP-categories, is directly related to the problem of determining the equivalence of certain processes. Indeed, the maps in these categories may be directly interpreted as processes which communicate by two-way channels. The maps of an SP-category may also be viewed as a proof theory for a simple logic with a game theoretic… ▽ More The word problem for categories with free products and coproducts (sums), SP-categories, is directly related to the problem of determining the equivalence of certain processes. Indeed, the maps in these categories may be directly interpreted as processes which communicate by two-way channels. The maps of an SP-category may also be viewed as a proof theory for a simple logic with a game theoretic intepretation. The cut-elimination procedure for this logic determines equality only up to certain permuting conversions. As the equality classes under these permuting conversions are finite, it is easy to see that equality between cut-free terms (even in the presence of the additive units) is decidable. Unfortunately, this does not yield a tractable decision algorithm as these equivalence classes can contain exponentially many terms. However, the rather special properties of these free categories -- and, thus, of two-way communication -- allow one to devise a tractable algorithm for equality. We show that, restricted to cut-free terms s,t : X --> A, the decision procedure runs in time polynomial on |X||A|, the product of the sizes of the domain and codomain type. △ Less

Submitted 9 April, 2009; originally announced April 2009.

The logic of message passing

Authors: J. R. B. Cockett, Craig Pastro

Abstract: Message passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message passing. In order to achieve this we introduce the categorical notion of a linear actegory and the related polycategorical notion of a poly-actegory. Not surprisingly the notation used for the ter… ▽ More Message passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message passing. In order to achieve this we introduce the categorical notion of a linear actegory and the related polycategorical notion of a poly-actegory. Not surprisingly the notation used for the term calculus borrows heavily from the (synchronous) pi-calculus. The cut elimination procedure for the system provides an operational semantics. △ Less

Submitted 14 November, 2007; v1 submitted 23 March, 2007; originally announced March 2007.

Comments: 51 pages

Journal ref: Science of Computer Programming 74 no.8 (2009) 498-533

Restriction categories III: colimits, partial limits, and extensivity

Authors: J. R. B. Cockett, Stephen Lack

Abstract: 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 partia… ▽ More 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. △ Less

Submitted 16 October, 2006; originally announced October 2006.

Comments: 39 pages

MSC Class: 18B99; 18A30; 18D20; 68P05

Journal ref: Mathematical Structures in Computer Science, 17(4):775-817, 2007

A language for multiplicative-additive linear logic

Authors: J. R. B. Cockett, C. A. Pastro

Abstract: A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive categories with additives. It is also shown that proof equivalence is decidable by showing that the cut elimination rewrites supply a confluent rewriting system mod… ▽ More A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive categories with additives. It is also shown that proof equivalence is decidable by showing that the cut elimination rewrites supply a confluent rewriting system modulo equations. △ Less

Submitted 15 April, 2004; originally announced April 2004.

Comments: 16 pages without appendices, 30 with appendices

MSC Class: 18C50; 03F52; 03F05

Journal ref: Electronic Notes in Theoretical Computer Science 122 (2005) 23-65

On the complexity of Cockett-Seely polarized games

Authors: J. R. B. Cockett, C. A. Pastro

Abstract: In this paper the complexity of provability of polarized additive, multiplicative, and exponential formulas in the (initial) Cockett-Seely polarized game logic is discussed. The complexity is ultimately based on the complexity of finding a strategy in a formula which is, for polarized additive formulas, in the worst case linear in their size. Having a proof of a sequent is equivalent to having a… ▽ More In this paper the complexity of provability of polarized additive, multiplicative, and exponential formulas in the (initial) Cockett-Seely polarized game logic is discussed. The complexity is ultimately based on the complexity of finding a strategy in a formula which is, for polarized additive formulas, in the worst case linear in their size. Having a proof of a sequent is equivalent to having a strategy for the internal-hom object. In order to show that the internal-hom object can have size exponentially larger than the formulas of the original sequent we develop techniques for calculating the size of the multiplicative formulas. The structure of the internal hom object can be exploited and, using dynamic programming techniques, one can reduce the cost of finding a strategy in such a formula to the order of the product of the sizes of the original formulas. The use of dynamic techniques motivates the consideration of games as acyclic graphs and we show how to calculate the size of these graph games for the multiplicative and additive fragment and, thus, the cost of determining their provability using this dynamic programming approach. The final section of the paper points out that, despite the apparent complexity of the formulas, there is, for the initial polarized logic with all the connectives (additives, multiplicatives, and exponentials) a way of determining provability which is \emph{linear} in the size of the formulas. △ Less

Submitted 29 February, 2004; v1 submitted 26 February, 2004; originally announced February 2004.

Comments: 27 pages

MSC Class: 03F20; 03F52; 18A15