MELL in a Free Compact Closure

Etienne Duchesne

Description

Niveau: Supérieur, Doctorat, Bac+8
MELL in a Free Compact Closure Etienne Duchesne Laboratoire d'Informatique de Paris Nord Abstract. We present a step by step construction of the exponential modality in the context of the free compact closure Int(PInj) of sets and partial functions. Each step provides a key feature necessary to compute the exponential formula of Mellies, Tabareau & Tasson [MTT09]. We obtain a denotational model of multi- plicative and exponential linear logic based on the geometry of interaction. 1 Introduction Linear logic relies on a policy of hypothesis consumption: when proving a sequent A1, . . . , An B, each hypothesis Ai is used exactly once in the course of the reason- ing. This restriction restores the idempotency of double negation A?? = A, and in particular the linear implication A( B can be defined by means of linear conjunction (the tensor product ?) and negation: A( B = (A?B?)?. However most reasonings need the duplication or the discarding of the hypothesis. The role of the exponential modality !A is to provide this expressivity: we explicitly denote !A the formula A on which we want to perform such non-linear reasonings. The logic obtained from these connectives is called multiplicative and exponential linear logic (MELL). The general structure shared by the various models of MELL can be expressed synthetically with the language of category theory (see [Mel02] for a survey).

• trace operator


• category having


• a?u ?


• free compact


• m? ?


• ip-pairs m?


• exponential


• category


• injection-projection pair


• tive comonoid

Sujets

• Duchesne
• Trace operator
• Exponential
• Category

Informations

• Publié par: mijec
• Nombre de lectures: 18
• Langue: English

Extrait

1

MELL in a Free Compact Closure

Etienne Duchesne

Laboratoire d’Informatique de Paris Nord [e-mail]

Abstract.by step construction of the exponential modality inWe present a step the context of the free compact closureInt(PInj)of sets and partial functions. Each step provides a key feature necessary to compute the exponential formula of Melli ` es,Tabareau&Tasson[MTT09].Weobtainadenotationalmodelofmulti- plicative and exponential linear logic based on the geometry of interaction.

Introduction

Linear logic relies on a policy of hypothesis consumption: when proving a sequent A 1 , . . . , A n `B, each hypothesisA i is used exactly once in the course of the reason- ing. This restriction restores the idempotency of double negationA ⊥⊥ =A, and in particular thelinear implicationA(Bcan be defined by means of linear conjunction (thetensor product⊗) and negation:A(B= (A⊗B ⊥ ) ⊥ . However most reasonings need the duplication or the discarding of the hypothesis. The role of theexponential modality!Ais to provide this expressivity: we explicitly denote!Athe formulaAon which we want to perform such non-linear reasonings. The logic obtained from these connectives is calledmultiplicative and exponential linear logic(MELL). The general structure shared by the various models of MELL can be expressed synthetically with the language of category theory (see [Mel02] for a survey). Roughly, the linear fragment can be interpreted in a?-autonomous category (that is to say a category with a monoidal product⊗, a closure(and an idempotent dualityA ?? ' A), or in any other relaxed version of it, like a compact closed category (in which (A⊗B) ? 'A ? ⊗B ? so thatA(B'A ? ⊗B). The exponential modality needs to add the structure of acommutative comonoidon any objectA: we need a map!A→!A⊗!A in order to interpret the duplication of an hypothesis (corresponding to thecontracitno rule: from!A,!A, Γ`Bdeduce!A, Γ`B), and a map!A→1in order to interpret the discarding of an hypothesis (corresponding to theweakening rule: fromΓ`B deduce!A, Γ`B). In this paper we are interested in how to build the structure needed to interpret MELL. In particular we will focus on two constructions:

1. 2.

the free compact closure of a traced category [JSV96]; from a category with a feedback operator, it builds a compact closed category, thus suitable to interpret the linear fragment of MELL; thefreeexponentialformulaofMelli`es,Tabareau&Tasson[MTT09];presentedas a three steps construction, the solution of this formula freely generates a commuta- tive comonoid from any object.

The difficulty is to meet the requirements of this formula. Our construction enables to overcome it in the case of the free compact closure of sets and partial injections.

1. Free compact closure of a traced category.A trace operator is the categorical formalization of a feedback operator, like an iterator or a fixed point operator. To a mor- phismh:A⊗U→B⊗Uit associates a morphismtr U A,B (h) :A→B(fig. (a)). The Intconstruction generates a compact closed category from any symmetric monoidal categoryCtrace operator (a TSMC for short); it simulates insidewith a Cthe interac- tive behavior of programs exchanging questions and answers with their environment. Objects ofInt(C)are the pairs ofC-objects(A + , A − )whereA + represents “answers” andA − represents “questions”; a morphism from(A + , A − )to(B + , B − )inInt(C) is a morphismf:A + ⊗B − →B + ⊗A − inC. The composition with a morphism g:B + ⊗C − →C + ⊗B − is defined thanks to the trace operator (fig. (b)); the duality is then simply the symmetry(A + , A − ) ? = (A − , A + ).

B U

A

h

U

B

A (a) Trace operator

h

C + A −

g B + B − f A + C −

(b) Composition inInt(C)

An important example of TSMC isPInjthe category of sets and partial injections with the disjoint union]as monoidal product. The trace operator is defined by a graph union (withι, π, ρcanonical partial injections andf:A]U→B]U):

ι:A→A]U ∅ ] π: B B] ] U U → →A B ] rt U B U ,A (f) = G πf(ρf) n ι ρ=id U : n≥0 However the GoI of Girard [Gir89], traditionally presented as the interpretation of linear logic inInt(PInj)(see [AHS02] or appendix A), fails to provide a denotational model of exponentials.

2. Free exponential modality formula.The generic construction given in [MTT09] applied to a symmetric monoidal categoryCgoes through three steps.

First step:Acopointed object(B, v)is an objectBtogether withv:B→1. Co- pointed objects inCform a categoryC • where morphisms from(B, v)to(C, w) are the morphismsf:B→Cpreserving the copoints:w◦f=v. For the first step we assume that each objectAgenerates afree copointed object (A ⊥ , a);iewe assume that the forgetful functorU:C • →Chas a right adjoint. The elements ofA ⊥ represent1or0element ofA. In the case of the category of sets and relationsRel,1is the singleton and a setAgenerates the free copointed object given by the cartesian productA& 1and the right projection;