scholarly journals An explicit formula for the free exponential modality of linear logic

2017 ◽  
Vol 28 (7) ◽  
pp. 1253-1286 ◽  
Author(s):  
PAUL-ANDRÉ MELLIÈS ◽  
NICOLAS TABAREAU ◽  
CHRISTINE TASSON

The exponential modality of linear logic associates to every formula A a commutative comonoid !A which can be duplicated in the course of reasoning. Here, we explain how to compute the free commutative comonoid !A as a sequential limit of equalizers in any symmetric monoidal category where this sequential limit exists and commutes with the tensor product. We apply this general recipe to a series of models of linear logic, typically based on coherence spaces, Conway games and finiteness spaces. This algebraic description unifies for the first time a number of apparently different constructions of the exponential modality in spaces and games. It also sheds light on the duplication policy of linear logic, and its interaction with classical duality and double negation completion.

2013 ◽  
Vol 2013 ◽  
pp. 1-25
Author(s):  
Carmen Caprau

We introduce the category of singular 2-dimensional cobordisms and show that it admits a completely algebraic description as the free symmetric monoidal category on atwin Frobenius algebra, by providing a description of this category in terms of generators and relations. A twin Frobenius algebra(C,W,z,z∗)consists of a commutative Frobenius algebraC, a symmetric Frobenius algebraW, and an algebra homomorphismz:C→Wwith dualz∗:W→C, satisfying some extra conditions. We also introduce a generalized 2-dimensional Topological Quantum Field Theory defined on singular 2-dimensional cobordisms and show that it is equivalent to a twin Frobenius algebra in a symmetric monoidal category.


2020 ◽  
Vol 32 (1) ◽  
pp. 45-62 ◽  
Author(s):  
Ramon Antoine ◽  
Francesc Perera ◽  
Hannes Thiel

AbstractWe previously showed that abstract Cuntz semigroups form a closed symmetric monoidal category. This automatically provides additional structure in the category, such as a composition and an external tensor product, for which we give concrete constructions in order to be used in applications. We further analyze the structure of not necessarily commutative {\mathrm{Cu}}-semirings, and we obtain, under mild conditions, a new characterization of solid {\mathrm{Cu}}-semirings R by the condition that {R\cong\llbracket R,R\rrbracket}.


1999 ◽  
Vol 64 (1) ◽  
pp. 227-242 ◽  
Author(s):  
Kosta Došen ◽  
Zoran Petrić

AbstractIt is proved that all the isomorphisms in the cartesian category freely generated by a set of objects (i.e., a graph without arrows) can be written in terms of arrows from the symmetric monoidal category freely generated by the same set of objects. This proof yields an algorithm for deciding whether an arrow in this free cartesian category is an isomorphism.


2005 ◽  
Vol 02 (06) ◽  
pp. 1133-1186 ◽  
Author(s):  
MARC A. NIEPER-WISSKIRCHEN

Let A be an algebra over an operad in a cocomplete closed symmetric monoidal category. We study the category of A-modules. We define certain symmetric product functors of such modules generalizing the tensor product of modules over commutative algebras, which we use to define the notion of a jet module. This in turn generalizes the notion of a jet module over a module over a classical commutative algebra. We are able to define Atiyah classes (i.e., obstructions to the existence of connections) in this generalized context. We use certain model structures on the category of A-modules to study the properties of these Atiyah classes. The purpose of the paper is not to present any really deep theorem. It is more about the right concepts when dealing with modules over an algebra that is defined over an arbitrary operad, i.e., the aim is to show how to generalize various classical constructions, including modules of jets, the Atiyah class and the curvature, to the operadic context. For convenience of the reader and for the purpose of defining the notations, the basic definitions of the theory of operads and model categories are included.


Author(s):  
G.M. Bierman

Linear logic was introduced by Jean-Yves Girard in 1987. Like classical logic it satisfies the law of the excluded middle and the principle of double negation, but, unlike classical logic, it has non-degenerate models. Models of logics are often given only at the level of provability, in that they provide denotations of formulas. However, we are also interested in models which provide denotations of deductions, or proofs. Given such a model two proofs are said to be equivalent if their denotations are equal. A model is said to be ‘degenerate’ if there are no formulas for which there exist at least two non-equivalent proofs. It is easy to see that models of classical logic are essentially degenerate because any formula is either true or false and so all proofs of a formula are considered equivalent. The intuitionist approach to this problem involves altering the meaning of the logical connectives but linear logic attacks the very connectives themselves, replacing them with more refined ones. Despite this there are simple translations between classical and linear logic. One can see the need for such a refinement in another way. Both classical and intuitionistic logics could be said to deal with static truths; both validate the rule of modus ponens: if A→B and A, then B; but both also validate the rule if A→B and A, then A∧B. In mathematics this is correct since a proposition, once verified, remains true – it persists. Many situations do not reflect such persistence but rather have an additional notion of causality. An implication A→B should reflect that a state B is accessible from a state A and, moreover, that state A is no longer available once the transition has been made. An example of this phenomenon is in chemistry where an implication A→B represents a reaction of components A to yield B. Thus if two hydrogen and one oxygen atoms bond to form a water molecule, they are consumed in the process and are no longer part of the current state. Linear logic provides logical connectives to describe such refined interpretations.


2008 ◽  
Vol 18 (3) ◽  
pp. 613-643 ◽  
Author(s):  
ERNIE MANES ◽  
PHILIP MULRY

In this paper we introduce the concept of Kleisli strength for monads in an arbitrary symmetric monoidal category. This generalises the notion of commutative monad and gives us new examples, even in the cartesian-closed category of sets. We exploit the presence of Kleisli strength to derive methods for generating distributive laws. We also introduce linear equations to extend the results to certain quotient monads. Mechanisms are described for finding strengths that produce a large collection of new distributive laws, and consequently monad compositions, including the composition of monadic data types such as lists, trees, exceptions and state.


1989 ◽  
Vol 31 (1) ◽  
pp. 17-29 ◽  
Author(s):  
N. D. Gilbert ◽  
P. J. Higgins

The tensor product of two arbitrary groups acting on each other was introduced by R. Brown and J.-L. Loday in [5, 6]. It arose from consideration of the pushout of crossed squares in connection with applications of a van Kampen theorem for crossed squares. Special cases of the product had previously been studied by A. S.-T. Lue [10] and R. K. Dennis [7]. The tensor product of crossed complexes was introduced by R. Brown and the second author [3] in connection with the fundamental crossed complex π(X) of a filtered space X, which also satisfies a van Kampen theorem. This tensor product provides an algebraic description of the crossed complex π(X ⊗ Y) and gives a symmetric monoidal closed structure to the category of crossed complexes (over groupoids). Both constructions involve non-abelian bilinearity conditions which are versions of standard identities between group commutators. Since any group can be viewed as a crossed complex of rank 1, a close relationship might be expected between the two products. One purpose of this paper is to display the direct connections that exist between them and to clarify their differences.


1981 ◽  
Vol 23 (2) ◽  
pp. 209-214
Author(s):  
Stefano Kasangian ◽  
Fabio Rossi

It is shown that, for a monoidal category V, not every commutation is a symmetry and also that a commutation does not suffice to define the tensor product A ⊗ B of V-categorles A and B. Moreover, it is shown that every symmetry can be transported along a monoidal equivalence.


1992 ◽  
Vol 07 (35) ◽  
pp. 3255-3265 ◽  
Author(s):  
L. BÉGIN ◽  
P. MATHIEU ◽  
M.A. WALTON

A closed and explicit formula for all [Formula: see text] fusion coefficients is presented which, in the limit k→∞, turns into a simple and compact expression for the su(3) tensor product coefficients. The derivation is based on a new diagrammatic method which gives directly both tensor product and fusion coefficients.


Sign in / Sign up

Export Citation Format

Share Document