Paul-André Melliès

Ribbon Tensorial Logic

Keywords: CCS Concepts, Theory of computation → Linear logic, Categorical semantics, Control primitives, • Mathematics linear logic, tensorial logic, proof nets, proof structures, functorial knot theory, dialogue categories, ribbon categories

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

One fundamental insight of contemporary proof theory is that logical proofs π and counter-proofs π ′ behave in the same way as dynamic and interactive protocols exchanging information in the course of time. Depending on the paradigm chosen, the atomic tokens exchanged between a proof π and a counter-proof π ′ have received different names in the literature: they are called "particles" in the geometry of interaction, and "moves" in game semantics. The difference of terminology between "particles" and "moves" is not entirely innocuous: one basic intuition conveyed by the geometry of interaction [START_REF] Abramsky | Games and Full Completeness for Multiplicative Linear Logic[END_REF][START_REF] Girard | Towards a geometry of interaction[END_REF] and partly forgotten by game semantics is the fact that these elementary particles "circulate" inside the proof. Working in linear logic but using the traditional notations of classical logic for conjunction and disjunction, one can write as sequents

(a) A ∧ A * ⊢ false (b) true ⊢ A ∨ A *
the two basic principles (a) that a formula A and its negation A * cannot be true at the same time and (b) that a formula A or its negation A * is always true. Once transcribed in a categorical language, the sequents define two combinators

cut : A ∧ A * -→ false axiom : true -→ A ∨ A *
which may be interpreted as specific morphisms in a * -autonomous category. The basic idea of the geometry of interaction is that these two combinators cut and axiom implement input-output channels which may be drawn directly on the formulas as depicted below:

cut axiom input output input output A < A * A < A * cut axiom
The orientation of the arrows on these input-output channels indicates the direction in which the particle will cross the channel. Now, imagine that you wake up one morning in a world which has become "post-factual", and where the conjunction ∧ = ⊗ and the disjunction ∨ = have been identified to the same connective, noted ⊗. In this logical nightmare, and unhappy state of confusion, the two combinators cut and axiom have the following type

cut : A ⊗ A * -→ false axiom : true -→ A ⊗ A *
and they may be thus composed into a morphism true axiom / / A ⊗ A * cut / / false from true to false. The morphism should be seen as a fraudulent proof of the disjunctive unit ⊥ = false and thus as a logical inconsistency produced by cut-eliminating the proof π = axiom with the counter-proof π ′ = cut on the formula A ⊗ A * . As it turns out, when transcribed in the geometry of interaction, the composite morphism induces a loop consisting of two input-output channels:

A A * cut axiom (1)
A categorical account of proof structures The creation of such loops is a direct threat to the nice modularity of proofs, and of their underlying logical protocols. One key observation made by Girard is that no such loop is ever produced in linear logic during the cut-elimination of a proof π : A against a proof π ′ : A ⊸ B. This observation underlies the fundamental distinction between the two notions of proof structure and of proof net in linear logic. Recall from [START_REF] Girard | Linear logic[END_REF] that a proof structure of multiplicative linear logic is a "proof-like" structure constructed using the connectives ⊗ and of linear logic as well as the axiom and cut links. A proof net is then defined as a proof structure generated by a derivation tree π of linear logic. A typical instance of proof structure which is not a proof net (and thus does not represent any proof of linear logic) is the following one:

The starting point of the present paper is to recast in the language of categorical semantics the relationship between proof nets and proof structures in multiplicative linear logic. This categorical reformulation is very instructive and useful, in particular because it leads us to a very natural definition of "proof net" and of "proof structure" for commutative or ribbon tensorial logic.

Following Girard, we have just defined "proof nets" as specific "proof structures" generated by derivation trees π of multiplicative linear logic. However, it is customary today to replace the original definition of proof net by the following one, of a more conceptual flavour: a multiplicative proof net is a morphism of the free symmetric * -autonomous category * -autonomous(X ) generated by a given small category X . A typical choice for the category X is a discrete category (which may be seen as a set for that reason) whose objects define the atomic formulas of the logic. In order to understand the relationship between proof nets and proof structures, we suggest here to reformulate the notion of proof structure in a similar way. To that purpose, we consider the free compact closed category compact-closed(X ) generated by a given small category X . Recall that a compact closed category is a symmetric monoidal category, with unit noted I , where each object A comes equipped with an object A * and a pair of morphisms

cut : A * ⊗ A -→ I axiom : I -→ A ⊗ A *
making the diagrams below commute:

A ⊗ A * ⊗ A A A A⊗cut ax iom⊗A id A * A * A * ⊗ A ⊗ A * A * ⊗ax iom id cut ⊗A *
These two triangular diagrams are depicted in the language of string diagrams (see [START_REF] Selinger | A survey of graphical languages for monoidal categories[END_REF] for a nice introduction to string diagrams) as:

cut axiom = A A * A * A * A * cut axiom A A * A = A A
These data make the object A * a right dual of the object A, a situation written as A ⊣ A * . In a compact closed category C , the operation A → A * defines an equivalence of categories

(-) * : C op -→ C
between the original category C and its opposite category. As a matter of fact, a compact-closed category is the same thing as a * -autonomous category where the tensor product ⊗ and its opposite coincide up to symmetric monoidal equivalence. The construction of the free compact-closed category generated by X comes with a functor

X -→ compact-closed(X ).
By definition of the free * -autonomous category, and since the category compact-closed(X ) is * -autonomous, this functor can be lifted to a structure-preserving functor of * -autonomous categories

[-] : * -autonomous(X ) -→ compact-closed(X ) unique up to isomorphism, which makes the diagram below commute: * -autonomous(X ) compact-closed(X )

X [-]
atoms atoms This leads us to the following categorical definition of proof structure:

Definition 1 (proof structure). Given two formulas A,B of multiplicative linear logic with objects of X as atoms, a proof structure from A to B is defined as a morphism

Θ : [A] -→ [B]
in the free compact-closed category generated by the category X . Note that the formulas A and B are seen here as objects of the category * -autonomous(X ). By extension, a proof structure of a formula A of multiplicative linear logic is defined as a proof structure from the multiplicative unit 1 of linear logic to the formula A.

Consider for instance the case where the discrete category X contains exactly one object noted α, and where the formula A is defined as A = α. The functor [-] applied to a formula A of multiplicative linear logic replaces each linear conjunction ⊗ and linear disjunction of the formula A by a tensor product. The two formulas A ⊗ A * = α ⊗ α * and A A * = α α * are thus interpreted as the same object

[ α ⊗ α * ] = [ α α * ] = α ⊗ α *
According to our definition, the morphism

axiom : I → α ⊗ α *
of the category compact-closed(X ) depicted as α * axiom α defines a proof structure Θ of the formula α ⊗ α * . Quite obviously, this proof structure Θ should be identified with the proof structure depicted in the more traditional notation (2) used by Girard [START_REF] Girard | Linear logic[END_REF]. Note that the morphism axiom also defines a proof structure Θ ′ of the formula α α * . The key difference between the two proof structures Θ and Θ ′ is that the proof structure Θ ′ is the image

Θ ′ = [π ] : I -→ [α α * ]
of a proof net π : 1 → α α * living in the free * -autonomous category. This is not the case for the proof structure Θ.

A well-known limitation One well-known limitation of the theory of proof nets and of proof structures in multiplicative linear logic is that the proof structure Θ = [π ] associated to a proof net π does not characterize uniquely the proof net. Now that we have reformulated the notions of proof net and of proof structure in a categorical way, a simple and concise way to understand this limitation is to observe that the identity and symmetry morphisms id,symm : ⊥ ⊗ ⊥ -→ ⊥ ⊗ ⊥ do not coincide in general in a * -autonomous category. From this follows that the two derivation trees π 1 and π 2 below

π 1 = ⊢ 1, ⊥ axiom ⊢ 1, ⊥ ⊗-intro ⊢ 1, 1, ⊥ ⊗ ⊥ -intro ⊢ 1 1, ⊥ ⊗ ⊥ π 2 = ⊢ 1, ⊥ axiom ⊢ 1, ⊥ ⊗-intro ⊢ 1, 1, ⊥ ⊗ ⊥ exchange ⊢ 1, 1, ⊥ ⊗ ⊥ -intro ⊢ 1 1, ⊥ ⊗ ⊥
which only differ by the exchange rule which permutes the formulas 1 and 1 in the derivation tree π 2 , define different morphisms of the free * -autonomous category, and thus different proof nets π 1 and π 2 of multiplicative linear logic. However, their image [π 1 ] and [π 2 ] in the free compact closed category coincide. The reason is that the two objects 1 and ⊥ are transported by the functor [-] to the tensor unit I , and that the identity and symmetry morphisms id,symm : I ⊗ I -→ I ⊗ I coincide in any symmetric monoidal category, because the tensor unit I is a commutative monoid whose multiplication I ⊗ I → I is moreover invertible. This means that some fundamental information about the proof nets π 1 and π 2 has been lost when one translates them into the same proof structure Θ = [π 1 ] = [π 2 ]. Let us stress that this problem has nothing to do with our categorical formulation of proof nets and of proof structures: it is a problem inherent in linear logic, see [8-11, 19, 20] for discussion. As a matter of fact, this problem has haunted the theory of multiplicative proof nets since the notion was introduced by Girard. A slightly ad hoc solution has been formulated in the literature: the idea is to extend the original notion of proof structure with "jumps" connecting the disjunctive units ⊥ to other parts of the proof structure. Unfortunately, this solution requires to consider proof structures modulo an equational theory on "rewirings" originally formulated by Trimble. More recently, Heijtljes and Houston [START_REF] Heijltjes | No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete[END_REF] have established that the problem of proof net equivalence is PSPACE-complete, which means that unless P=PSPACE, it is unlikely that there exists an easy graph-theoretic solution to this problem.

The ongoing discussion on the imperfect correspondence between proof nets and proof structures may be summarized into the following purely categorical fact:

Annoying fact. The canonical functor [-] : * -autonomous(X ) → compact-closed(X )
which transports a proof net of multiplicative linear logic to its underlying proof structure, is not faithful.

Ribbon categories

The canonical functor [-] from proof nets to proof structures transports every derivation tree π to a set of links [π ] describing the flow of particles through the axiom and cut links of the proof. Unfortunately, we have just seen that the translation [-] is not faithful: two proofs π 1 and π 2 of the same formula A with the same proof structure Θ may very well be different. We will explain in a few paragraphs how to correct this uncomfortable situation by shifting from linear logic to tensorial logic, a more primitive logical framework where tensorial negation is not necessarily involutive. Before that, we would like to take advantage of a number of recent ideas coming from knot theory and representation theory in order to upgrade our current account of proof structures. What we are aiming at eventually is to "materialise" the set of links [π ] into a topological ribbon tangle reflecting the interactive behavior of the proof π .

To that purpose, we start from the notion of ribbon category which emerged at the interface of knot theory and of representation theory for quantum groups, see [START_REF] Kassel | Quantum groups[END_REF][START_REF] Shum | Tortile tensor categories[END_REF] for a detailed description. A ribbon category is defined as a monoidal category equipped with combinators for braiding and U-turns, satisfying a series of expected equations, see (Def. 7, §2.3) for a definition. The notion of ribbon category is supported by an elegant coherence theorem, which states that the free ribbon category on a category X has • as objects: sequences (A ϵ 1 1 , . . . ,A ϵ n n ) of signed objects of X where each A i is an object of the category X , and each ϵ i is either + or -, • as morphisms: oriented ribbon tangles considered modulo topological deformation, where every open strand is colored by a morphism of X , and every closed strand is colored by an equivalence class of morphisms of X , modulo the equality д • f ∼ f • д for every pair of morphisms of the form f : A → B and д : B → A.

So, a typical morphism from (A + ) to (B + ,C -,D + ) in the category ribbon(X ) looks like this

g f D + C - B + A +
where f : A -→ B and д : C -→ D are morphisms in the category X . Now, consider the full and faithful functor

X

-→ ribbon(X ) which transports every object A of X to the corresponding signed sequence (A + ). By construction, every functor from the category X to a ribbon category D lifts as a structure-preserving functor ⟨-⟩ which makes the diagram below commute:

ribbon(X ) D X ⟨-⟩

int er pr et at ion of links links

Once properly oriented and colored, every topological ribbon knot P defines a morphism P : I -→ I from the tensorial unit I = () to itself in the category ribbon(X ). Hence, its image ⟨P⟩ defines an invariant of the ribbon knot P modulo topological deformation. This functorial method enables for instance to establish that the Jones polynomial ⟨P⟩ associated to a ribbon knot P defines a topological invariant, see [START_REF] Kassel | Quantum groups[END_REF] for details. This kind of topological invariant is quite useful. By way of illustration, the non trivial fact that the left trefoil K L and the right trefoil K R depicted below

K L = K R =
are not the same knot modulo deformation, is easily proved by computing their Jones polynomials, and by observing that they are different:

⟨K L ⟩ = 2 x 2 + 1 x 4 + y 2 x 2 ⟨K R ⟩ = 2x 2 -x 4 + x 2 y 2
An important point is that these topological diagrams can be drawn in ribbon categories precisely because the conjunctive tensor product ⊗ and the disjunctive tensor product coincide there. Seen from that operational point of view, the topological ribbon tangles like K L and K R are nothing but a sophisticated instance of logical inconsistency, producing a deadlock or a livelock loop (1) in the protocol.

Balanced dialogue categories In order to connect proof theory and knot theory, we find convenient to start from a braided notion of dialogue category. The notion of dialogue category has been already used by the author [START_REF] Melliès | Game semantics in string diagrams[END_REF] in order to reflect the dialogical interpretations of proofs as interactive strategies. A dialogue category is defined as a monoidal category equipped with a primitive notion of duality.

Definition 2 (Dialogue categories).

A dialogue category is a monoidal category C equipped with an object ⊥ together with two functors

x → (x ⊸ ⊥) : C op -→ C x → (⊥ x ) : C op -→ C
and two families of isomorphisms

φ x,y : C (x ⊗ y, ⊥) C (y,x ⊸ ⊥) ψ x,y : C (x ⊗ y, ⊥) C (x, ⊥ y)
natural in x and y.

A balanced dialogue category is then defined (Def. 8) as a dialogue category whose underlying monoidal category C is balanced in the sense of Joyal and Street [START_REF] Joyal | The geometry of tensor calculus[END_REF][START_REF] Joyal | Braided tensor categories[END_REF]. This means that the category C is equipped with a braiding and a twist, and that it satisfies a series of coherence diagrams reflecting topological equalities of ribbon tangles. Interestingly, no additional coherence property is required between the dialogue structure and the balanced structure.

The proof-theoretic nature of balanced dialogue categories is witnessed by the fact that they come together with an internal logic: a braided and twisted variant of tensorial logic which we call ribbon tensorial logic. The logic is formulated in §3 in the traditional style of proof theory, that is, as a sequent calculus whose derivation trees are identified modulo a notion of proof equality. Just as for linear logic and * -autonomous categories, one establishes that the free balanced dialogue category generated by a category X has

• objects: the formulas of ribbon tensorial logic (constructed with the binary tensor product ⊗ and its unit I = 1 together with the left negation A → A ⊸ ⊥ and the right negation A → ⊥ A) with atoms provided by the objects of the category X , • morphisms from A to B: the derivation trees π of the sequent A ⊢ B in ribbon tensorial logic, modulo the equational theory of the logic.

The proof-as-tangle theorem Once the proof-theoretic nature of balanced dialogue categories is firmly established, all is left to do is to relate them to topology. This is achieved by a simple but fundamental observation. A pointed category (C , ⊥) is defined as a category C equipped with an object ⊥ singled out in the category.

A pointed category may be alternatively defined as an S-algebra for the monad S : Cat → Cat which transports every category X to the category X + 1 defined as the disjoint sum of X with the terminal category 1. The unique object of 1 is noted ⊥ and provides the singled-out object of the pointed category (X + 1, ⊥).

Every category X induces a free ribbon category ribbon(X + 1) generated by the category X + 1. The category ribbon(X + 1) is monoidal and balanced by construction. The key observation is that it is also a dialogue category where the left and right negation functors are defined as

x ⊸ ⊥ def = x * ⊗ ⊥ ⊥ x def = ⊥ ⊗ x * .
Note that the resulting balanced dialogue category is somewhat degenerate, since the canonical morphism

(⊥ (x ⊸ ⊥)) ⊗ y -→ ⊥ ((x ⊗ y) ⊸ ⊥)
which defines the strength of the double negation monad, is an isomorphism. Now, the unit of the monad S instantiated at the category X inc :

X -→ X + 1 induces a functor X -→ X + 1 -→ ribbon(X + 1)
from X to the balanced dialogue category ribbon(X + 1). From this, it follows that there exists a structure-preserving functor of balanced dialogue categories

[-] : balanced-dialogue(X ) -→ ribbon(X + 1)

which makes the diagram below commute:

balanced-dialogue(X ) ribbon(X + 1)

X X + 1 [-] inc
The functor [-] transports:

• the formulas of ribbon tensorial logic into signed sequences of ⊥ ' s and of logical atoms provided by the objects of the underlying category X , • the proofs of ribbon tensorial logic modulo proof equality into ribbon tangles modulo topological deformation.

Definition 3 (Proof nets).

A tensorial proof net π of ribbon tensorial logic is defined as a morphism of the free balanced dialogue category.

Definition 4 (Proof structures). A tensorial proof structure of ribbon tensorial logic from a formula A to a formula B is a morphism

Θ : [A] → [B]
of the free ribbon category.

We establish in §4 the following "proof-as-tangle" theorem:

Theorem. The functor [-] which transports tensorial proof nets to tensorial proof structures, is faithful.

This theorem is important because it enables one to identify every derivation tree π of ribbon tensorial logic modulo commuting conversions, with the underlying ribbon tangle [π ] modulo topological deformation. The ribbon tangle [π ] : [A] → [B] should be understood as a topological "materialisation" of the dialogical interpretation of the proof π : A → B as an innocent strategy between the dialogue games A and B: each strand of the tangle [π ] describes a specific pair of Opponent and Player moves played by the innocent strategy associated to the tensorial proof π . In this way, the proof-as-tangle theorem provides a topological and type-theoretic foundation to game semantics. In particular, it should be mentioned that the theorem still holds when one removes the topology of ribbon tangles, and replaces ribbon tensorial logic by commutative tensorial logic, balanced dialogue categories by symmetric dialogue categories, and ribbon categories by compact-closed categories.

Theorem. The canonical functor

[-] : symmetric-dialogue(X ) -→ compact-closed(X + 1)
which transports tensorial proof nets to tensorial proof structures in commutative tensorial logic, is faithful. Here, we use the notation symmetric-dialogue(X ) to denote the free symmetric dialogue category generated by X .

This means that in ribbon tensorial logic as well as in commutative tensorial logic, a derivation tree π is entirely characterized by its proof structure [π ]. The proof-as-tangle theorem resolves in this way the old and annoying problem of the theory of proof nets of linear logic discussed earlier in the introduction. It also connects proof theory and knot theory by providing a topological coherence theorem for balanced (or symmetric) dialogue categories.

Plan of the paper We start by introducing in §2 the notion of balanced dialogue category. We formulate in §3 the corresponding ribbon tensorial logic, whose proofs are designed to be interpreted in balanced dialogue categories. The proof-as-tangle theorem for ribbon tensorial logic is stated and established in §4. We finally illustrate in §5 how to use the proof-as-tangle theorem as a coherence theorem.

Related works

We would like to mention the early work by Arnaud Fleury [START_REF] Fleury | Ribbon braided multiplicative linear logic[END_REF] who considered a sequent calculus for a braided version of linear logic which is very similar to our sequent calculus for ribbon tensorial logic. Besides the connection already mentioned to the theory of multiplicative proof nets in linear logic [8-11, 19, 20], our interpretation of ribbon tensorial proofs as ribbon tangles induces an interpretation of these proofs as sums of planar diagrams in Temperley-Lieb algebras, whose relationship to [START_REF] Abramsky | Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics[END_REF] deserves to be clarified.

Balanced dialogue categories

We introduce the notion of balanced dialogue category. To that purpose, we start by recalling the definition of braided monoidal category in § 2.1, of balanced monoidal category in § 2.2 and of ribbon category in § 2.3. We finally formulate our notion of balanced dialogue category in § 2.4.

Braided monoidal categories

In order to fix notations, we recall that a monoidal category C is a category equipped with a functor ⊗ : C × C → C and an object I and three natural isomorphisms

α A,B,C : (A ⊗ B) ⊗ C -→ A ⊗ (B ⊗ C) λ A : I ⊗ A -→ A ρ A : A ⊗ I -→ A making the two coherence diagrams below commute. (A ⊗ B) ⊗ (C ⊗ D ) ((A ⊗ B) ⊗ C ) ⊗ D A ⊗ (B ⊗ (C ⊗ D )) (A ⊗ (B ⊗ C )) ⊗ D A ⊗ ((B ⊗ C ) ⊗ D ) α α α ⊗D α A⊗α (A ⊗ I ) ⊗ B A ⊗ (I ⊗ B) A ⊗ B α ρ ⊗B A⊗λ Definition 5 (braiding). A braiding in a monoidal category C is a family of isomorphisms σ A,B : A ⊗ B -→ B ⊗ A
natural in x and y such that the two diagrams

A ⊗ (B ⊗ C ) (B ⊗ C ) ⊗ A (A ⊗ B) ⊗ C (a) B ⊗ (C ⊗ A) (B ⊗ A) ⊗ C B ⊗ (A ⊗ C ) σ α α σ ⊗C α B ⊗σ (A ⊗ B) ⊗ C C ⊗ (A ⊗ B) A ⊗ (B ⊗ C ) (b ) (C ⊗ A) ⊗ B A ⊗ (C ⊗ B) (A ⊗ C ) ⊗ B σ α -1 α -1 A⊗σ α -1 σ ⊗B
commute. The braiding map σ A,B is depicted in string diagrams as a positive braiding of the ribbon strands A and B where its inverse is depicted as the negative braiding:

σ A,B = A B A B σ -1 A,B = A B A B
The two coherence diagrams (a) and (b) are then depicted as topological equalities between string diagrams: The twist θ A is depicted as the ribbon A twisted positively in the trigonometric direction with an angle 2π whereas its inverse θ -1 A is depicted as the same ribbon A twisted negatively this time, with an angle -2π :

A B C A B C (a) = A B C A B C A B C A B C (b ) = A B C A B C

Balanced categories Definition 6 (balanced category). A balanced category C is a braided monoidal category equipped with a family of morphisms

A ⊗ B B ⊗ A A ⊗ B B ⊗ A σ A,B θ A⊗B θ B ⊗θ A σ B,A (3)
θ A = A A θ -1 A = A A
This notation enables us to give a topological motivation to the axioms of a balanced category. The first requirement that θ I is the identity means that the ribbon strand I should be intuitively thought as "ultra thin". The second requirement that the coherence diagram (3) commutes reflects the following topological equality between string diagrams:

θ A ⊗B = A B A B

Ribbon categories

This leads us to the definition of ribbon category, a well-established concept [START_REF] Kassel | Quantum groups[END_REF][START_REF] Shum | Tortile tensor categories[END_REF] in the representation theory of quantum groups, and in low-dimensional topology:

Definition 7 (ribbon category). A ribbon category C is a balanced category where every object A has a right dual A * , a situation written as A ⊣ A * . See the introduction for a definition of right dual.

Balanced dialogue categories

At this stage, we are ready to introduce the notion of balanced dialogue category which provides a functorial bridge between proof theory and the topology of knots.

Definition 8 (balanced dialogue categories).

A balanced dialogue category is a dialogue category C in the sense of Def. 2, moreover equipped with a braiding and a twist defining a balanced category.

An interesting aspect of the definition is that it does not require any coherence relation between the dialogue structure and balanced structure of the category C .

Illustration. An instructive example of balanced dialogue category D coming from algebra, and more specifically from the representation theory of quantum groups, is the following one: the category Mod(H ) of (finite and infinite dimensional) H -modules associated to a ribbon Hopf algebra H . Note that the full subcategory C of rigid objects A in a balanced dialogue category D (that is, objects with a right dual) is a ribbon category. Typically, the category Mod f (H ) of finite dimensional H -modules associated to a ribbon Hopf algebra H defines a ribbon category, see [START_REF] Kassel | Quantum groups[END_REF] for details.

Ribbon tensorial logic

We introduce below the sequent calculus of ribbon tensorial logic, and mention a number of commuting conversions involved in the cut-elimination procedure.

The ribbon groups

Recall that the braid group B n on n strands is presented by the generators σ i for 1 ≤ i ≤ n -1 and the equations

σ i • σ i+1 • σ i = σ i+1 • σ i • σ i+1 σ i • σ j = σ j • σ i when |j -i | ≥ 2. ( 4
)
There is an obvious left action

▷ : B n × [n] -→ [n] (5)
σ i • θ i = θ i+1 • σ i σ i • θ i+1 = θ i • σ i σ i • θ j = θ j • σ i when j < i or when j ≥ i + 2.
Each group G n may be alternatively seen as a groupoid noted S G n , with a unique object * and S G n ( * , * ) = G n . A nice and conceptual definition of the ribbon groups G n is possible, as follows.

The groupoid G defined as the disjoint sum of the groupoids S G n coincides with the free balanced category generated by the terminal category 1. Recall that the category 1 has a unique object * and a unique map. Hence, the group G n may be alternatively defined as G (n,n) where n = 1 ⊗ • • • ⊗ 1 is the n-fold tensor product of the generator 1 of the category G . The fact that the free balanced category G generated by the category 1 coincides with the disjoint sum of the groupoids S G n is just the ribbon-theoretic counterpart to the well-known fact that the free braided monoidal category B generated by the category 1 coincides with the disjoint sum of the groupoids S B n . From this observation follows that there exists a family of group homomorphisms

⊗ : G p × G q -→ G p+q
which reflects the monoidal structure of the balanced category G . Moreover, the action (5) extends to a left action

▷ : G n × [n] -→ [n]
where each generator θ i acts trivially on [n] = {1, . . . ,n}, in the sense that

θ i ▷ k = k for all k ∈ [n].

The sequent calculus

The formulas of ribbon tensorial logic are finite trees generated by the grammar

A,B ::= A ⊗ B | 1 | A ⊸ ⊥ | ⊥ A | ⊥ | α
where α is an object of a fixed small category X of atoms. The sequents are two-sided

A 1 , . . . ,A m ⊢ B
with a sequence of formulas A 1 , ...,A m on the left-hand side, and a unique formula B on the right-hand side. The proofs of ribbon

Axiom f : α → β in the category X α β Cut Γ A Υ 1 , A, Υ 2 B Υ 1 , Γ, Υ 2 B Right ⊗-introduction Γ A ∆ B Γ, ∆ A ⊗ B Left ⊗-introduction Υ 1 , A, B, Υ 2 C Υ 1 , A ⊗ B, Υ 2 C Right 1-introduction 1 Left 1-introduction Υ 1 , Υ 2 A Υ 1 , 1, Υ 2 A Right (⊥ )-introduction Γ, A ⊥ Γ ⊥ A Left (⊥ )-introduction Γ A ⊥ A, Γ ⊥ Right ( ⊥)-introduction A, Γ ⊥ Γ A ⊥ Left ( ⊥)-introduction Γ A Γ, A ⊥ ⊥ Figure 1. Sequent calculus of tensorial logic.
tensorial logic are defined as derivation trees in a carefully designed sequent calculus, which we formulate now. The sequent calculus is defined as the sequent calculus of tensorial logic in its most basic (and non-commutative) form [START_REF] Melliès | Une étude micrologique de la négation[END_REF], recalled in Figure 1, together with a family of exchange rules A 1 , . .

. ,A n ⊢ B [д ]

A д▷1 , . . . ,A д▷n ⊢ B parametrized by the elements д of the ribbon group G n .

The commutative conversions

Ribbon tensorial logic is inspired by the topology of knots, and one thus needs to take extra care in order to design the equational theory on its derivation trees. Nonetheless, the basic recipe to identify two derivation trees π 1 and π 2 is the same in ribbon tensorial logic as in any other sequent calculus: the equality is defined by a series of local commuting conversions π 1 ↭ π 2 on derivation trees. Moreover, these commuting conversions rules are essentially the same for ribbon tensorial logic as for traditional (commutative) tensorial logic. The only difference is that every exchange rule of ribbon tensorial logic is labelled by an element д ∈ G n of the ribbon group. For that reason, one needs to treat with an extreme attention every commuting conversion π 1 ↭ π 2 involving an exchange rule. For each such commuting conversion, the challenge is to label properly the exchange rules appearing on each side π 1 and π 2 of the conversion in commutative tensorial logic, in order for the conversion π 1 ↭ π 2 to make sense in ribbon tensorial logic. The archetypal illustration of commuting conversion in ribbon tensorial logic is provided by the conversion which transforms the derivation tree

π 1 . . . A 1 , . . . , An ⊢ A π 2 . . . ϒ 1 , B, A, ϒ 2 ⊢ C [p ⊗ σ ⊗ q ] ϒ 1 , A, B, ϒ 2 ⊢ C Cut ϒ 1 , A 1 , . . . , An, B, ϒ 2 ⊢ C into the derivation tree π 1 . . . A 1 , . . . , An ⊢ A π 2 . . . ϒ 1 , B, A, ϒ 2 ⊢ C Cut ϒ 1 , B, A 1 , . . . , An, ϒ 2 ⊢ C [p ⊗ σ n,1 ⊗ q ] ϒ 1 , A 1 , . . . , An, B, ϒ 2 ⊢ C
where p and q are the respective lengths of ϒ 1 and of ϒ 2 and where σ m,n is defined as the positive braid permuting m strands above n strands. Another important illustration is the conversion which transforms the derivation tree

π 1 . . . A 1 , . . . , An ⊢ A π 2 . . . ϒ 1 , A, ϒ 2 ⊢ C [p ⊗ θ ⊗ q ] ϒ 1 , A, ϒ 2 ⊢ C Cut ϒ 1 , A 1 , . . . , An, ϒ 2 ⊢ C into the derivation tree π 1 . . . A 1 , . . . , An ⊢ A π 2 . . . ϒ 1 , A, ϒ 2 ⊢ C Cut ϒ 1 , A 1 , . . . , An, ϒ 2 ⊢ C [p ⊗ θ ⟨n⟩ ⊗ q ] ϒ 1 , A 1 , . . . , An, ϒ 2 ⊢ C
where θ ⟨n⟩ is the positive twist on n strands. These two commutative conversions should be understood as naturality conditions on the braiding σ and on the twist θ . Yet another important commuting conversion identifies for every pair д,h ∈ G n the derivation tree

π . . . A 1 , . . . , An ⊢ B [h ] A h▷1 , . . . , A h▷n ⊢ B [д ] A д▷(h▷1) , . . . , A д▷(h▷n) ⊢ B
with the derivation tree

π . . . A 1 , . . . , An ⊢ B [д • h ] A д•h▷1 , . . . , A д•h▷n ⊢ B
This commuting conversion comes with a similar conversion for the unit element e ∈ G n . Together, the two commuting conversions ensure that the action of the ribbon group G n on a sequent A 1 , . . . ,A n ⊢ B with n hypothesis is algebraic in the traditional sense, modulo conversion.

One main technical observation of the paper is that the traditional coherence diagrams which define a braiding (in §2.1) and a twist (in §2.2) can be "internalized" as commuting conversions of ribbon tensorial logic. Typically, the coherence diagram (a) for braiding (Def. 5, §2.1) is reflected in ribbon tensorial logic by the commuting conversion which identifies the derivation tree

π . . . ϒ 1 , A, B, C, ϒ 2 ⊢ D Left ⊗ ϒ 1 , A ⊗ B, C, ϒ 2 ⊢ D [p ⊗ σ ⊗ q ] ϒ 1 , C, A ⊗ B, ϒ 2 ⊢ D
with the derivation tree π . . .

ϒ 1 , A, B, C, ϒ 2 ⊢ D [p ⊗ 1 ⊗ σ ⊗ q ] ϒ 1 , A, C, B, ϒ 2 ⊢ D [p ⊗ σ ⊗ 1 ⊗ q ] ϒ 1 , C, A, B, ϒ 2 ⊢ D Left ⊗ ϒ 1 , C, A ⊗ B, ϒ 2 ⊢ D
Similarly, the coherence diagram (3) for the twist in the definition of a balanced category (Def. 6, §2.2) is reflected by the commuting conversion which identifies the derivation tree π . . .

ϒ 1 , A, B, ϒ 2 ⊢ C Left ⊗ ϒ 1 , A ⊗ B, ϒ 2 ⊢ C [p ⊗ θ ⊗ q ] ϒ 1 , A ⊗ B, ϒ 2 ⊢ C
with the derivation tree π . . .

ϒ 1 , A, B, ϒ 2 ⊢ C [p ⊗ σ ⊗ q ] ϒ 1 , B, A, ϒ 2 ⊢ C [p ⊗ θ ⊗ θ ⊗ q ] ϒ 1 , B, A, ϒ 2 ⊢ C [p ⊗ σ ⊗ q ] ϒ 1 , A, B, ϒ 2 ⊢ C Left ⊗ ϒ 1 , A ⊗ B, ϒ 2 ⊢ C
The fact that the coherence diagrams required of a balanced category can be "lifted" in this way to ribbon tensorial logic is somewhat surprising, because it means that the topological notions of braiding σ and of twist θ are compatible with the logical and multicategorical (rather than categorical) nature of sequents

A 1 , • • • ,A n ⊢ B of tensorial logic.

The cut elimination theorem

The equational theory of ribbon tensorial logic is thus obtained from the equational theory of traditional (commutative) tensorial logic by selecting very carefully the label д ∈ G n associated for each conversion rule π 1 ↭ π 2 and for each exchange rule appearing in the derivation trees π 1 and of π 2 . Once these choices of labelling have been done properly, it is not difficult to establish the following cut-elimination theorem, in just the same way as for commutative tensorial logic: Theorem 1 (Cut-elimination). Every derivation tree of ribbon tensorial logic is equivalent to a cut-free derivation tree modulo commuting conversions.

A focusing theorem

The commuting conversions of ribbon tensorial logic are not only useful to prove the cut-elimination theorem. They also enable us to establish a focusing theorem for the derivation trees of the logic. The theorem is important because it ensures that every cut-free derivation tree π can be transformed by a series of commuting conversions to a normal form π nf where the construction of the derivation is performed in phases. A cycle of construction starts with a number of derivation trees π 1 . . .

Γ 1 ⊢ A 1 • • • π i . . . Γ i ⊢ A i • • • π n . . . Γ n ⊢ A n
where all the formulas of the context Γ i are either atomic: that is, equal to an object α of the category X , or negated: that is, of the form A ⊸ ⊥ or ⊥ A. One then applies the phases below one after the other in order to get a derivation tree π of the same form, whose sequent Γ ⊢ A has all the formulas of its context Γ either atomic or negated.

1. A left introduction rule of the left negation or of the right negation which produces a sequent whose conclusion formula is ⊥, 2. A series of exchange rules which permute the formulas of the context, 3. A series of left ⊗-introduction and of left 1-introduction rules, which produces a sequent where at most one formula in the context is not negated or atomic, 4. A right introduction of the left negation or of the right negation, or an axiom rule, which produces a sequent where all the formulas (context and conclusion) are either negated or atomic, 5. A series of right ⊗-introduction rules, and of right 1-introduction rules, 6. A series of exchange rules which permute the atomic or negated formulas of the context, As just claimed, one obtains at the end of each cycle a sequent Γ ⊢ A where all the formulas of the context Γ are either negated or atomic. A derivation tree π is called focused when it has been produced by a number of such construction cycles.

Theorem 2 (Focusing). Every derivation tree π is equivalent to a focused derivation tree π nf modulo the commuting conversions of ribbon tensorial logic.

The theorem is based on the ability of permuting the order of introduction rules using commuting conversions. The proof is essentially standard, except for the special care required by the exchange rules.

Soundness theorem

Suppose given a functor X -→ D from the category of atoms of our ribbon tensorial logic, to a given balanced dialogue category D. Then, one establishes that Theorem 3 (Soundness). Every derivation tree π of a sequent

A 1 ⊗ • • • ⊗ A n ⊢ B
in ribbon tensorial logic may be interpreted as a morphism

The proof-as-tangle theorem

A more conceptual and sophisticated way to formulate the soundness theorem (Thm. 3, §3.6) is to state that the free balanced dialogue category dialogue(X ) generated by the category X of atoms, coincides with a category of tensorial formulas and of derivation trees modulo the equational theory of ribbon tensorial logic. We have seen in the introduction how to deduce from this property a functor [-] : dialogue(X ) -→ ribbon(X + 1) which transports every tensorial proof net π into a topological tangle [π ]. We establish now the main result of the paper.

Theorem 4 (Proof-as-tangle). The functor [-] is faithful.

Proof. The proof is to a large extent based on the focusing theorem (Thm. 2). Suppose that two cut-free derivation trees

π 1 . . . A ⊢ B π 2 . . . A ⊢ B (6)
of ribbon logic induce the same tangle [π 1 ] = [π 2 ] modulo topological deformation in the free ribbon category ribbon(X + 1). We show that π 1 ↭ π 2 and conclude. We proceed by induction on the number of strands in the tangle. By the focusing theorem, we know that the proofs π 1 and π 2 are equal modulo logical equality to:

π ′ 1 . . . A 1 , . . . , An ⊢ B π ′ 2 . . . A 1 , . . . , An ⊢ B
where each A i is either a negation or an atom, followed by the same sequence of left introduction of tensor and left introduction of unit. Suppose that B = ⊥. In that case, the formula ⊥ was either introduced by:

• the left introduction of a left negation X ⊸ ⊥,

• or the left introduction of a right negation ⊥ X .

By symmetry, we may suppose without loss of generality that this last rule introduces a left negation X ⊸ ⊥ in the context. In that case, the proof π ′ 1 is equal to

π ′′ 1 . . . X 1 , . . . , X n-1 ⊢ X Left ⊸ X 1 , . . . , X n-1 , X ⊸ ⊥ ⊢ ⊥ [д ] A 1 , . . . , An ⊢ ⊥
The equality of [π 1 ] and [π 2 ] modulo deformation implies that ⊥ is connected in [π ′ 2 ] to the same formula X ⊸ ⊥. From that follows that X ⊸ ⊥ is also introduced in π 2 by the left introduction of a left negation. In other words, the proof π ′ 2 factors as

π ′′ 2 . . . Y 1 , . . . , Y n-1 ⊢ Y Left ⊸ Y 1 , . . . , Y n-1 , X ⊸ ⊥ ⊢ ⊥ [h ] A 1 , . . . , An ⊢ ⊥
From this, we conclude that the derivation tree

π ′′ 1 . . . X 1 , . . . , X n-1 ⊢ X Left ⊸ X 1 , . . . , X n-1 , X ⊸ ⊥ ⊢ ⊥
induces the same topological tangle as the derivation tree

π ′′ 2 . . . Y 1 , . . . , Y n-1 ⊢ Y Left ⊸ Y 1 , . . . , Y n-1 , X ⊸ ⊥ ⊢ ⊥ [h ] A 1 , . . . , An ⊢ ⊥ [д -1 ] X 1 , . . . , X n-1 , X ⊸ ⊥ ⊢ ⊥
Since all the formulas A i are either negated formulas or atoms, we deduce from the topology of tangles that

д -1 • h ∈ G n is of the form f ⊗ 1. From this follows that the proof π ′′ 1 . . . X 1 , . . . , X n-1 ⊢ X
has the same topological tangle as the proof

π ′′ 2 . . . Y 1 , . . . , Y n-1 ⊢ X [f ] X 1 , . . . , X n-1 ⊢ X
From this, we deduce by induction hypothesis that they are equal proofs, in the sense that their proof nets coincide. The proof π ′ 1 is thus equal to the proof

π ′′ 2 . . . Y 1 , . . . , Y n-1 ⊢ X [f ] X 1 , . . . , X n-1 ⊢ X Left ⊸ X 1 , . . . , X n-1 , X ⊸ ⊥ ⊢ ⊥ [д ] A 1 , . . . , An ⊢ ⊥
which may be rewritten into

π ′′ 2 . . . Y 1 , . . . , Y n-1 ⊢ X Left ⊸ Y 1 , . . . , Y n-1 , X ⊸ ⊥ ⊢ ⊥ [f ⊗ 1] X 1 , . . . , X n-1 , X ⊸ ⊥ ⊢ ⊥ [д ] A 1 , . . . , An ⊢ ⊥
which may be then rewritten into the proof π 2 :

π ′′ 2 . . . Y 1 , . . . , Y n-1 ⊢ X Left ⊸ Y 1 , . . . , Y n-1 , X ⊸ ⊥ ⊢ ⊥ [h ] A 1 , . . . , An ⊢ ⊥
This concludes the proof by induction when the conclusion B of the two sequents π 1 and π 2 is equal to the formula B = ⊥. □

We have seen the most difficult part of the topological argument establishing the "proof-as-tangle" theorem. The remaining part of the argument works in essentially the same way. For instance, suppose that the conclusion of the sequent

A 1 , • • • ,A n ⊢ B
produced by the two derivations trees π 1 and π 2 in ( 6) is the tensor formula B = B 1 ⊗ B 2 , and that all the hypothesis A 1 , . . . ,A n are either negated or atomic. In that case, one may suppose without loss of generality that the last rule of π 1 introduces a tensor on the right. The derivation tree π 1 thus factors as

π 11 . . . A 1 , . . . , A k ⊢ B 1 π 12 . . . A k +1 , . . . , A n ⊢ B 2 Right ⊗ A 1 , . . . , A k , A k +1 , . . . , A n ⊢ B 1 ⊗ B 2
The fact that the tangles [π 1 ] and[π 2 ] are equal modulo deformation implies that π 2 splits in the same way as two proofs π 21 and π 22 ; moreover, the tangles [π 11 ] and [π 21 ] are equal modulo deformation, and similarly for [π 12 ] and [π 22 ]. This enables one to conclude by induction that π 11 and π 21 are equal modulo commuting conversions, and similarly for π 12 and π 22 . This concludes our argument that π 1 and π 2 are equal modulo commuting conversions.

Illustration

The proof-as-tangle theorem (Thm. 4, §4) is not just meaningful for proof-theory: it also provides a useful coherence theorem for balanced dialogue categories, such as the category Mod(H ) of finite and infinite dimensional H -modules associated to a ribbon Hopf algebra H , mentioned in §2.4. By way of illustration, imagine that one wants to establish that the diagram

⊥ (⊥ A) ⊥ (A ⊸ ⊥) (⊥ A) ⊸ ⊥ A ⊥ (A ⊸ ⊥) ⊥ turn A turn ⊥ A η ′ A η A θ ⊥ (A ⊸⊥) (7)
commutes in every balanced dialogue category D, where

η A : A → ⊥ (A ⊸ ⊥) η ′ A : A → (⊥ A) ⊸ ⊥ turn A : ⊥ A → A ⊸ ⊥
denote the units η,η ′ of the two double negation monads, and the canonical isomorphism turn A between the left and right negation of A. Commutativity of [START_REF] Girard | Geometry of interaction II : deadlock-free algorithms[END_REF] in any balanced dialogue category is equivalent to the fact that the following derivation trees π 1 and π 2 of ribbon tensorial logic are equal modulo commuting conversions:

Axiom A ⊢ A Left ⊸ A , A ⊸ ⊥ ⊢ ⊥ [torsion] A , A ⊸ ⊥ ⊢ ⊥ Right A ⊢ ⊥ (A ⊸ ⊥) Axiom A ⊢ A Left ⊥ A , A ⊢ ⊥ Right ⊸ A ⊢ (⊥ A) ⊸ ⊥ Axiom A ⊢ A Left ⊸ A , A ⊸ ⊥ ⊢ ⊥ [σ • θ 1 ] A ⊸ ⊥ , A ⊢ ⊥ Right A ⊸ ⊥ ⊢ ⊥ A Left ⊸ A ⊸ ⊥ , (⊥ A) ⊸ ⊥ ⊢ ⊥ [σ • θ 1 ] (⊥ A) ⊸ ⊥ , A ⊸ ⊥ ⊢ ⊥ Right (⊥ A) ⊸ ⊥ ⊢ ⊥ (A ⊸ ⊥) Cut A ⊢ ⊥ (A ⊸ ⊥)
where the element torsion = θ ⟨2⟩ of G 2 twists the two hypothesis of the proof, or (equivalently) twists the conclusion ⊥ with an angle 2π , see §3.3 for a definition of θ ⟨n⟩. One convenient way to construct the ribbon tangles [π 1 ] and [π 2 ] associated to the derivation trees π 1 and π 2 is to proceed by structural induction, and to interpret every derivation tree π of a sequent A 1 , . . . ,A n ⊢ B as a form [π ] on the object [A 1 ]⊗ . . . ⊗[A n ]⊗[B] * in the category ribbon(X +1). Recall that a form on an object A in a ribbon category C , is defined as a morphism from A to the tensorial unit I . If we use the notation ℏ = ⊥ for the tensorial pole object of ribbon(X + 1) and h = ⊥ * for its right dual, we can then describe [π 1 ] and [π 2 ] as a sequence of local transformations performed on forms. When we apply this recipe to [π 1 ], we obtain the following sequence of local transformations [START_REF] Melliès | Une étude micrologique de la négation[END_REF] for details. In the ribbon tangle [π 1 ], the dark black strand tracks the circulation of ℏ = ⊥ inside the proof while the light blue strands tracks the circulation of the formula A. The ribbon tangle [π 2 ] associated to the derivation tree π 2 is computed by the same procedure and depicted on top of the derivation tree π 2 , in the following way:

1 1
It is not difficult to see by "pulling the strings" that the two ribbon tangles [π 1 ] and [π 2 ] are equal modulo topological deformation. This implies (by Thm. 4) that the two derivation trees π 1 and π 2 are equal modulo commuting conversions. This establishes the nontrivial fact that the diagram ( 7) is commutative in every balanced dialogue category. The example illustrates in what sense the proofs of ribbon tensorial logic are of a topological nature. The translation into ribbon tangles may be also seen as a topologically-aware refinement of game semantics where the interactive strategies interpreting tensorial proofs are refined into ribbon tangles.

θ

  A : A -→ A natural in A, satisfying the equality θ I = id I where I is the monoidal unit, and making the diagram

LICS ' 18 ,

 18 July 9-12, 2018, Oxford, United Kingdom Paul-André Melliès commute for all objects A and B of the category C .

  [π ] :A 1 ⊗ • • • ⊗ A n -→ Bof the balanced dialogue category D. Moreover, the interpretation [π ] provides an invariant of the derivation tree π modulo commuting conversions.The interpretation [π ] of the derivation tree π is defined by structural induction on the height of the derivation tree. The only interesting point of the construction is that the exchange ruleA 1 , . . . ,A n ⊢ B [д ] A д▷1 , . . . ,A д▷n ⊢ B is interpreted by precomposing the interpretation [π ] : A 1 ⊗ . . . ⊗ A n -→ B of the proof π with the morphism A д▷1 ⊗ . . . ⊗ A д▷n -→ A 1 ⊗ . . . ⊗ A nassociated to the element д ∈ G n of the ribbon group acting on the object A 1 ⊗ . . . ⊗ A n in the balanced dialogue category D.

  AxiomA ,A * Left ⊸ A , A * ⊗ ℏ , h [torsion] A , A * ⊗ ℏ , h Right A , A * ⊗ ℏ ⊗ hdefining the topological tangle depicted below: torsion This intermediate representation enables us to compute the associated ribbon tangle [π 1 ] by a step-by-step procedure, as done in the right-hand side figure above, see Chap. 7 of

  of the group B n on the set [n] = {1, • • • ,n} of strands, induced by the group homorphism B n → S n to the symmetry group S n on n elements. This action enables one to define a wreath product of B n on the additive group (Z, +, 0). The resulting group G n is called the ribbon group on n strands. The group is presented by the generators σ

i for 1 ≤ i ≤ n -1 and θ i for 1 ≤ i ≤ n, together with the equations (4) of the braid group B n and the equations below: