Composition of Different-Type Relations via the Kleisli Category for the Continuation Monad

AbstractCartesian differential categories are categories equipped with a differential combinator which axiomatizes the directional derivative. Important models of Cartesian differential categories include classical differential calculus of smooth functions and categorical models of the differential $$\lambda $$ λ -calculus. However, Cartesian differential categories cannot account for other interesting notions of differentiation such as the calculus of finite differences or the Boolean differential calculus. On the other hand, change action models have been shown to capture these examples as well as more “exotic” examples of differentiation. However, change action models are very general and do not share the nice properties of a Cartesian differential category. In this paper, we introduce Cartesian difference categories as a bridge between Cartesian differential categories and change action models. We show that every Cartesian differential category is a Cartesian difference category, and how certain well-behaved change action models are Cartesian difference categories. In particular, Cartesian difference categories model both the differential calculus of smooth functions and the calculus of finite differences. Furthermore, every Cartesian difference category comes equipped with a tangent bundle monad whose Kleisli category is again a Cartesian difference category.

Download Full-text

Bistructures, Bidomains and Linear Logic

BRICS Report Series ◽

10.7146/brics.v1i9.21661 ◽

1994 ◽

Vol 1 (9) ◽

Author(s):

Gordon Plotkin ◽

Glynn Winskel

Keyword(s):

Partial Order ◽

Full Subcategory ◽

Linear Logic ◽

The Other ◽

Causal Dependency ◽

Input And Output ◽

Event Structures ◽

Kleisli Category ◽

Higher Types ◽

Cartesian Closed

Bistructures are a generalisation of event structures to represent spaces of functions at higher types; the partial order of causal dependency is replaced by two orders, one associated with input and the other output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has associated co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry's bidomains.

Download Full-text

The Kleisli Category is a Category Of Fractions

Quaestiones Mathematicae ◽

10.2989/16073600209486025 ◽

2002 ◽

Vol 25 (3) ◽

pp. 397-403 ◽

Cited By ~ 1

Author(s):

E. Giuli ◽

K.A. Hardie ◽

J.J.C. Vermeulen

Keyword(s):

Kleisli Category ◽

Category Of Fractions

Download Full-text

On semantics of a term calculus for classical logic

Publications de l Institut Mathematique ◽

10.2298/pim1206079l ◽

2012 ◽

Vol 92 (106) ◽

pp. 79-95

Author(s):

Silvia Likavec ◽

Pierre Lescanne

Keyword(s):

Classical Logic ◽

Sequent Calculus ◽

Denotational Semantics ◽

Proof System ◽

Cut Elimination ◽

Kleisli Category

The calculus of Curien and Herbelin was introduced to provide the Curry-Howard correspondence for classical logic. The terms of this calculus represent derivations in the sequent calculus proof system and reduction reflects the process of cut-elimination. We investigate some properties of two well-behaved subcalculi of untyped calculus of Curien and Herbelin, closed under the call-by-name and the call-by-value reduction, respectively. Continuation semantics is given using the category of negated domains and Moggi?s Kleisli category over predomains for the continuation monad. Soundness theorems are given for both versions thus relating operational and denotational semantics. A thorough overview of the work on continuation semantics is given.

Download Full-text

Cartesian Difference Categories

Logical Methods in Computer Science ◽

10.46298/lmcs-17(3:23)2021 ◽

2021 ◽

Vol Volume 17, Issue 3 ◽

Author(s):

Mario Alvarez-Picallo ◽

Jean-Simon Pacaud Lemay

Keyword(s):

Finite Differences ◽

Differential Calculus ◽

Directional Derivative ◽

Lambda Calculus ◽

Smooth Functions ◽

Kleisli Category ◽

Discrete Nature ◽

Categorical Models ◽

Action Models ◽

Differential Categories

Cartesian differential categories are categories equipped with a differential combinator which axiomatizes the directional derivative. Important models of Cartesian differential categories include classical differential calculus of smooth functions and categorical models of the differential $\lambda$-calculus. However, Cartesian differential categories cannot account for other interesting notions of differentiation of a more discrete nature such as the calculus of finite differences. On the other hand, change action models have been shown to capture these examples as well as more "exotic" examples of differentiation. But change action models are very general and do not share the nice properties of Cartesian differential categories. In this paper, we introduce Cartesian difference categories as a bridge between Cartesian differential categories and change action models. We show that every Cartesian differential category is a Cartesian difference category, and how certain well-behaved change action models are Cartesian difference categories. In particular, Cartesian difference categories model both the differential calculus of smooth functions and the calculus of finite differences. Furthermore, every Cartesian difference category comes equipped with a tangent bundle monad whose Kleisli category is again a Cartesian difference category.

Download Full-text

Bistructures, Bidomains and Linear Logic

BRICS Report Series ◽

10.7146/brics.v4i15.18805 ◽

1997 ◽

Vol 4 (15) ◽

Cited By ~ 1

Author(s):

Pierre-Louis Curien ◽

Gordon Plotkin ◽

Glynn Winskel

Keyword(s):

Partial Order ◽

Linear Logic ◽

The Other ◽

Causal Dependency ◽

Input And Output ◽

Event Structures ◽

Kleisli Category ◽

Higher Types ◽

Cartesian Closed Categories ◽

Cartesian Closed

Bistructures are a generalisation of event structures which allow<br />a representation of spaces of functions at higher types in an orderextensional setting. The partial order of causal dependency is replaced by two orders, one associated with input and the other with output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has an associated co-Kleisli category which is closely related to that of Berry's bidomains (both have equivalent non-trivial full sub-cartesian closed categories).

Download Full-text

Jets and differential linear logic

Mathematical Structures in Computer Science ◽

10.1017/s0960129520000249 ◽

2020 ◽

pp. 1-27

Author(s):

James Wallbridge

Keyword(s):

Vector Bundles ◽

Differential Operators ◽

Linear Logic ◽

Variational Calculus ◽

Functional Derivative ◽

Partial Differential ◽

Partial Differential Operators ◽

Kleisli Category ◽

New Interpretation ◽

Linear Differential

Abstract We prove that the category of vector bundles over a fixed smooth manifold and its corresponding category of convenient modules are models for intuitionistic differential linear logic. The exponential modality is modelled by composing the jet comonad, whose Kleisli category has linear differential operators as morphisms, with the more familiar distributional comonad, whose Kleisli category has smooth maps as morphisms. Combining the two comonads gives a new interpretation of the semantics of differential linear logic where the Kleisli morphisms are smooth local functionals, or equivalently, smooth partial differential operators, and the codereliction map induces the functional derivative. This points towards a logic, and hence a computational theory of non-linear partial differential equations and their solutions based on variational calculus.

Download Full-text