Chu’s construction: A proof-theoretic approach

G. Bellin ^{∗}

March 12, 1999

Abstract

The essential interaction between classical and intuitionistic features in the system of linear logic is best described in the language of category theory. Given a symmetric monoidal closed category C with products and coproducts, the category C × C^{op} can be given the structure of a ∗-autonomous category by a special case of the Chu construction. The main result of the paper is to show that the intuitionistic translations induced by Girard’s trips determine the functor from the free ∗-autonomous category A on a set of atoms {P_{i}} to C × C^{op}, where C is the free monoidal closed category with products and coproducts on the set of atoms {P_{O}_{i}, P_{I}_{i}} (a pair P_{O}, P_{I} in C for each atom P of A).

Contents

1 Preface 2 2 The trip translation 4

∗Research supported by EPSRC senior research fellowship on grant GL/L 33382. We wish to thank Martin Hyland for his essential suggestions and crucial support in the develoment of this work.

2.1 Languages, intuitionistic and classical MALL . . . . . . . . . . 4 2.2 Background: trips and linear λ terms . . . . . . . . . . . . . . 8 2.3 Background: the trip translations in CMLL^{−} . . . . . . . . . 9 2.4 The functorial trip translation for MALL . . . . . . . . . . . . 12

3 The Chu construction 14

1 Preface

An essential aim of linear logic is the study of the dynamics of proofs, especially normalization (cut elimination) in a system enjoying the good prooftheoretic properties of intuitionistic logic, but where the dualities of classical logic hold. Proofs in classical linear logic CLL are formalized in the sequent calculus, but also by proof-nets and in the latter representation CLL is not only strongly normalizable, but also confluent. Although Girard’s main system of linear logic [12] is classical, considerable attention in the literature has also been given to the system of intuitionistic linear logic ILL, where proofs are also formalized in a sequent calculus and in a natural deduction system.

The fact that intuitionistic logic plays an important role in the architecture of linear logic is not suprising: as indicated in the introductory section of Girard’s fundamental paper [12], a main source of inspiration for the system was its denotational semantics of coherent spaces, a refinement of Scott’s semantics for the λ-calculus. Fundamental decisions about the system CLL were made so that CLL has a semantics of proofs in coherent spaces in the same way as intuitionistic logic has a semantics of proofs in Scott’s domains (a form of the Curry-Howard isomorphism). But linear logic is not just a refinement of intuitionistic logic, such as ILL: there are expectations that CLL may tell us something fundamental about classical logic as well, indeed, that through linear logic a deep level of analysis may have been reached from which the “unity of logic” can be appreciated [13]. Therefore the relations between classical and intuitionistic components of CLL deserve careful investigation.

A natural points of view to look at this issue is categorical logic. It has been known for years that monoidal closed categories provide a model for intuitionistic linear logic, though a fully adequate formulation of the syntax and of the categorical semantics of ILL especially with respect to the exponentials, has required considerable subtlety and effort [4, 5, 6]. It is also well known that ∗-autonomous categories give a model for classical linear logic [3]. The appendix to [2] provides a method, due to Barr’s student Chu, to construct ∗-autonomous categories starting from monoidal closed ones.

In our proof-theoretic investigation we encounter a special case of Chu’s construction. Given the free ∗-autonomous category A on a set of objects (propositional variables) {P_{i}} and given the symmetric monoidal closed category C with products and coproducts, free on the set {P_{O}_{j}, P_{I}_{j}} (a pair P_{O}, P_{I} in C for each atom P of A), the category C × C^{op} can be given the structure of a ∗-autonomous category. In particular, the tensor product (C, C^{op})⊗(D, D^{op}) must be an object of the form (C ⊗D, (C −∘ D^{op})×(D −∘ C^{op})) and the identity of the tensor must be (1, ⊤). Since A is free, there is a functor F from A to (C × C^{op}); but so far no familiar construction had been shown to correspond to the functor F given by the abstract theory. Here we show that a familiar proof-theoretic construction, namely Girard’s trips [12] on a proof-net, represent the action of such a functor on the morphisms of A.

This result rewards several efforts to understand and clarify the theory of proof-nets. Given a proof-structure, i.e., a directed graph where edges are labelled with formulas, a correctness criterion characterizes those proofstructures which correspond to proofs in the sequent calculus. Girard’s condition (“there are no short trip”) is exponential in time on the size of the proof-structure, while other quadratic criteria are known (among others, one was given in the author’s thesis [7]). Thus it is natural to ask what additional information is contained in the construction of Girard’s trips other than the correctness of a proof-structure. The beginning of an answer came in 1992, when Jacques van de Wiele and the author, inspired by Danos’ notion of a pure net, defined the trip translation: every Girard’s trip on a cut-free proof-nets corresponds to a derivation in the fragment of intuitionistic linear logic with times and linear implication. But the significance of this result seemed limited by the fact that the result did not seem to extend beyond the multiplicative fragment. A better understanding of the situation and a generalization of the theorem has come only from an explicit effort to formulate the trip translation as a functorial operation; only then it became evident that classical multiplicative linear logic was to be related to intuitionistic multiplicative and additive linear logic and the categorical result followed (for which we gratefully acknowledge the influence and the support of Martin Hyland).

When the languages and the aims of different scientific communities meet in a new theory and new structures are identified, the conceptual architecture may look different from the different points of view and it may be hard to say which structures are fundamental. From the point of view of categorical logic Chu’s construction seems to suggest a fundamental status to monoidal closed categories with respect to the ∗-autonomous ones. However, the correspondence established by Chu’s construction is not an isomorphism, as the functor F is not full, and its faithfulness at the moment is only a conjecture. Therefore the relations between classical and intuitionistic linear logic remain a complex matter. More is also to be said about the exponentials, which we leave to a future paper. Finally, further clarification is needed to spell out intriguing analogies between Chu’s construction and the game theoretic semantics of linear logic.

2 The trip translation

2.1 Languages, intuitionistic and classical MALL

The syntax of propositional classical Linear Logic CLL is given in Girard [12]: formulas are in “negation normal form”, i.e., they are built from propositional constants 1, ⊥, ⊤ and 0, atoms P_{i} and negations of atoms (P_{i})^{⊥} using the connectives ⊗, ℘, & and ⊕ and the exponential operators ! and ?; negation for nonatomic formulas is defined:

⊥^{⊥} =_{d} 1 1^{⊥} = ⊥ (A ⊗ B)^{⊥} =_{d} A^{⊥}℘B^{⊥} (A℘B)^{⊥} =_{d} A^{⊥} ⊗ B^{⊥} ⊤^{⊥} =_{d} 0 0^{⊥} =_{d} ⊤ (A&B)^{⊥} =_{d} A^{⊥} ⊕ B^{⊥} (A ⊕ B)^{⊥} =_{d} A^{⊥}&B^{⊥}

(!A)^{⊥} =_{d} ?(A^{⊥}) (?A)^{⊥} = !(A^{⊥})

CMALL [CMLL] is the fragment of CLL without exponentials [without exponentials and additives]; CMLL^{−} is CMLL without propositional constants.

Recall that the sequent calculus for propositional CMALL has the following axioms and rules:

identity rules

logical axiom:

⊢A^{⊥},A

cut: ; \frac{⊢ Γ, A^{⊥} ⊢ Δ, A}{⊢ Γ, Δ}

structural rules exchange:

\frac{⊢ Γ, A, B, Δ}{⊢ Γ, B, A, Δ}

logical rules

{one: \atop ⊢ 1}

nil: ; \frac{⊢ Γ}{⊢ Γ, ⊥}

times:

\frac{⊢ Γ, A ⊢ Δ, B}{⊢ Γ, Δ, A ⊗ B}

par: ; \frac{⊢ Γ, A, B}{⊢ Γ, A℘B}

{true: \atop ⊢ Γ, ⊤}  with: ; \frac{⊢ Γ, A ⊢ Γ, B}{⊢ Γ, A&B} plus: ; \frac{⊢ Γ, A_{i}}{⊢ Γ, A_{0} ⊕ A_{1}} for i = 0, 1.

The sequent calculus CMALL.

The propositional language of intuitionistic Linear Logic ILL is built from a set of propositional atoms {P_{O}, P_{I}, P′_{O}, P′_{I}, …}, and the propositional constants 1, ⊤ and 0, using the connectives −∘ (linear implication) and ⊗, & and ⊕ and the exponential !. (We take the point of view that there is no symbol “⊥” for “multiplicative falsity” in ILL. Thus P_{O} and P_{I} may be regarded as “positive and negative atoms”, respectively). Again IMALL is the fragment of ILL without exponentials, etc.

The sequent calculus for propositional IMALL has the following axioms and rules:

identity rules

logical axiom: A ⊢ A

cut: ; \frac{Γ ⊢ A A, Δ ⊢ B}{Γ, Δ ⊢ B}

structural rules

exchange:

\frac{Γ, A, B, Δ ⊢ C}{Γ, B, A, Δ ⊢ C}

logical rules

{R one: \atop ⊢ 1}  L one: ; \frac{Γ ⊢ B}{Γ, 1 ⊢ B}

R times:

\frac{Γ ⊢ A Δ ⊢ B}{Γ, Δ ⊢ A ⊗ B}

L times:

\frac{Γ, A, B ⊢ C}{Γ, A ⊗ B ⊢ C}

R implication: \frac{Γ, A ⊢ B}{Γ ⊢ A −∘ B} L implication:

\frac{Γ ⊢ A B, Δ ⊢ C}{A −∘ B, Γ, Δ ⊢ C}

{R true: \atop Γ ⊢ ⊤}  {L zero: \atop 0, Γ ⊢ A}

R with:

\frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A&B}

L with: ; \frac{Γ, A_{i} ⊢ B}{Γ, A_{0}&A_{1} ⊢ B}

for i = 0, 1.

plus: ; \frac{Γ ⊢ A_{i}}{Γ ⊢ A_{0} ⊕ A_{1}}

for i = 0, 1.

L plus:

\frac{A, Γ ⊢ C B, Γ ⊢ C}{A ⊕ B, Γ ⊢ C}

The sequent calculus IMALL.

Proof-structures for CMALL are directed graphs with at least one external point and where each vertex is typed and has the form indicated in Figure 1. The dashed line in a ⊥-vertex is called an attachment.

Figure 1: Links

On proof-structures for CMLL Girard’s trips are defined according to the drawings in Figure 2; the choice of the form of a trip at a par link is called a left or right switch. Proof-nets for MLL are proof-structures satisfying Girard’s no-short-trip condition, namely, that for every switching of the par links and every conclusion C, the trip starting at C returns to C after visiting each edge precisely twice (cf. [12])

In the case of CMALL we have true boxes which behave line n + 1-ary axioms. Moreover, a boolean valued polynomial is associated with each edge, a distinct boolean variable x is associated with each with link, x and 1 − x being added to the polynomials associated with the left and right premise of the with link in question. The polynomial of the conclusion of a link is the sum of the polynomials of the premises. All the conclusions of the proof-net must have 1 as associated polynomial. A proof structure is sliced by substituting arbitrary boolean values for the variables and erasing the edges whose polynomial evaluates to 0; in a sliced proof-structure additive links are all unary. (For a more precise definition, of additive proof-nets, see Girard [14].) All said, a CMALL proof-structure is a proof-net if for every evaluation of the polynomials, the resulting slice has no short trip.

What matters here is that the following theorem can be proved:

Figure 2: Girard’s trips

Girard’s Theorem. There exists a ‘context-forgetting’ map ( )^{−} from sequent derivations in MALL to proof-nets with the following properties:

(a) Let d be a sequent derivation of ⊢ Γ; then (d)^{−} is a proof-net with conclusion Γ;

(b) (Sequentialization) If R is a proof-net with conclusion Γ, then there is a sequent calculus derivation d of ⊢ Γ such that R = (d)^{−}.

2.2 Background: trips and linear λ terms

A trip in the sense of Girard induces the structure of a λ-term in any suitable graph with a selected external point (pointed graph):

Theorem 1. (J. van de Wiele) Every connected pointed graph with vertices of incidence 1 and 3 corresponds to a linear λ-term (and viceversa). The correspondence is established in linear time by a trip starting with the selected external point.

We perform a trip in the style of Girard according to the figure below; during the trip we determine whether a vertex is to be regarded as (1) a variable, (2) an application or (3) a λ-abstraction. Case (2) occurs when during the second visit to a vertex of incidence 3 the trip enters the vertex through the same edge from which it had exited after the first visit; case (3) occurs when the second visit is through the other edge; case (1) is that of an external vertex different from the selected one.

Figure 3: Linear λ-terms

The proof is by induction on the number of vertices. Notice that if we remove the first vertex of incidence 3 encountered during the trip then the resulting graph is disconnected in case (2) but remains connected in case (3). Different variables are assigned to different external points in case (1). Since linear λ-terms are always typable, van de Wiele’s result also shows that every such connected pointed graph corresponds to a proof in the implicative fragment of intuitionistic linear logic.

2.3 Background: the trip translations in CMLL^{−}

Essentially the same technique applied to a proof-net for CMLLL^{−} yields a translation of the proof-net into a derivation in the implication and tensor fragment of intuitionistic multiplicative linear logic. In a proof-structure edges are arrows and vertices are directed and already typed, but the correctness condition for proof-nets guarantees that the passages of a trip across ⊗ and ℘ links have the same patterns as those of application and abstraction links, respectively. Trips always have a starting point in a conclusion and the order of the passages across a link matters. To state our result we need a definition.

Definitions. (i) Given a proof-net R for CMLL^{−} and a selected conclusion A, we say that a Girard trip starting from A is covariant on an edge if the second passage of the trip is in the same direction as the edge; otherwise, the trip is contravariant on the edge. Now a trip starting from A induces an input-output orientation δ : R → {I, O} thus: an edge X is an output X_{O} or an input X_{I} depending on whether the trip is covariant or contravariant on it. (ii) An input-output orientation δ : R → {I, O} (and the corresponding trip) is computationally inconsistent if in some proof-net R′ obtained from R by cut elimination the premises of some cut have the same orientation, i.e., either the orientation, A_{I}, A_{I}^{⊥} or the orientation A_{O}, A_{O}^{⊥}.

Notice the ambiguity of the notation: P_{O}, P_{I} are used here for the orientation of a CLL formula P and also for its translation into ILL; P_{O}, P_{I} are also atoms of ILL.

Theorem 2. (Bellin and van de Wiele) (i) Every computationally consistent Girard’s trip on a proof-net for CMLL^{−} starting from a selected conclusion corresponds to a sequent calculus derivation in IMLL^{−}. Every proof-net for CMLL^{−} has some computationally consistent orientation.

(ii) Conversely, every sequent derivation in IMLL^{−} corresponds to a computationally consistent trip on a proof-net.

We summarize the argument here; for more details, see [8], pp. 37-44. The following proposition follows almost immediately from the definition of orientation and the basic properties of trips.

Proposition 1. Every orientation makes the selected conclusion an output, all other conclusions are inputs. Every link is oriented in one of the admissible ways indicated in Figure 4.

The existence of computationally consistent trips on every CMLL^{−} proofnet can be proved by induction on the length of the cut-elimination process for CMLL^{−}.

Given a computationally consistent orientation δ : S → {I, O}, the for-

Figure 4: Admissible orientations.

mulas in the proof-net are translated as follows:

(P^{⊥})_{O} = P_{I},  for P atomic (P^{⊥})_{I} = P_{O};
(A ⊗ B)_{O} = A_{O} ⊗ B_{O},  (A℘B)_{I} = A_{I} ⊗ B_{I};
(A ⊗ B)_{I} = A_{O} −∘ B_{I}, if δ(A) = O,
= B_{O} −∘ A_{I}, if δ(B) = O.
(A℘B)_{O} = A_{I} −∘ B_{O}, if δ(B) = O,  (right switch)
= B_{I} −∘ A_{O}, if δ(A) = O.  (left switch)

To show that the case of Cut is well-defined, one proves the following proposition, using the fact that the orientation is computationally consistent:

Proposition 2. (A^{⊥})_{I}^{δ} = A_{O}^{δ}

Remarks. (i) The above translation of formulas is not functorial, as it depends on the given proof.

(ii) The above result does not extend to full CMLL: let ⊥ be the selected conclusion in the cut-free proof-net with conclusion P, P^{⊥}, ⊥.

(iii) The above result does not extend to CMALL: consider the cut-free proof-net with conclusions A&B, A^{⊥} ⊗ B^{⊥}, A ⊕ B.

2.4 The functorial trip translation for MALL

One motivation for our result has been the extension of the trip translation to the whole system CLL. The key remark is to define the translation as in Figure 5, accepting that CMLL needs to be translated into IMALL rather than into IMLL. This now works wonderfully, and also the translation of the formulas is functorial as it does not depend on the proof. Also, we do not need to know in advance which trips are computationally consistent: they are given by the interaction of the additives in the translation of the ⊗ and ℘ links.

Now ⊥_{O} = ⊤, so the cut-free proof-net in Remark (ii) above (with conclusions P, P^{⊥}, ⊥ and with ⊥ selected) is translated by the axiom P_{I}, P_{O} ⊢ ⊤: so the translation of the proof-net is erased. However, this information is preserved in the derivations of P_{I}, 1 ⊢ P_{I} and of P_{O}, 1 ⊢ P_{O}, when the selected conclusion is P^{⊥} or P.

All said, the definition of the functorial trip translation is given in Figures 5 and 6. The selected conclusion in a CMALL sequent is written in boldface.

(P^{⊥})_{O} = P_{I},  for P atomic;  (P^{⊥})_{I} = P_{O};
1_{O} = 1  1_{I} = ⊤  ⊥_{I} = 1  ⊥_{O} = ⊤;
(A ⊗ B)_{O} = A_{O} ⊗ B_{O},  (A℘B)_{I} = A_{I} ⊗ B_{I};
(A ⊗ B)_{I} = (A_{O} −∘ B_{I}) & (B_{O} −∘ A_{I}); (A℘B)_{O} = (A_{I} −∘ B_{O}) & (B_{I} −∘ A_{O});
⊤_{O} = ⊤ ⊤_{I} = 0; 0_{O} = 0 0_{I} = ⊤;
(A&B)_{O} = A_{O}&B_{O},  (A&B)_{I} = A_{I} ⊕ B_{I};
(A ⊕ B)_{O} = A_{O} ⊕ B_{O},  (A ⊕ B)_{I} = A_{I}&B_{I}

Fig. 5: Functorial trip translation, the propositions.

Remarks. (i) The treatment of ⊥ suggsts a possible treatment of the exponentials: (!A)_{O} = !A_{O}; (!A)_{I} = !A_{O} −∘ ⊤; (?A)_{O} = !A_{I} −∘ ⊤, (?A)_{I} = !A_{O}.

⊢ P^{⊥}, P  ⟹  P_{O} ⊢ P_{O}  ⊢ P^{⊥}, P  ⟹  P_{I} ⊢ P_{I}
cut : \frac{⊢ Γ, A  ⊢ A^{⊥}, Δ, C}{⊢ Γ, Δ, C} ⟹ cut : \frac{Γ_{I} ⊢ A_{O}  A_{I}^{⊥}, Δ_{I} ⊢ C_{O}}{Γ_{I}, Δ_{I} ⊢ C_{O}}
⊗_{O} : \frac{⊢ Γ, A  ⊢ Δ, B}{⊢ Γ, Δ, A ⊗ B} ⟹ ⊗ −R : \frac{Γ_{I} ⊢ A_{O}  Δ_{I} ⊢ B_{O}}{Γ_{I}, Δ_{I} ⊢ A_{O} ⊗ B_{O}}
⊗_{I} : \frac{⊢ Γ, A  ⊢ B, Δ, C}{⊢ Γ, A ⊗ B, Δ, C} ⟹ −∘ −L : \frac{\frac{Γ_{I} ⊢ A_{O}  B_{I}, Δ_{I} ⊢ C_{O}}{Γ_{I}, A_{O} −∘ B_{I}, Δ_{I} ⊢ C_{O}}}{Γ_{I}, (A_{O} −∘ B_{I})&(B_{O} −∘ A_{I}), Δ_{I} ⊢ C_{O}}

℘_{O} : \frac{⊢ Γ, A, B}{⊢ Γ, A℘B} and \frac{⊢ Γ, A, B}{⊢ Γ, A℘B} ⟹ −∘ −R : \frac{\frac{Γ_{I}, A_{I} ⊢ B_{O}}{Γ_{I} ⊢ A_{I} −∘ B_{O}} \frac{Γ_{I}, B_{I} ⊢ A_{O}}{Γ_{I} ⊢ B_{I} −∘ A_{O}}}{Γ_{I} ⊢ (A_{I} −∘ B_{O})&(B_{I} −∘ A_{O})}

℘_{I} : \frac{⊢ A, B, Γ, C}{⊢ A℘B, Γ, C}  ⟹  \frac{A_{I}, B_{I}, Γ_{I} ⊢ C_{O}}{A_{I} ⊗ B_{I}, Γ_{I} ⊢ C_{O}}
⊢ 1  ⟹  ⊢ 1
⊥_{I} : \frac{⊢ Γ, A}{⊢ ⊥, Γ, A}  ⟹  1 − L : \frac{Γ_{I} ⊢ A_{O}}{1, Γ_{I} ⊢ A_{O}}
⊥_{O} : \frac{⊢ Γ}{⊢ Γ, ⊥ ⊥}  ⟹  Γ_{I} ⊢ ⊤
⊢ Γ, ⊤ ⊤  ⟹  Γ_{I} ⊢ ⊤  ⊢ ⊤, Γ, C  ⟹  0, Γ_{I} ⊢ C_{O}
&_{O} : \frac{⊢ Γ, A  ⊢ Γ, B}{⊢ Γ, A&B} ⟹ & − R : \frac{Γ_{I} ⊢ A_{O}  Γ_{I} ⊢ B_{O}}{Γ_{I}, Δ_{I} ⊢ A_{O}&B_{O}}
&_{I} : \frac{⊢ A, Γ, C  ⊢ B, Γ, C}{⊢ A&B, Γ, C} ⟹ ⊕ −L : \frac{A_{I}, Γ_{I} ⊢ C_{O}  B_{I}, Γ_{I} ⊢ C_{O}}{A_{I} ⊕ B_{I}, Γ_{I} ⊢ C_{O}}

⊕_{O} : \frac{⊢ Γ, A_{i}}{⊢ Γ, A_{0} ⊕ A_{1}} ⟹ ⊕ −R : \frac{Γ_{I} ⊢ (A_{i})_{O}}{Γ_{I} ⊢ (A_{0})_{O} ⊕ (A_{1})_{O}}

⊕_{I} : \frac{⊢ Γ, A_{i}, C}{⊢ Γ, A_{0} ⊕ A_{1}, C} ⟹ ⊕ −R : \frac{Γ_{I}, (A_{i})_{I} ⊢ C_{O}}{Γ_{I}(A_{0})_{I}&(A_{1})_{I} ⊢ C_{O}}

Fig. 6: Functorial trip translation, the proofs.

13 (ii) The functorial translation appears as an abstract representation of the game-theoretic semantics: think of P_{O} in an axiom as a move by the opponent and P_{I} as the reply by the player.

(iii) To the trip translation there corresponds an obvious functorial map in the opposite direction; in proof-theoretic terms it amounts to regarding IMALL as a fragment of CMALL, namely:

1. writing formulas in “negation normal form”, using De Morgan laws;

2. writing proofs in the sequent calculus with “right-hand sequents” only;

3. finally, translating them into proof-nets, i.e., “forgetting the context”.

3 The Chu construction

We follow the categorical semantics for IMLL in [5]:

Theorem 3. Let A be the free ∗-autonomous category on a set of objects {P, P′, …} and let C be the symmetric monoidal closed category with products, free on the set of objects {P_{O}, P_{I}, P′_{O}, P′_{I}, …} (a pair P_{O}, P_{I} for each atom P of A).

(i) We can give C × C^{op} the structure of a ∗-autonomous category thus:

(X_{O}, X_{I}) ⊗ (Y_{O}, Y_{I}) =_{df} (X_{O} ⊗ Y_{O}, (X_{O} −∘ Y_{I}) × (Y_{O} −∘ X_{I}))

with unit (1, ⊤) and involution (X_{O}, X_{I})^{⊥} =_{df} (X_{I}, X_{O})

where 1 is the unit of ⊗ in C and ⊤ the terminal object of C.

Therefore there is a functor F from A to (C × C^{op}) sending an object P to (P_{O}, P_{I}). If π : I → ℘(Γ) is a morphism of A represented as a proof-net R with conclusions Γ, then the morphism (1, ⊤) → (℘(Γ)_{O}, ℘(Γ)_{I}) is given by all the Girard’s trips on R.

(ii) If in addition C has also coproducts, then (C × C^{op}) has also products:

(X_{O}, X_{I})&(Y_{O}, Y_{I}) =_{df} (X_{O}&Y_{O}, X_{I} ⊕ Y_{I}).

The functor F preserves also the structure of the products.

(iii) More generally, consider the 2-categories • IMALL, with objects the symmetric monoidal closed categories with

products, 1-cells the monoidal functors and 2-cells the natural isomorphisms;

• CMLL, with objects the ∗-autonomous categories, 1-cells the monoidal functors and 2-cells the natural isomorphisms;

then the construction C ↦ C × C^{op} extends to a 2-functor IMALL → CMLL, taking structure-preserving 1-cells to structure-preserving 1-cells.

Hence there is a structure-preserving functor F from the free ∗-autonomous category on P, P′, … to C × C^{op}, sending P ↦ (P_{O}, P_{I}), …, which is given by the proof-theoretic trip translations above.

Sketch of proof of (i) and (ii). In C × C^{op} define X℘Y =_{df} (X^{⊥} ⊗ Y^{⊥})^{⊥} and X −∘ Y =_{df} X^{⊥}℘Y and show that X −∘ Y gives the closed structure for ⊗. By the definitions

(V, Y) −∘ (W, Z) = ((V −∘ W) × (Z −∘ Y), V ⊗ Z)

We exhibit a natural bijection of hom-sets

(U, X) ⊗ (V, Y) → (W, Z)  ∼  (U, X) → (V, Y) −∘ (W, Z)

Indeed a map in (U, X) ⊗ (V, Y) → (W, Z) consists of a map a : U ⊗ V → W and of a pair of maps b : Z → U −∘ Y, c : Z → V −∘ X; a map in (U, X) → (V, Y) −∘ (W, Z) consists of a pair of maps a′ : U → V −∘ W, b′ : U → Z −∘ Y and of a map c′ : V ⊗ Z → X. But a ↦ a′ and c ↦ c′ by the natural bijections given by the symmetric monoidal closed structure of C. Similarly, there is a natural bijection η between Z → U −∘ Y and Z ⊗ U → Y and also a natural bijection η′ between Z ⊗ U → Y and U → Z −∘ Y; composing η′ and η we get b ↦ b′. Therefore −∘ is a right adjoint for ⊗ in C × C^{op}.

Remarks. (i) The functor F is not full. For instance, F (⊥) = (⊤, 1), and there is a morphism F (1) → F (⊥) in C × C^{op}, namely, the map t × t′ : (1, ⊤) → (⊤, 1), where t′ : ⊤ → 1 =_{df} t : 1 → ⊤; however, the free category A does not have a morphism 1 → ⊥, i.e., ⊥ is not provable in MLL. The system CLL + ⊥ = 1 has been studied, e.g., in [11], and perhaps this extension of linear logic deserves further consideration, but it is not the answer to our concern here. Indeed even in CMLL without the units a map in C × C^{op}, say F (X) → F (Y), may correspond to two arbitrary proofs d of X_{O} ⊢ Y_{O} and d′ of Y_{I} ⊢ X_{I}, where d and d′ are “too dissimilar” to result from the same proof-net by the trip translation. The task is rather to characterize a subcategory of C × C^{op} for which the functor F is full.

(ii) Is the functor F is faithful? This question raises the issue of the identity of proofs in linear logic, which is not fully understood beyond the multiplicative fragment without units. In [5] cut reductions in IMALL correspond to βη equality of the terms which express the maps in the free symmetric monoidal closed category and commutative conversions correspond to natural isomorphisms between them. If in C × C^{op} we consider terms up to βη equivalence, then faithfulness requires that the corresponding assumption is made about A, i.e., morphisms of A should be represented by proof-nets up to cut-elimination and η-equivalence. This condition seems unproblematic only for CMLL without units, because in this fragment the Church-Rosser property holds strictly. Thus it is safe to leave the whole issue of faithfulness to further research.

References

[1] Samson Abramsky and Radha Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic. J. Symb. Logic 59, 2, pp.543-574, 1994.

[2] M. Barr. ∗-Autonomous categories, Lecture Notes in Mathematics 752, Springer-Verlag, 1979, Berlin, Heidelberg, New York.

[3] M. Barr. ∗-Autonomous categories and linear logic, Mathematical Structures in Computer Science (1991), 1, pp. 159-178

[4] N. Benton, G. Bierman, V. de Paiva, M. Hyland. A term calculus for intuitionistic linear logic. Springer LNCS 664, pp. 75-90, 1993.

[5] N. Benton, G. Bierman, V. de Paiva, M. Hyland. Linear λ-Calculus and Categorical Models Revisited, Preprint, Comp. Lab., Univ. of Cambridge.

[6] G. M. Bierman. What is a Categorical Model of Intuitionistic Linear Logic? In Proceedings of the International Conference on Typed Lambda Calculi and Applications. April 10-12, 1995. Edinburgh, Scotland. Springer LNCS.

[7] G. Bellin. Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information, Phd Thesis, Stanford University. Available as: Report CST-80-91, June 1990, Dept. of Computer Science, Univ. of Edinburgh.

[8] G. Bellin and P. J. Scott. Theor. Comp. Sci. 135, 1994 n. 1, pp. 11-65.

[9] G. Bellin and J. van de Wiele. Subnets of Proof-nets in MLL^{−}, in Advances in Linear Logic, Girard, Lafont and Regnier eds., London Math. Soc. Lect. Note Series 222, Cambridge University Press, 1995, pp. 249-270.

[10] Valeria C.V. de Paiva. The Dialectica Categories. PhD thesis. DPMMS, University of Cambridge, 1988. Available as Comp. Lab. Tech. Rep. 213, 1990.

[11] A. Fleury and C. Retoré. The Mix Rule, Mathematical Structures in Computer Science 4, 1994, pp. 273-85.

[12] J-Y. Girard. Linear Logic, Theoretical Computer Science 50, 1987, pp.1-102.

[13] J-Y. Girard. On the unity of logic. Ann. Pure App. Log. 59, pp.201-217, 1993.

[14] J-Y. Girard. Proof-nets: the parallel syntax for proof-theory. In Logic and Algebra, New York, 1995. Marcel Dekker.

[15] M. Hyland and L. Ong. Fair games and full completeness for Multiplicative Linear Logic without the Mix rule. ftp-able at theory.doc.ic.ac.uk in

papers/Ong, 1993.

[16] F.Lamarche. Games Semantics for Full Propositional Logic. Proceedings of LICS 1995.

Gianluigi Bellin Facoltà di Scienze Unversità di Verona Strada le Grazie - Ca’ Vignal 37134 Verona - ITALY

Email: bellin@sci.univr.it.