Theory and Applications of Categories, Vol. 3, No. 5, 1997, pp. 85–131.

PROOF THEORY FOR FULL INTUITIONISTIC LINEAR LOGIC, BILINEAR LOGIC, AND MIX CATEGORIES

J.R.B. COCKETT AND R.A.G. SEELY

Transmitted by Michael Barr

ABSTRACT. This note applies techniques we have developed to study coherence in monoidal categories with two tensors, corresponding to the tensor–par fragment of linear logic, to several new situations, including Hyland and de Paiva’s Full Intuitionistic Linear Logic (FILL), and Lambek’s Bilinear Logic (BILL). Note that the latter is a noncommutative logic; we also consider the noncommutative version of FILL. The essential difference between FILL and BILL lies in requiring that a certain tensorial strength be an isomorphism. In any FILL category, it is possible to isolate a full subcategory of objects (the “nucleus”) for which this transformation is an isomorphism. In addition, we define and study the appropriate categorical structure underlying the MIX rule. For all these structures, we do not restrict consideration to the “pure” logic as we allow non-logical axioms. We define the appropriate notion of proof nets for these logics, and use them to describe coherence results for the corresponding categorical structures.

0. Introduction

In [CS91] we introduced the notion of “weakly distributive category”, now renamed “linearly distributive category”, in order to study the pure proof theory of the cut rule for the sequent calculus with finite sequences of formulas on both sides of the turnstile. This is generally thought of as the “classical” sequent calculus, but in fact this proof theory is not truly “classical” in any real sense, and may be thought of as the tensor–par fragment of linear logic with no negation. We wished to show how features could be added in a modular fashion to this basic categorical setting, in order to model the more expressive fragments of linear logic: this program is now largely complete, see [CS91, BCST, BCS92], and includes the subject matter of this paper.

Crucial to this program was the provision of an intrinsic characterization of the par. In classical linear logic the negation was an obstruction, for it allowed the par to be viewed as merely the de Morgan dual of the usual tensor product, and so for its special

1Research partially supported by NSERC, Canada. ^{2}Research partially supported by Le Fonds FCAR, Québec, and NSERC, Canada. Diagrams in this paper were produced with the help of the TEXcad drawing program of G. Horn and the diagram macros of F. Borceux.

Received by the editors 1996 September 23 and, in revised form, 1997 March 17. Published on 1997 March 28 1991 Mathematics Subject Classification : 03B70, 03F07, 03G30, 18D10, 18D15, 19D23. Key words and phrases: monoidal closed categories, tensorial strength, coherence, categorical proof

theory.

\begin{matrix}c \\ ◯ \end{matrix} J.R.B. Cockett and R.A.G. Seely 1997. Permission to copy for private use granted.

properties to be swept under the rug of “duality”. Foremost here is the role played by tensorial strength. The central feature of “linear distributivity”, which amounts to the property that each tensor is linearly strong relative to the other, had not been stressed before [CS91], largely we believe, because its role is not apparent in the fully dual context of classical linear logic.

At about the same time as [CS91], a system which lacked the full duality of classical linear logic was being studied by de Paiva and Hyland. The logic was linear and had, instead of negation, a linear implication [HP93]. They named the logic, appropriately, “full intuitionistic linear logic” or FILL for short. Interestingly—and quite independently—they noticed the crucial role played by the “weak distributivities” linking the tensor and par in their system [HP91]. These were exactly the linear strengths, or “linear distributivities”, we had been studying. (They even used the same term—weak distributivity—as we then used.)

Since the 1950’s Lambek has studied a number of logics without structural rules; a summary of many of these may be found in [L93]. We shall consider two such noncommutative linear logics here: the main feature that distinguishes these from FILL, apart from their being noncommutative, is that the par–tensorial strength for the internal hom arising from the linear distributivity should be an isomorphism. The first such logic has the minimal closed structure that is natural in this setting, having left and right implications for the tensor; we shall refer to this logic as “Grishin Implicative Linear Logic” or GILL for short, reflecting the fact that Grishin was the first to note the importance of the isomorphism mentioned above [Gr83]. In addition we consider Lambek’s system BL2, which we shall refer to as BILL. This logic has not only GILL’s left and right implications but also left and right dual implications for the par. We shall show that the categorical semantics of GILL and BILL are in fact equivalent, and correspond to an appropriate notion of noncommutative ∗-autonomous category. In [L93] Lambek shows that in the posetal case, adding the Grishin isomorphism to (noncommutative) FILL gives full multiplicative linear logic; we extend this in the obvious way to full categorical generality.

We shall also show how our approach to coherence via proof nets can be applied to these variants of linear logic: in particular we shall discuss the proof nets for both (commutative and noncommutative) FILL and BILL. The principle addition to our previous work is to show how the autonomous (or monoidal closed) structure may be handled. Our approach is somewhat different from the related work of Trimble’s [T94], in that we use proof “boxes” to handle “scoping” for this structure. We shall briefly discuss a suggestive box-free notation which is closer to Trimble’s approach. However, we also discuss the shortcomings of this notation. If one wishes to express, for example, the proof theory of FILL, what is allowed in the scope of an implication (introduction) and what is not becomes quite crucial: in a box-free notation it is much more difficult to recover these precise scopes.

A further related point of some interest is worth mentioning: Schellinx [Sc91] showed that cut elimination fails for FILL. It may, therefore, seem quite paradoxical to claim coherence results (normalization theorems) for this proof theory, since cut elimination and normalization for logical systems are regarded as being intimately related—even synonymous. However, FILL is a curious witness to the fact that this relationship need not necessarily be very straightforward.

Hyland and de Paiva in [HP93] take the view that that cut elimination must not fail. In order to obtain cut elimination in this setting, however, they had to modify the sequent calculus by attaching proof annotations. These annotations are essentially the natural deduction style proofs which we present here.

Here we wish to promote the virtues of natural deduction per se, and so the temptation to adopt a contrary view has been impossible to resist. In the unannotated sequent calculus for FILL not only can normal FILL derivations contain “essential cuts” but also it is possible for two distinct FILL derivations to be equivalent as proofs and yet be impossible to reduce to each other under the usual cut elimination procedure. However, when one presents these proofs in the natural deduction style we are advocating, these obstructions untangle in a rather natural way.

After developing the theory for FILL and BILL, we show that there are several connections between these doctrines. The most interesting uses the notion of the nucleus of a FILL category: this is a generalization of the notion of the nucleus of a symmetric monoidal category. The nucleus of a (commutative) FILL category is a ∗-autonomous full subcategory with the same tensor, par and implication.

In addition, we fill a gap in the literature by defining what it means for a linearly distributive category to satisfy the MIX rule. There are some subtleties here concerning the appropriate coherence conditions that are necessary for a good fit with the logic. While the MIX rule has been studied before [FR94], the connection with categorical structures had not been completely worked out. One point of interest is that a linearly distributive category satisfies the MIX rule if and only if its nucleus does. This has an interesting consequence: all linearly distributive categories which have either the tensor cartesian or par cartesian, necessarily satisfy the MIX rule. This gives a plentiful source of examples of MIX categories.

This paper is part of a series of papers on the structure of linearly distributive categories; more complete details, at least on the basic context, can be found in the other papers [CS91, BCST, BCS92]—the reader should also see [T94] for its treatment of autonomous categories.

Work such as this focuses on the structure of proofs of a theory in a manner still not quite standard in logic. There are two questions coherence theory deals with: the existence of proofs of particular logical sequents, and the equality of proofs of a particular sequent, or equivalently, whether or not particular homsets in the appropriate free category are inhabited, and whether or not two morphisms with the same domain and codomain are equal. The first is indeed part of standard proof theory, but the second is still frequently seen (wrongly we contend) as merely part of category theory. In particular, in the many complexity studies of the proof theory of linear logic, few have addressed the complexity of equality of proofs: this is a pity as there are many interesting open questions here.

There are a few features of our presentation we would like to emphasize. Foremost is the role of tensorial strength (or linear distributivity), which captures the essence of the implicit duality between the tensors, even—or perhaps especially—in the context where a real duality is absent. We have seen this extends to the modalities ! and ? as well [BCS92].

Next, the reader should note the manipulations on our circuit diagrams (our version of proof nets)—while in all essentials these are of course equivalent to the usual Girard-Danos-Regnier proof nets, the lack of the de Morgan duality forces these nets to “open up” into a two-sided form with premises and conclusions, which we believe makes them more natural to work with. The calculus of thinning links for the tensor units was introduced in [BCST] and is the main novelty of our presentation. A similar calculus is applicable for any operators that introduce thinning, such as the exponentials. We must point out that most of the complications of this work come from the presence of the tensor units. Corresponding results for unit-free systems are quite trivial, and simple complete decision procedures for equality of maps are available. Just as has been found with the study of the complexity of existence of proofs in fragments of linear logic, we have found much of the structural richness lies with the units when analyzing equality of proofs: as mentioned above, complexity results here would be of interest.

Finally, to express the fact that the extension from FILL to ∗-autonomous categories is not conservative requires care in choosing the proof nets for FILL and BILL. Crucial in making this tractable is our use of scope boxes to represent the linear implications for the tensor (and the dual implications for the par). We show how these can be used to extend the term calculus for proof nets introduced in [BCST] and recall the subtle problem of correctly capturing the planarity condition in the noncommutative case which is accommodated by this formulation.

A reminder, and finally, a disclaimer: First, the reader will have already noticed that we have adopted the term “linearly distributive category” for what previously we have called “weakly distributive category”. This we view as a minor matter, but we have come to agree with some critics that this term is somewhat more appropriate, especially in view of the realization that distributive categories are not “weakly distributive” [CS91j]. (Well, they are not “linearly distributive” either, but that fact seems not to disturb one’s soul quite as much!) We thank Mike Barr for the suggestion of this (better) terminology. More controversial, perhaps, is our use of the symbol ⊕ for the dual tensor par, which conflicts with the notation used by Girard, but more appropriately fits the context here, where implicit duality is key. In particular, ⊕ is a multiplicative connective, and not the additive connective corresponding to a categorical coproduct nor the biproduct of linear algebra.

Finally, the key technical points introduced here are fairly straightforward, and follow the methods of [BCST] as closely as possible. Some parts of this paper consist of technical matters that arise in extending [BCST] to the present context, and may be omitted without interrupting the flow of the present paper; these have been put in the appendices. In particular, where details seem sketchy here, the reason is generally because they follow closely the details of [BCST] and can be reconstructed easily using that paper as a guide.

This paper ought to be considered as an incentive to read [BCST]. We intended that paper to be a general model of how to treat monoidal categories more general than just linearly distributive categories; this paper is an illustration of how to do that.

1. Links and circuits

We start by identifying the various links we shall allow in the graphs we use to represent deductions in the logical systems we wish to study. The reader already familiar with proof nets should find this quite straightforward. We base our presentation on the notion of typed circuit as introduced in [BCST]. In this paper we shall generally use the graphical presentation of circuits, but the reader can easily make this more rigorous by adapting the syntax of [BCST]. In Appendix A we shall show how to extend that syntax to include the new operators introduced here. There are some simple points to keep in mind:

• Our graphs are quite similar to the usual proof nets—edges represent formulas and vertices represent logical rules (introduction and elimination steps). We shall usually not label the edges (“wires”) for clarity; one can generally fill in the labels without difficulty.

• Since the logical systems we consider have no notion of negation, our graphs must correspond to two-sided sequents; they have premises and conclusions, unlike the one-sided proof nets of Girard. These nets more closely resemble traditional natural deduction than the usual proof nets; for instance, cut is replaced by grafting of trees, and the cut elimination process by reduction.

• To handle thinning (from units or from exponentials, for instance), we introduce a new kind of link (“thinning links”), which witness the folkloric condition that whenever a thinning occurs, the formula introduced must “connect” to the existing net in some way. Keeping track of how these thinning links may move about without essentially changing the net is the essence of our coherence theorem [BCST].

• We adopt a notation of Y. Lafont, indicating the principal port with a black dot. On some of the implication links this will make finding the principal port simpler. For other links we shall sometimes omit this principal port indicator.

• In order to make it easier to spot switchable links, we shall often identify them with a small arc joining the two (auxiliary) edges that may be cut in setting the switch. This arc is of course a meta-notation, and forms no part of the net.

• The “implication” links ({− \atop ∘} I), (∘− I), (⧀ E), (⧁ E) all involve “scope boxes”; that is they are applicable only to the situation where one has a subnet C to attach the link to, as with the “storage boxes” for ! and ? [BCS92].

For the bilinear logic we call BILL, we use circuits generated by a set A of atomic types and a set C of components, corresponding to non-logical axioms. Types are generated from atomic types by including the units ⊤, ⊥ for the two tensors and closing under the operations ⊗, ⊕, {− \atop ∘}, ∘−, ⧀, ⧁. There are introduction and elimination links for each of these operations and for the constants ⊥, ⊤; circuits are then generated by these links from C. We shall treat GILL and FILL as fragments of BILL at present: GILL lacks the dual tensors ⧀ and ⧁; FILL, as fragment of GILL has a further crucial difference which is emphasized below in Remark 1.1.

The introduction and elimination links are listed in Table 1. Each will be identified by a label (⊙ I), (⊙ E), where ⊙ is the operator involved, and the I, E indicates the link that introduces (a wire leaves the link at the principal port) or eliminates (a wire enters the link at the principal port) a compound formula created with that operator. A mnemonic: one obtains the cycle A, B, A ⊙ B going clockwise around an introduction link, and going counterclockwise around an elimination link.

Note that the links for {− \atop ∘} (and similarly ∘−, ⧀, ⧁) are in fact based on the traditional natural deduction rules for implication. The ({− \atop ∘} I) rule is a binding rule (i.e. involving a “box”) that replaces a derivation A, Γ ⊢ B, Δ with a derivation Γ ⊢ A {− \atop ∘} B, Δ, and the ({− \atop ∘} E) rule is just “evaluation” or modus ponens. In the box rules we have just drawn a “half-box”; generally the full scope can be deduced from the context, but if necessary one might want to indicate the rest of the scope box, say, with a dotted line. In valid (or sequential) nets C will have to be valid as well; this will be checked using the sequentialization process of Appendix B, or, equivalently, by showing that the circuit can be built inductively.

Since some of these connectives will not be familiar (and because we use a different notation from just about anyone else!—Lambek uses \ , / for {− \atop ∘}, ∘−, and ^{.}−_{·} , _{·}−^{.} for ⧁, ⧀), the sequent rules that correspond to these links are given in Table 2. In commutative logics the reader can add the exchange rule for himself. We shall just mention a few points here:

• The two linear implication (or internal hom) operators {− \atop ∘}, ∘− (“then” and “if”) are both used only in the noncommutative case (where proof circuits must be planar). Using the notation of [CS91], in the full classical (i.e. with negation) noncommutative logic they correspond to A {− \atop ∘} B = A^{⊥} ⊕ B and A ∘− B = A ⊕^{⊥}B.

• The operators ⧀, ⧁ (“less” and “from”) are dual linear implications (internal homs): they are the corresponding right adjoints to the par ⊕ (recall the implications are in the same sense left adjoints to the tensor ⊗). In full classical noncommutative linear logic they may be defined as A ⧀ B = A ⊗ B^{⊥} and A ⧁ B = ^{⊥}A ⊗ B. We shall often abuse terminology and refer to all four connectives as “implications” or “homs”: the context should make the usage clear.

[figure: ⊗; A; B; A ⊗ B; (⊗ I); ⊗; A ⊗ B; A; B; (⊗ E); ⊤; ⊤; (⊤ I); ⊤; ⊤; (⊤ E)]
[figure: ⊕; A; B; A ⊕ B; (⊕ I); ⊕; A ⊕ B; A; B; (⊕ E); ⊥; ⊥; (⊥ I); ⊥; ⊥; (⊥ E)]
[figure: {− \atop ∘}; C; B; A; Γ; Δ; A {− \atop ∘} B; ({− \atop ∘} I); {− \atop ∘}; B; A; A {− \atop ∘} B; ({− \atop ∘} E); ∘−; C; A; B; Γ; Δ; A ∘− B; (∘− I); ∘−; A; A ∘− B; B; (∘− E)]

[figure: ⧁; B; A ⧁ B; A; (⧁ I); ⧁; C; B; A; Γ; Δ; A ⧁ B; (⧁ E); ⧀; A; A ⧀ B; B; (⧀ I); ⧀; C; A; B; Γ; Δ; A ⧀ B; (⧀ E)]

C is an arbitrary subcircuit with appropriate in/outputs

Table 1: Links for proof circuits

• The following adjunctions summarize these points:

\begin{matrix}A ⊗ B ⟶ C & C ⟶ A ⊕ B \\ B ⟶ A {− \atop ∘} C & A ⧁ C ⟶ B \\ A ⊗ B ⟶ C & C ⟶ A ⊕ B \\ A ⟶ C ∘− B & C ⧀ B ⟶ A \end{matrix}

Γ ⊢ Δ, A, Δ′ Γ′, A, Γ′′ ⊢ Δ′′

Γ′, Γ, Γ′′ ⊢ Δ, Δ′′, Δ′ (cut)

if Γ′ or Δ = ϕ and Γ′′ or Δ′ = ϕ

{Γ, A, B, Γ′ ⊢ Δ \atop Γ, A ⊗ B, Γ′ ⊢ Δ} (⊗ L)  Γ ⊢ Δ, A, Δ′ Γ′ ⊢ Δ′′, B, Δ′′′ Γ, Γ′ ⊢ Δ′′, Δ, A ⊗ B, Δ′′′, Δ′ (⊗ R)
if Δ′ = Δ′′ = ϕ or Γ = Δ′ = ϕ or Γ′ = Δ′′ = ϕ

Γ, A, Γ′ ⊢ Δ Γ′′, B, Γ′′′ ⊢ Δ′ Γ′′, Γ, A ⊕ B, Γ′′′, Γ′ ⊢ Δ, Δ′ (⊕ L)  {Γ ⊢ Δ, A, B, Δ′ \atop Γ ⊢ Δ, A ⊕ B, Δ′} (⊕ R)

if Γ′ = Γ′′ = ϕ or Γ′′ = Δ′ = ϕ or Γ′ = Δ = ϕ

{Γ, Γ′ ⊢ Δ \atop Γ, ⊤, Γ′ ⊢ Δ} (⊤ L)  ⊢ ⊤ (⊤ R)

⊥ ⊢  (⊥ L)  {Γ ⊢ Δ, Δ′ \atop Γ ⊢ Δ, ⊥, Δ′} (⊥ R)

Γ ⊢ Δ, A Γ′, B, Γ′′ ⊢ Δ′ Γ′, Γ, A {− \atop ∘} B, Γ′′ ⊢ Δ, Δ′ ({− \atop ∘} L)  {A, Γ ⊢ B, Δ \atop Γ ⊢ A {− \atop ∘} B, Δ} ({− \atop ∘} R)

Γ ⊢ B, Δ Γ′, A, Γ′′ ⊢ Δ′ Γ′, A ∘− B, Γ, Γ′′ ⊢ Δ′, Δ (∘− L)  {Γ, B ⊢ Δ, A \atop Γ ⊢ Δ, A ∘− B} (∘− R)

{B, Δ ⊢ A, Γ \atop A ⧁ B, Δ ⊢ Γ} (⧁ L)  Γ, A ⊢ Δ Γ′ ⊢ Δ′, B, Δ′′ Γ, Γ′ ⊢ Δ′, Δ, A ⧁ B, Δ′′ (⧁ R)

{Δ, A ⊢ Γ, B \atop Δ, A ⧀ B ⊢ Γ} (⧀ L)  B, Γ ⊢ Δ Γ′ ⊢ Δ′, A, Δ′′ Γ′, Γ ⊢ Δ′, A ⧀ B, Δ, Δ′′ (⧀ R)

Table 2: Sequent rules corresponding to circuit links 1.1. Remark. (FILL and bilinear logic) There is a restriction that must be placed on the ({− \atop ∘} I) rule for the system FILL: Δ must be empty. As originally presented by de Paiva and Hyland, FILL does not include dual implications but one could add similar restrictions to the other “boxed” rules. This restriction will be discussed further in Section 2, where we shall discuss its semantics, and in Appendix B, where we impose the restriction as part of the sequentialization process. The bilinear logics BILL and GILL have no such restriction.

if Δ or Γ′ = ϕ if Δ or Γ′′ = ϕ

if Γ or Δ′ = ϕ if Γ or Δ′′ = ϕ

In Table 3, we show a number of rewrites associated with these graphical links: reductions, which allow one to eliminate a “redundant” wire joining principal ports for the same operator, and expansions, which allow one to identify a wire carrying a compound formula by “splitting” the wire into “simpler” wires, ultimately into atomic wires. This introduces two nodes for the same operator joined along auxiliary ports. We have only given some of the reductions and expansions in Table 3; the rewrites for ⊕ are like those for ⊗, and the rewrites for ∘−, ⧀, ⧁ are suitable duals to those for {− \atop ∘}. The expansions for the units must have appropriate thinning links, as in [BCST]. The proof that this forms a confluent and strongly normalizing system is beyond the scope of this note (see Remark 1.3).

In addition to the usual reductions and expansions, there are eight equations necessary for handling the boxes in the rules ({− \atop ∘} I), (∘− I), (⧁ E), (⧀ E). These we shall regard as permutation rules in the spirit of natural deduction (or as equalities in the terminology of rewriting). The ones for ({− \atop ∘} I) are given in Table 4; the others are the evident duals. In Table 4, the wires may be multiple or null, as appropriate, and the rectangles represent subgraphs; they need not be valid subcircuits (i.e. sequential subcircuits). For instance, the rectangle G outside the first scope box might be a (⊗ E) link both of whose output wires enter the rectangle C inside the scope box, and dually, the rectangle G outside the third scope box might be a (⊕ I) link. In enlarging or contracting the scope of a box, the only restriction is that the result is a valid circuit. Note how we have indicated the extent of the boxes with dotted lines, as suggested before.

1.2. Remark. (Orienting scope rules) It may seem attractive to orient the scope rules, say in the direction of enlarging scope (left to right) and to use these scope enlargements as reductions. Without the FILL restriction this leads immediately to unresolvable critical pairs between scope enlargements (and in fact, even with the FILL restriction, when there are dual implications, we obtain similar unresolvable critical pairs).

However, there is another source of critical pairs to consider: these arise between scope changes for the linear implications and the reduction rule for the par and, similarly, between the scope changes for the dual implications and the reduction rule for the tensor. These are problematic in all the settings which we consider and prevent the orientation of scope changes in either the enlarging or shrinking direction.

As these critical pairs have a crucial role in determining the coherence results for FILL we shall document them here. In Figure 1 we see an example of a critical pair that cannot be resolved if we treat scope expansion as a reduction rewrite. Notice here there is a ⊕ reduction just above the scope box. However, one can enlarge the scope box so that the scope cuts the wire on which this reduction occurs. Now one can no longer perform the

[figure: ⊕; ⊗; ⊕; ⊕; ⊗; {− \atop ∘}; f; ⊕; ⊕; ⊗; ⊗; ⊕; ⊕; ⊗; ⊗; {− \atop ∘}; {− \atop ∘}; f; f; ⟸; ⟹]

Figure 1: Orienting scope?—scope expansion

[figure: ⊕; ⊗; ⊕; ⊕; {− \atop ∘}; g; ⊕; ⊕; ⊗; ⊗; ⊕; ⊕; {− \atop ∘}; {− \atop ∘}; g; g; ⟸; ⟹]

Figure 2: Orienting scope?—scope reduction

[figure: ⊗; ⊗; ⟹; A; B; A; B; A ⊗ B; A; B; {− \atop ∘}; C; B; A; Γ; Δ; A {− \atop ∘} B; {− \atop ∘}; A; B; C; B; A; Γ; Δ; ⟹; ⊗; ⊗; ⟹; A ⊗ B; A ⊗ B; A; B; A ⊗ B; {− \atop ∘}; A; A {− \atop ∘} B; A {− \atop ∘} B; {− \atop ∘}; B; ⟹; A {− \atop ∘} B; ⊤; ⊤; ⟹; A; A; ⊤; ⊤; ⊤; ⟹]

Table 3: Reductions and expansions for proof circuits

reduction nor can we further enlarge the scope: thus, the pair cannot be resolved.

For the orientation in the direction of shrinking scope we have the analogous critical pair in Figure 2. Here reducing the scope prevents the ⊕ reduction. However the scope cannot be further reduced so as to enable the rule again.

In the commutative logics, as with traditional proof nets, those graphs that correspond to sequent proofs are those that satisfy the “net criterion” of Danos-Regnier: for any setting of the switches, the graph, considered as an undirected graph, must be acyclic and connected. Recall a switch is set by cutting one of the two switchable edges at a switchable link. We shall refer to such graphs as “circuits” (redundantly “valid circuits”)

[figure: {− \atop ∘}; C; G; {− \atop ∘}; C; G; =; {− \atop ∘}; C; G; {− \atop ∘}; C; G; =]

Table 4: Box scope equivalences

or “proof nets”. We refer to graphs which may or may not satisfy the net criterion as “graphs” or (occasionally abusing terminology) simply as “invalid circuits”.

The net criterion for the noncommutative logics is in fact a bit trickier than it first might seem. Traditionally it has been assumed that it suffices to add the criterion that the net be planar, by which we mean that there are no crossings in the graph. In [BCST] we noted that this is not quite right. However, it is still the case that any sequential nets must be planar and satisfy this criterion and, thus, this is a useful and intuitive heuristic in the noncommutative logic. In Appendix B we present a valid sequentialization process. An example of a planar non-sequential circuit which satisfies the net criterion is given in Figure 16. The sequent rules given in Table 2 are all valid in the noncommutative logics; for the commutative logics, where the circuits need not be planar, one must add the exchange rules in the obvious way.

In Figure 3 are some (valid) circuits. The first corresponds to the “evaluation map” A⊗(A{− \atop ∘}B) ⟶ B in an autonomous (monoidal closed) category, the second to the linear distributivity A ⊗ (B ⊕ C) ⟶ (A ⊗ B) ⊕ C in a linearly distributive category, and the third to the triple dual composite map

(((A {− \atop ∘} I) {− \atop ∘} I) {− \atop ∘} I) ⟶ (A {− \atop ∘} I) ⟶ (((A {− \atop ∘} I) {− \atop ∘} I) {− \atop ∘} I)

in a symmetric autonomous category. Switchable links are indicated to help verify the net criterion. Note that the third net is not planar, and indeed the existence of this map depends on symmetry. We leave it as an exercise for the reader to construct the corresponding planar endomorphism on the object (I ∘− (A {− \atop ∘} I)) {− \atop ∘} I; we shall see this net again later.

In Figure 4 we show an example of circuit rewrites. In particular, we illustrate the verification that the composite (A {− \atop ∘} B) ⊕ C ⟶ A {− \atop ∘} (B ⊕ C) ⟶ (A {− \atop ∘} B) ⊕ C reduces to the expanded normal form of the identity wire on (A {− \atop ∘} B) ⊕ C. We shall see that

[figure: ⊗; {− \atop ∘}; ⊗; ⊕; ⊗; ⊕; {− \atop ∘}; {− \atop ∘}; {− \atop ∘}; {− \atop ∘}; {− \atop ∘}; {− \atop ∘}; (1); (2); (3)]

Figure 3: Some examples of proof circuits

this is one half of the exercise of checking that we have an isomorphism (A {− \atop ∘} B) ⊕ C ⟶ A {− \atop ∘} (B ⊕ C) in the circuit category; the other direction is left as an exercise.

1.3. Remark. (Rewrites in terms of directed circuits) The reductions and expansions for the nets for FILL and BILL may be made to look like those for linearly distributive categories, by making the scoping for {− \atop ∘}, ∘−, ⧀, ⧁ implicit, rather than explicit as given by the boxes in the rules for these connectives. This can be done by treating the “halfbox” as a wire, read in a contravariant sense, and so amounts to introducing “directed circuits”. In this approach, the ({− \atop ∘}) rules would look like this

[figure: {− \atop ∘}; A; B; A {− \atop ∘} B; {− \atop ∘}; A {− \atop ∘} B; A; B]

[figure: {− \atop ∘}; {− \atop ∘}; ⊕; {− \atop ∘}; {− \atop ∘}; ⊕; (A {− \atop ∘} B) ⊕ C; ⊕; ⊕; A {− \atop ∘} (B ⊕ C); (A {− \atop ∘} B) ⊕ C; ⟹; {− \atop ∘}; ⊕; {− \atop ∘}; ⊕; ⊕; ⊕; {− \atop ∘}; {− \atop ∘}; ⊕; ⊕; ⟹; {− \atop ∘}; {− \atop ∘}; ⊕; ⊕; =]

Figure 4: An example of circuit rewrites

and the {− \atop ∘} reduction then may be given as

[figure: {− \atop ∘}; {− \atop ∘}; ⟹; which induces; {− \atop ∘}; C; B; A; Γ; Δ; {− \atop ∘}; A; B; C; B; A; Γ; Δ; ⟹]

which is essentially the reduction in Table 3. There is a similar expansion rule, which expands a {− \atop ∘} wire into a “loop”, one side of which is contravariant, the other side being covariant. The other implications are handled similarly.

This version of the nets and particularly of the rewrites is very intuitive, especially as it seems just like the familiar context of circuits from [BCST], and so makes circuit manipulations quite simple. There is a problem with losing the boxes, however, for the scoping they provide is quite vital for FILL. In particular, the sequentialization process does not to work without some way to keep track of the scope of the implication connectives, which the sequent calculus does automatically. The main symptom that sequentiality is a problem with these directed nets is their implicit “∗-autonomous” structure. This is harmless in the bilinear context, as these settings are (as we shall shortly see) ∗- autonomous, however, for FILL, this is quite disastrous as in general there is not even a faithful (structure preserving) functor into a ∗-autonomous category. Thus, even though these directed circuits do provide an adequate notation for bilinear categories, we shall continue to use the scope boxes as they can also express correctly the semantics of FILL.

2. Logical theories and categorical doctrines

We shall deal with several logical theories (and the corresponding categorical structures) in this paper. The full system using all the binary connectives ⊗, ⊕, {− \atop ∘}, ∘−, ⧀, ⧁ and the constants ⊤, ⊥ and using the sequent rules of Table 2 (or equivalently the circuit links of Table 1) is Lambek’s bilinear logic BILL. We also consider the fragment of bilinear logic which omits the connectives ⧀, ⧁; we call this noncommutative logic GILL.^{1} If we add the permutation rule to GILL (and so may omit ∘−, which is then equivalent to {− \atop ∘} in the evident way), we have commutative GILL. If we add the restriction “Δ must be empty” to the ({− \atop ∘} I) link (or equivalently, the ({− \atop ∘} R) sequent rule) in commutative GILL we obtain de Paiva and Hyland’s system FILL. If we add this restriction and the corresponding restriction to the (∘− R) rule to noncommutative GILL, we get noncommutative FILL.

2.1. Remark. (Cut elimination and FILL) Neither the commutative nor noncommutative versions of FILL, if presented as a sequent calculus (as in Table 2, with the restriction of Remark 1.1) satisfies cut elimination. Schellinx [Sc91] provides an example^{2} of how cut elimination fails in FILL. In [HP93] Hyland and de Paiva argue that if one wants a computationally significant sequent calculus, then cut elimination is important. To recapture the result, they introduce a more general ({− \atop ∘} R) rule in which the Δ need not be empty (ı.e. the sequent rule ({− \atop ∘}R) from Figure 11 in their paper). Their new rule, however, has an important side condition involving the term calculus with which they annotate their proofs. Using this rule they prove a cut elimination theorem and show that any derivation using the more general rule can be transformed, at the cost of introducing cuts, into one which uses the restricted rule in which Δ must be empty.

While neither the sequent calculus nor its cut elimination process are primary concerns of this paper, it is of some interest to understand these different perspectives, and in particular how the resolution in [HP93] is achieved. In this paper we also claim a normalization result, but it is based in the natural deduction style. We would argue that the term calculus used to annotate the proofs in [HP93] consists essentially of representations of these natural deduction proofs. The reason they can be used to recapture cut elimination is precisely because the underlying representation can be normalized. Of course, this does not mean that [HP93] lacks interest: the cut elimination procedure they developed translates into an algorithm for reducing natural deduction proofs which is more detailed than our specification of reduction in terms of rewrite rules. In particular, it provides information about how the permuting conversions introduced by scope should be manipulated during reduction.

1“Grishin Implicative Linear Logic”: The distinguishing feature of GILL as opposed to FILL is the sequent axiom corresponding to the costrength θ^{−1} defined below, whose importance, as Lambek [L93] has pointed out, was first noticed by Grishin [Gr83], who in addition anticipated linear and bilinear logic by several years.

2In fact in [Sc91] the example given uses additives: however, the author, in a private communication, showed us that essentially the same example worked for FILL without additives.

In this remark we shall refer to the system proposed in [HP93] as the annotated sequent calculus, and the system described in this paper as unannotated. An example where the normal form has a cut which cannot be removed in our unannotated sequent calculus for FILL is as follows:

[figure: ⊕; ⊗; {− \atop ∘}]  \begin{matrix}B ⊕ C ⊢ B, C & {A, B ⊢ A ⊗ B \atop B ⊢ A {− \atop ∘} (A ⊗ B)} \\ B ⊕ C ⊢ A {− \atop ∘} (A ⊗ B), C \end{matrix}

(In this discussion we shall abbreviate sequent derivations by omitting sub-derivations of sequents of the form A ⊕ B ⊢ A, B and A, B ⊢ A ⊗ B.)

To eliminate this cut we would want to move it up the right branch of the derivation. However, the FILL restriction inhibits us from performing the desired cut elimination step. In the annotated calculus this problem is avoided by keeping track of the fact that C is “independent” of the proposition to be bound by the implication so that the appropriate implication can still be formed. In the natural deduction system represented by the circuits of this paper, this circuit is in normal form, even though it seems to contain a “cut”; no reduction may be performed on this circuit.

The cut elimination process on the unannotated sequent calculus tends to enlarge scopes. Thus, it is worth looking again at the critical pair of Figure 1, which illustrated why scope enlargement is not a viable rewrite rule. The circuits in that Figure have the following sequentializations.

The “vertex” of the critical pair corresponds to the following deduction.

\begin{matrix}\begin{matrix}{X ⊢_{f} A, B, C \atop X ⊢ A ⊕ B, C} & \begin{matrix}Y, A ⊢ Y ⊗ A & B ⊢ B \\ Y, A ⊕ B ⊢ Y ⊗ A, B \end{matrix} \\ Y, X ⊢ Y ⊗ A, B, C \end{matrix} ; Y, X ⊢ (Y ⊗ A) ⊕ B, C & {Z, (Y ⊗ A) ⊕ B ⊢ Z ⊗ ((Y ⊗ A) ⊕ B) \atop (Y ⊗ A) ⊕ B ⊢ Z {− \atop ∘} (Z ⊗ ((Y ⊗ A) ⊕ B))} \\ Y, X ⊢ Z {− \atop ∘} (Z ⊗ ((Y ⊗ A) ⊕ B)), C \end{matrix}

First, in the left fork in the critical pair, the scope is enlarged. The corresponding cut elimination step moves the ({− \atop ∘} R) step, producing the following deduction. (We abbreviate this somewhat, removing the subderivation of the linear distributivity Z, Y, A⊕ B ⊢ Z ⊗ ((Y ⊗ A) ⊕ B).) Note the cut cannot be moved further after this step.

\begin{matrix}{X ⊢_{f} A, B, C \atop X ⊢ A ⊕ B, C} & {Z, Y, A ⊕ B ⊢ Z ⊗ ((Y ⊗ A) ⊕ B) \atop Y, A ⊕ B ⊢ Z {− \atop ∘} (Z ⊗ ((Y ⊗ A) ⊕ B))} \\ Y, X ⊢ Z {− \atop ∘} (Z ⊗ ((Y ⊗ A) ⊕ B)), C \end{matrix}

Second, in the right fork in the critical pair, the scope is not enlarged but instead a ⊕ reduction is performed. The corresponding cut elimination step produces the following deduction. Note again that no further movement of the cut is possible without violating the FILL restriction. It is also worth noting that the circuit corresponding to this derivation is the normal form of the original derivation; that is, there is no possible further reduction that can be done, even if one rearranges the scope boxes. Once again, we see that normal forms may contain “essential cuts”.

\begin{matrix}\begin{matrix}Y ⊢ Y & X ⊢_{f} A, B, C \\ Y, X ⊢ Y ⊗ A, B, C \end{matrix} ; Y, X ⊢ (Y ⊗ A) ⊕ B, C & {Z, (Y ⊗ A) ⊕ B ⊢ Z ⊗ ((Y ⊗ A) ⊕ B) \atop (Y ⊗ A) ⊕ B ⊢ Z {− \atop ∘} (Z ⊗ ((Y ⊗ A) ⊕ B))} \\ Y, X ⊢ Z {− \atop ∘} (Z ⊗ ((Y ⊗ A) ⊕ B)), C \end{matrix}

The point is that these unannotated derivations give rise to equivalent proofs yet the unannotated cut elimination process cannot transform them into the same derivation without “backwards” steps. Of course, the annotated system will.

From our perspective, the system GILL (in either commutative or noncommutative guise) is more natural than FILL. The point about GILL is that we have a connection between the implication, or internal hom, {− \atop ∘} and the par ⊕, given by tensorial strength. In FILL on the other hand, the connection between the autonomous structure and the linearly distributive structure is not as strong (pun intended), as we shall see below. However, GILL is undoubtedly not at all “intuitionistic”, unlike FILL. In symmetric GILL (A {− \atop ∘} ⊥) {− \atop ∘} ⊥ is isomorphic to A for any A, so that GILL is “classical”, in that we have an involutive negation. In fact, GILL is precisely full classical multiplicative linear logic: the logical doctrine corresponding to GILL is just ∗-autonomous categories, again, in either commutative or noncommutative guise. This may perhaps be expected, as strength and costrength have generally been seen to be the mediators of implicit duality in this series of papers.

The distinction between FILL and GILL in fact represents the tip of an interesting digression, which is not discussed in [HP93], but some of which may be found in [L93]. If a linearly distributive category has as well closed monoidal structure (with respect to the tensor ⊗), then the tensorial strength represented by the linear distributivities A⊗(B⊕C) ⟶ (A ⊗ B) ⊕ C automatically extends via the adjunction defining the closed monoidal structure to a strength or “distributivity”: (A {− \atop ∘} B) ⊕ C ⟶ A {− \atop ∘} (B ⊕ C). In fact, this latter natural family provides an equivalent presentation of the linear distributive structure. The general ({− \atop ∘} I) rule we give in Table 1 (or equivalently the ({− \atop ∘} R) rule in Table 2) corresponds categorically to having an inverse (costrength) to this family of maps: A {− \atop ∘} (B ⊕ C) ⟶ (A {− \atop ∘} B) ⊕ C. We can check that in the category of circuits with the more general “boxed” links we do indeed have such an isomorphism; half of this exercise is illustrated in Figure 4. This strength isomorphism characterizes the logical systems of bilinear logic BILL and its fragment GILL.

We shall formalize this discussion in the following definitions. First, we shall construct the following canonical morphism in a linearly distributive autonomous category:

(A {− \atop ∘} B) ⊕ C ⟶^{θ} A {− \atop ∘} (B ⊕ C)

= (A {− \atop ∘} B) ⊕ C ⟶^{θ_{1}} A {− \atop ∘} [(A ⊗ (A {− \atop ∘} B)) ⊕ C]

⟶^{θ_{2}} A {− \atop ∘} (B ⊕ C)

where θ_{1} corresponds under the “internal hom” adjunction to the linear distribution A ⊗ [(A{− \atop ∘}B)⊕C] ⟶ [A⊗(A{− \atop ∘}B)]⊕C and θ_{2} is the evident map induced by the “evaluation” morphism A ⊗ (A {− \atop ∘} B) ⟶ B. The map θ is in fact a strength morphism, in that the following two diagrams commute:

[figure: ((A {− \atop ∘} B) ⊕ C) ⊕ D; θ ⊕ D; (A {− \atop ∘} (B ⊕ C)) ⊕ D; θ; A {− \atop ∘} ((B ⊕ C) ⊕ D); a; A {− \atop ∘} a; (A {− \atop ∘} B) ⊕ (C ⊕ D); θ; A {− \atop ∘} (B ⊕ (C ⊕ D))]

[figure: (A {− \atop ∘} B) ⊕ ⊥; θ; A {− \atop ∘} (B ⊕ ⊥); u; A {− \atop ∘} u; A {− \atop ∘} B]

It is a pleasant exercise to show that these diagrams follow from the adjointness and the linear distributivity—the simplest proof is to write the corresponding circuits and reduce them to expanded normal form. The ease of such calculations is after all the point of these papers, but the determined traditionalist might want to do a diagram chase instead.

Note that if θ has an inverse θ^{−1}, then θ^{−1} is a costrength morphism A {− \atop ∘} (B ⊕ C) ⟶ (A {− \atop ∘} B) ⊕ C, in that the corresponding dual diagrams must commute.

This construction extends in the obvious way to the other internal homs ∘−, ⧀, ⧁, if they exist in the category, so we have a strength A ⊕ (B ∘− C) ⟶ (A ⊕ B) ∘− C, and costrengths A ⧁ (B ⊗ C) ⟶ (A ⧁ B) ⊗ C and (A ⊗ B) ⧀ C ⟶ A ⊗ (B ⧀ C). It is these canonical morphisms that we shall require to be isomorphisms in the next definition.

2.2. Definition. A bilinear category, or BILL category, is a (possibly nonsymmetric) linearly distributive category whose tensor has left adjoints in both coordinates, and whose cotensor has right adjoints in both coordinates, in the sense indicated:

\begin{matrix}A ⊗ B ⟶ C & C ⟶ A ⊕ B \\ B ⟶ A {− \atop ∘} C & A ⧁ C ⟶ B \\ A ⊗ B ⟶ C & C ⟶ A ⊕ B \\ A ⟶ C ∘− B & C ⧀ B ⟶ A \end{matrix}

Furthermore, the canonical morphisms discussed above, corresponding to the linear distributivities, are required to have inverses:

A {− \atop ∘} (B ⊕ C) ⟶ (A {− \atop ∘} B) ⊕ C

(A ⊕ B) ∘− C ⟶ A ⊕ (B ∘− C)

(A ⧁ B) ⊗ C ⟶ A ⧁ (B ⊗ C)

A ⊗ (B ⧀ C) ⟶ (A ⊗ B) ⧀ C

A symmetric bilinear category is a bilinear category whose tensor and cotensor are symmetric.

2.3. Definition. A Grishin category, or GILL category, is a linearly distributive category with internal homs {− \atop ∘}, ∘− as above, with inverses to the relevant canonical morphisms as in Definition 2.2. A symmetric Grishin category is a Grishin category whose tensor and cotensor are symmetric.

2.4. Definition. A full multiplicative category, or FILL category, is a linearly distributive category which is left and right monoidal closed (i.e. having both internal homs {− \atop ∘}, ∘−). A symmetric full multiplicative category is a symmetric linearly distributive monoidal closed category.

In the definitions above, we shall frequently let the context determine whether we mean the commutative (symmetric) or noncommutative variants. Generally the noncommutative case is our default.

We shall show below in Proposition 4.1 that GILL is equivalent to classical multiplicative linear logic. This means that the doctrines of GILL, BILL, and (noncommutative) ∗-autonomy are all equivalent. Notice, of course, that this collapse of notions does not include FILL.

3. Coherence

Our main concern in considering circuits for linearly distributive categories (and similarly for the other notions of monoidal categories we are considering here) was to obtain coherence theorems. If we exclude consideration of the units for the tensors ⊗, ⊕, the matter is fairly straightforward, even trivial. The notion of expanded normal form corresponds precisely to the notion of Kelly-Mac Lane graph, and so two morphisms are equal if and only if they correspond to circuits with the same expanded normal form. See [B92, BCST] for a general exposition of the ideas here, and for some specific applications to various sorts of monoidal categories. This approach also settles the other standard coherence question: given two objects, is there a morphism between them? For given a Kelly-Mac Lane graph, one can construct a canonical circuit structure in expanded normal form (essentially the subformula tree) and then check if it satisfies the criterion for net validity.

The coherence question (equality of maps) becomes considerably less trivial if one includes the units in the structure. It has recently been shown that the addition of the units to the multiplicative system of linear logic greatly adds to the complexity of the system [LW92]. This is reflected in the more complicated coherence result. Indeed, the classical treatments of coherence tend to avoid or restrict the units—one may consult [J90] for a rare exception. It is precisely to solve the coherence question that we introduce thinning links. Without thinning links the unit expansion rules lead to the situation that inequivalent circuits (i.e. circuits corresponding to unequal morphisms in the free category) can have the same expanded normal form. However, with thinning links, we no longer have a unique expanded normal form representative of each equivalence class; there may be several expanded normal forms in an equivalence class that differ in the wiring of their thinning links. In the present context we have in addition the scope equivalences to consider. A moment’s thought will convince the reader that these equivalences and rewirings give the only kinds of differences equivalent expanded normal forms can display.

So we have to account for these “permuting conversions”. In [BCST] we developed a set of “surgery” rules on nets, which in addition to the reductions and expansions above involved a number of rewiring rules for thinning links, and showed that these allowed a subnet with a thinning link attached to an input or output wire to be replaced with the same subnet with the thinning link reattached to some other input or output wire. Planarity must be respected in the noncommutative case. As a corollary, we obtain Trimble’s Rewiring Theorem [T94]: one can rewire the thinning links without altering the identity of the morphism precisely when the rewiring does not leave the empire of the unit involved. It is straightforward to apply this to the situations at hand, say for instance, for bilinear categories, and so also for full multiplicative categories.

In Table 5 we present a representative sample of the rewiring rules for the tensor unit ⊤ in graphical notation. A complete set of rewiring rules may be obtained by generating rules for all non-switching links corresponding to rules for the non-switching links shown, and similarly for switching links, and by applying the obvious dualities. There is a dual set of rewirings for the cotensor unit ⊥. Note that most of these rules respect planarity of graphs; only the rules specifically required for the commutative case are non-planar: these are the two rewirings in the last row of Table 5. In the noncommutative case we drop the rules in the last row of the table. A full set of rules for the linearly distributive case is in [BCST]; a full set of rules for the present context may be obtained from those by analogy.

There is one further important restriction we must place on the rewirings of Table 5: a rewiring can only be applied to a proof net if it preserves net validity; that is, if after the rewiring, one still has a proof net. The same restriction is also placed on the scope equivalences. Therefore, there is a hidden cost in applying these rules: namely one must check that the alteration yields a sequential net. In fact for most of our rules this is automatic and only those rules which involve rewiring past a switching link do not in general preserve net validity and so require this extra checking.

The key component in arriving at the coherence results of [BCST] is a pair of propositions (3.1, 3.2) that state that the rewirings on components (represented by boxes in Table 5) apply as well to arbitrary subnets, in both the commutative and noncommutative cases. In the noncommutative case we only need the planar rewrites from Table 5, but in addition it is necessary treat the unit reductions from Table 3 as equalities. This, as discussed below in Remark 3.4, complicates the determination of equality (indeed establishing a decision procedure is still an open problem). In the commutative case we do not need the unit reductions as equalities (they remain as rewrites), but we must add the non-planar rewrites in the last row of the Figure 5. These results easily generalize to the present context; in particular, for noncommutative bilinear logic we can state the following proposition. Note that by “box rewiring rules” we mean the rewirings involving arbitrary components. Proofs of the following results may be found in [BCST]:

3.1. Proposition. (Rewiring Theorem) The box rewiring rules apply to any subnet of a planar net, using only the planar rewirings and the unit reductions (as equations). For non-planar nets, the box rewiring rules apply to any subnet of a net, using only the unit rewirings.

As an immediate corollary we can derive the Empire Rewiring Theorem, which characterizes the unit rewirings in terms of the notion of empire [Gi87]. The extension of the definition of empire in the present context—at least in the commutative case—is straightforward, and is left to the reader. In the noncommutative case, the main problem is in defining the notion of empire. We shall not address this question here for two reasons: primarily because the essence of the result we want in this case is already carried by Proposition 3.1, and secondly because this would be a digression beyond the intended scope of this paper.

3.2. Proposition. (Empire rewiring) In a non-planar net a thinning link can be moved to any wire in its empire.

So in essence this says that for symmetric bilinear logic, the empire of a thinning link is the largest set of wires to which the thinning link can be moved while preserving the Lambek equivalence of proofs. We should mention the effect of the boxes: in BILL and GILL units and counits can be moved freely inside boxes (when the box is in the empire). However, in FILL there is an important restriction, introduced by the requirement to remain sequential: counit thinnings cannot be moved in or out of boxes.

These rewirings are the key to characterizing equality of morphisms in free bilinear categories (and FILL categories), since these free structures are given by circuits. More

[figure: ⧁; A; B; ⊤; A ⧁ B; ⊤; ⧁; A; B; ⊤; A ⧁ B; ⊤; =; ⊤; ⊤; ⊥; ⊥; A; ⊤; ⊤; ⊥; ⊥; A; =; ⊤; ⊤; ⊥; ⊥; A; =]

[figure: {− \atop ∘}; A; B; A {− \atop ∘} B; ⊤; =; ⊤; {− \atop ∘}; A; B; A {− \atop ∘} B; ⊤; ⊤; ⊤; ⊤; A; ⊤; ⊤; A; =; ⊤; ⊤; A; =; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤; z_{1}; z_{2}; z_{1}; z_{2}; z_{1}; z_{2}]

[figure: {− \atop ∘}; A {− \atop ∘} B; ⊤; ⊤; {− \atop ∘}; A {− \atop ∘} B; ⊤; ⊤; =; f; f; B; A; Γ; Δ; B; A; Γ; Δ; ⊤; ⊤; =; f; A; Δ; B; ⊤; ⊤; f; A; Δ; B]

[figure: ⊤; ⊤; f; ⊤; ⊤; f; =; Γ_{1}; A; B; Γ_{2}; Δ; ⊤; Γ_{1}; A; B; Γ_{2}; Δ; ⊤; ⊤; =; Γ; A; f; Δ; B; ⊤; ⊤; Γ; A; f; Δ; B]

[figure: ⊤; =; A; A; ⊤; ⊤; ⊤; ⊤; ⊤; =; Γ; A; B; f; Δ_{1}; Δ_{2}; ⊤; ⊤; Γ; A; B; f; Δ_{1}; Δ_{2}]

Table 5: Some unit rewirings precisely, given a set C of components and a set E of equivalences, the induced set of proof nets with one input and one output, quotiented by the equivalences generated by E and the reductions, expansions, and rewirings described above are the morphisms of a category NetE (C) whose objects are the formulas of the theory. If we restrict to the planar nets and equivalences, we get a category PNetE (C). This may be done for either bilinear logic, GILL, or FILL, starting with the appropriate formulas for generating the objects, and using the appropriate links for generating the circuits (morphisms). It is then a straightforward verification that the resulting categories are indeed categories of the appropriate doctrine.

For example, in the case of noncommutative bilinear logic, PNetE (C) is a bilinear category, as defined in Definition 2.2. More importantly, however, these categories of circuits are the free categories with appropriate structure generated by the components C and equivalences E. We shall state this for the bilinear case, but this restricts to the fragments FILL and GILL of bilinear logic as well.

3.3. Theorem. NetE (C) is the free symmetric bilinear category generated by the polygraph C and the equations E. Similarly, PNetE (C) is the free (nonsymmetric) bilinear category generated by this data.

3.4. Remark. (Decision procedures) So to establish the equality of morphisms in (say) the free bilinear category generated by a polygraph C, we need only use the equivalence of proofs in Net_{∅}(C) or PNet_{∅}(C), as appropriate. To provide a decision procedure for these nets we show that the basic net equivalences form an expansion/reduction system modulo equations, as defined in Appendix A of [BCST]. That proof can be extended to the present context; the main technical point is that the scope equivalences must be added to the equations. The proof from [BCST] must be modified to account for that; this essentially amounts to showing that with this enlarged E, X ∪ R is X -reducing and locally E-confluent. The key step in the proof in [BCST] involved defining an equivalence sk[ν](e^{∗}) induced by an equivalence e^{∗} and a reduction or expansion ν. In most cases this is immediate, and if e^{∗} involves any scope equivalences, they may be mimicked in defining sk[ν](e^{∗}).

We can then show as in [BCST] that this implies uniqueness of expanded normal forms modulo the equivalences given by the rewirings, and in the noncommutative case modulo the equivalences given by the rewirings and the unit reductions. From this we can arrive at a decision procedure in the commutative case; in the noncommutative case the matter is still open and complicated by the form of the rewiring allowed in this situation. The decision procedure for the commutative case is this: we define the skeleton of a net as the graph obtained from the net by removing all thinning links. Any net can be reduced to a net whose skeleton is completely reduced. This may involve scope equivalences. Two nets then are equivalent if when so reduced they have the same skeleton, and if the thinning links of one such reduced net can be rewired to the configuration of the other. When scope boxes are present changes of scope are also allowed. As there are only a finite number of possible configurations of the thinning links and scopes on a skeleton, a search of equivalent configurations is possible. Of course, this decision procedure as sketched would not be computationally feasible and, as mentioned earlier, there are open questions about its complexity.

In the noncommutative case, the presence of the unit reductions as rewirings allows for the introduction of “barbells” via “reverse unit reduction”, which make it possible to have an infinite number of possible rewirings on a skeleton. Thus, the above algorithm cannot be applied directly. While it seems likely that determining the equivalence of two configurations of thinning links on a skeleton in the noncommutative logic is decidable this is still an open problem. Notice that these complications arise entirely from the presence of thinning—for unit-free nets coherence is trivial, as one might expect from past results in this field.

3.5. Example. In [BCST] we illustrated a famous test case of coherence for autonomous categories; here we will present this example in a version that is valid in the noncommutative case (and so for instance in the free bilinear category generated by a set of objects). When does the following “triple-dual” diagram commute?

[figure: (I ∘− (A {− \atop ∘} I)) {− \atop ∘} I; k_{A} {− \atop ∘} id; (A {− \atop ∘} I); id; k′_{A{− \atop ∘}I}; (I ∘− (A {− \atop ∘} I)) {− \atop ∘} I]

where k, k′ are the evident canonical maps (adjoints to the evaluation maps).

We leave it as an exercise to show that in the case when I = ⊤ (but A arbitrary) each discharged unit has a trivial (singleton) empire, and so no rewiring is possible; hence the diagram does not commute. It is also an easy exercise to show that the diagram does commute if I = ⊥. But now consider the case where A = I = ⊤; in this case it is possible to rewire the thinning link that comes from A = ⊤ first, which allows the other units to be rewired, whereupon we rewire this first back to its original position. Figure 5 shows the expanded normal form of the circuit representing the composite map. The reader might like to try to rewire this to obtain the expanded normal form of the identity map: a similar calculation is carried out in [BCST].

4. From GILL to BILL

Next we use the circuits to show that GILL is multiplicative linear logic. That is, we show that the standard definition of negation is in fact involutive, so that a Grishin category is a linearly distributive category with negation, and so ∗-autonomous [CS91]. This is valid in both commutative and noncommutative cases; we shall present the noncommutative case as an illustration.

[figure: ∘−; {− \atop ∘}; {− \atop ∘}; {− \atop ∘}; ∘−; {− \atop ∘}; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤]

Figure 5: A valid circuit for the triple dual map

Theory and Applications of Categories, Vol. 3, No. 5 110

4.1. Proposition. A Grishin category is a linearly distributive category with negation. Proof. We define the two negation operators in the standard manner:

⊥A = ⊥ ∘− A A^{⊥} = A {− \atop ∘} ⊥

We must have maps

\begin{matrix}^{⊥}A ⊗ A ⟶^{γ_{A}^{L}} ⊥ & A ⊗ A^{⊥} ⟶^{γ_{A}^{R}} ⊥ \\ ⊤ ⟶^{τ_{A}^{L}} A^{⊥} ⊕ A & ⊤ ⟶^{τ_{A}^{R}} A ⊕^{⊥}A \end{matrix}

As circuits this amounts to having derived links with these shapes:

[figure: ¬; ¬; A^{⊥}; A; ^{⊥}A; A; A; A^{⊥}; A; ^{⊥}A]

These are given as follows:

[figure: {− \atop ∘}; ∘−; ∘−; {− \atop ∘}; A^{⊥}; A; ^{⊥}A; A; A; A^{⊥}; A; ^{⊥}A; ⊥; ⊥; ⊥; ⊥]

Next we must verify certain coherence conditions, which are equivalent to the following circuit equivalences:

[figure: ¬; ¬; A; A; A; A^{⊥}; A; ^{⊥}A; ^{⊥}A; A; ^{⊥}A; ¬; A^{⊥}; A; ¬; A^{⊥}; ⇐; ⇒; ⇐; ⇒; A; A^{⊥}; ^{⊥}A]

These are consequences of the circuit rewrites already defined. For example, in Figure 6 we show how the rewrites for A^{⊥} are derived, the ones for ^{⊥}A being dual.

It is worth pointing out why this proof fails for FILL. First note that the τ nets are not sequential for FILL, because the “Δ is empty” criterion is violated. Furthermore, in Figure 6, for the expansion rewrite note the use of the rewiring of the thinning link and of the box-rewrite, to pull the ({− \atop ∘} E) link outside the scope box. This step is impossible in FILL, as it introduces a circuit for which the “Δ is empty” criterion is violated, even though one started with circuit which did not violate the criterion.

To derive the obvious corollary, note that in the symmetric case this implies a Grishin category is ∗-autonomous [CS91], and in the nonsymmetric case this implies that a Grishin category is bilinear. In other words, in either the symmetric or nonsymmetric case the following notions, interpreted appropriately vis à vis symmetry, coincide: Grishin category, bilinear category, ∗-autonomous category, linearly distributive category with negation. The standard definitions, i.e. those that we mentioned in introducing the operators ⧀ and ⧁, do in fact work, and it is easy to verify that these defined operators have appropriate induced introduction and elimination links, and appropriate reduction and expansion rewrites. To illustrate this, in Figures 7 and 8 we show the derived rules and rewrites for ⧁, where A ⧁ B is defined as (⊥ ∘− A) ⊗ B, viz. ^{⊥}A ⊗ B. Of course, ⧀ is dual.

In addition, in a bilinear category, although one might be tempted to define two other negation operators, these turn out to be isomorphic to the ones already defined. More precisely, if we define ^{⊤}A = ⊤ ⧀ A and A^{⊤} = A ⧁ ⊤, then, as Lambek [L93] showed in the posetal case, in any bilinear category we have isomorphisms ^{⊤}A ≅ A^{⊥} and A^{⊤} ≅ ^{⊥}A. The circuits corresponding to ^{⊤}A \overrightarrow{⟵} A^{⊥} are shown in Figure 9; checking these are inverses is an easy exercise in circuit rewriting.

There are a number of other isomorphisms that hold in any bilinear category; here is a sample that ought to help fix the relationships between the connectives. We shall leave

[figure: {− \atop ∘}; {− \atop ∘}; A^{⊥}; A; A; A^{⊥}; ⊥; ⊥; {− \atop ∘}; A; ⊥; ⟹; ⊥; ⊥; ⟹; A; A; {− \atop ∘}; A^{⊥}; ⊥; {− \atop ∘}; A^{⊥}; A; ⊥; {− \atop ∘}; A^{⊥}; ⊥; =; {− \atop ∘}; A^{⊥}; A; {− \atop ∘}; A^{⊥}; ⟹; ⟹; A^{⊥}]

Figure 6: A^{⊥} rewrites

the verifications to the reader.

(A ⊕ B)^{⊥} ≅ B^{⊥} ⊗ A^{⊥} ^{⊥}(A ⊕ B) ≅ ^{⊥}B ⊗^{⊥}A

(A ⊗ B)^{⊥} ≅ B^{⊥} ⊕ A^{⊥} ^{⊥}(A ⊗ B) ≅ ^{⊥}B ⊕^{⊥}A

(A ⧁ B)^{⊥} ≅ B {− \atop ∘} A ≅ B^{⊥} ∘− A^{⊥}

⊥(A ⧀ B) ≅ B ∘− A ≅ ^{⊥}B {− \atop ∘}^{⊥}A

⊥(A^{⊥}) ≅ A (^{⊥}A)^{⊥} ≅ A

In the commutative case, of course, the two negations are the same, and much of this variety collapses.

[figure: ⧁ links:; ^{⊥}A; ∘−; ⊥; ⊗; ∘−; A ⧁ B; ⊥; ⊗; A; B; C; Γ; Δ; A ⧁ B; B; A; (⧁ I); (⧁ E)]

Figure 7: ⧁ derived links

5. From FILL to GILL; nuclearity

In [BCST] we proved that the extension from linearly distributive categories to ∗-autono-mous categories is conservative in the sense that the unit of the appropriate adjunction is fully faithful. So in the present context we can conclude that this conservativity will also apply. In the case of FILL, this extension cannot in general preserve the “internal homs” ({− \atop ∘}, ∘−, ⧁, ⧀) as, for example, in FILL there may be no map A^{⊥⊥} ⟶ A or, for the noncommutative case, no map from any of A^{⊥⊥}, ^{⊥}(A^{⊥}), or (^{⊥}A)^{⊥} to A.

However, there are two other ways of getting ∗-autonomous categories from FILL.^{3} We can keep the same objects but allow the GILL morphisms that come from dropping the FILL restriction on the box rules; this is the free Grishin category generated by the full multiplicative category. Of course, this extension is not full because of the possible lack of a map from A^{⊥⊥} ⟶ A in FILL. It is also not faithful, as the extension requires that A^{⊥⊥} and A are isomorphic; thus it suffices to exhibit a FILL category in which forcing such an isomorphism will cause a significant identification of maps. A simple example of a FILL category is Sets (or indeed any cartesian closed category), where we take ⊗ = × = ⊕: here A^{⊥⊥} is the final object and clearly forcing this to be isomorphic to A must collapse the whole category.

Of more interest, therefore, is the following construction of the full ∗-autonomous subcategory of a FILL category given by isolating “negated” objects. It is technically simpler to approach this subcategory through the nuclear maps:

5.1. Definition. A morphism f: A ⟶ B of a FILL category is nuclear if the “name” of f, ⌈f⌉: ⊤ ⟶ A {− \atop ∘} B, factors through the canonical morphism ϕ_{AB}: A^{⊥} ⊕ B ⟶ A {− \atop ∘} B.

3We shall only deal with the symmetric case in this section, although these comments can be extended to the nonsymmetric case with suitable modifications. See [CS96] for details concerning nuclearity in the noncommutative case.

⧁ reduction:

[figure: ^{⊥}A; ∘−; ⊥; ⊗; ∘−; ⊥; ⊗; A; B; C; Γ; Δ; A ⧁ B; B; A; ⟹; ^{⊥}A; ∘−; ⊥; C; Γ; B; A; ∘−; ⊥; A; Δ; ⟹; ⊥; ⊥; C; B; Δ; A; Γ; ⟹; B; Δ; A; Γ; C]

⧁ expansion:

[figure: ∘−; ⊥; ⊗; ∘−; A ⧁ B; ⊥; ⊗; A ⧁ B; ∘−; ⊥; ⊗; ∘−; ⊥; ⊗; A ⧁ B; A ⧁ B; ⟹; A ⧁ B; ⟹]

Figure 8: ⧁ derived rewrites

[figure: A; {− \atop ∘}; ⊥; {− \atop ∘}; A^{⊥}; ⊥; ⧀; ^{⊤}A; ⊤; ⧀; ⊤; A^{⊥}; ^{⊤}A; A]

Figure 9: Isomorphisms between two negations

We shall call the factoring morphism n_{f}: ⊤ ⟶ A^{⊥} ⊕ B. An object A is nuclear if 1_{A} is nuclear.

[figure: ⊤; ⌈f⌉; A {− \atop ∘} B; n_{f}; ϕ_{AB}; A^{⊥} ⊕ B]

This definition generalizes the definition of nuclear given by Higgs and Rowe [HR89] in the symmetric monoidal closed case.

5.2. Remark. In fact, it is possible to generalize this definition to be applicable in any linearly distributive category. In a linearly distributive category, we shall call a morphism f: A ⟶ B nuclear if and only if there are morphisms τ_{f}: ⊤ ⟶ C ⊕ B and γ_{f}: A ⊗ C ⟶ ⊥ such that the following commutes.

[figure: A; f; B; u_{⊗}^{R}; u_{⊕}^{L}; A ⊗ ⊤; ⊥ ⊕ B; 1 ⊗ τ_{f}; γ_{f} ⊕ 1; A ⊗ (C ⊕ A); δ_{L}^{L}; (A ⊗ C) ⊕ B]

[figure: {− \atop ∘}; {− \atop ∘}; ⊥; {− \atop ∘}; ⊕; A^{⊥} ⊕ B; A {− \atop ∘} B; ϕ_{AB} =; A; A {− \atop ∘} A; A; ⌈1_{A}⌉ =; {− \atop ∘}; {− \atop ∘}; ⊥; ⊕; A^{⊥} ⊕ A; A {− \atop ∘} A; n_{A}; ϕ_{AA} =; A; n_{A}; ⊤]

Figure 10: Circuits for nuclear objects

It is an easy exercise to prove that this definition in a FILL category is equivalent to the definition given above, see [CS96].

It is easy to show that A nuclear is equivalent to A “negated”, meaning that there are morphisms γ, τ satisfying two simple commuting diagrams, as in [CS91]. This is equivalent to requiring of A that it have negation links and rewrites, as described in the proof of Proposition 4.1. In Figure 10 we illustrate the circuits for ϕ_{AB}, ⌈1_{A}⌉ and the composite circuit n_{A}; ϕ_{AA}. This latter is assumed to be equivalent to ⌈1_{A}⌉, according to the commutative triangle above. It is a simple exercise that this is equivalent to the circuit reduction to the identity wire on A described in the proof of Proposition 4.1. It is also easy to check that in the present context this implies the equivalence given by the circuit expansion from the identity wire on A^{⊥}, showing that nuclear objects are the same as negated objects. It is perhaps worth mentioning that in the noncommutative case, this analysis becomes somewhat more subtle, involving the splitting of “nuclear idempotents”, for further details see [CS96].

The set of nuclear maps forms a two-sided ideal that includes (the identity map of) ⊤ and ⊥, and is closed under ⊗, ⊕ and (·)^{⊥}. We shall spare the reader the numerous circuit rewrites involved in proving this, pointing out that they are available in [CS96]; to give the flavour, in Figure 11 we illustrate the key steps in showing that f^{⊥} is nuclear if f is nuclear. In the Figure, the equivalence marked with a ∗ is a consequence of f being nuclear; the rewrite marked with a ‡ depends on the expansion of the wire marked A^{⊥} using the {− \atop ∘} and ⊥ expansions; the rewrite marked † depends on a scope expansion and a rewiring of the ⊥ thinning link.

Thus the full subcategory of nuclear objects, the nucleus, is a linearly distributive category with negation, and so is ∗-autonomous, with ⊥ as the dualising object. The inclusion preserves the internal hom, since we can show that if B is nuclear, A {− \atop ∘} B ≅

[figure: {− \atop ∘}; {− \atop ∘}; ⊥; ⊕; A^{⊥}; ⌈f^{⊥}⌉ ≡^{∗}; A; {− \atop ∘}; n_{f}; {− \atop ∘}; ⊥; B^{⊥}; A^{⊥}; B; ⊥; B^{⊥} {− \atop ∘} A^{⊥}; ⊤; {− \atop ∘}; {− \atop ∘}; ⊥; ⊕; A^{⊥}; ⟸^{†}; A; {− \atop ∘}; n_{f}; {− \atop ∘}; ⊥; B^{⊥}; A^{⊥}; B; ⊥; B^{⊥} {− \atop ∘} A^{⊥}; ⊤; {− \atop ∘}; {− \atop ∘}; ⊥; n_{f^{⊥}}; ϕ =; B^{⊥}; {− \atop ∘}; B^{⊥} {− \atop ∘} A^{⊥}; ⊕; ⊕; ⊕; n_{f}; {− \atop ∘}; ⊥; ⊥; B^{⊥}; B; A^{⊥}; ⊤; B^{⊥⊥} ⊕ A^{⊥}; n_{f}; ⊤; {− \atop ∘}; ⊥; ⟹; {− \atop ∘}; B^{⊥} {− \atop ∘} A^{⊥}; ⊕; B^{⊥}; B; A^{⊥}; ⇑^{‡}]

Figure 11: Circuits for nuclear objects (A ⊗ B^{⊥})^{⊥}, so the inclusion preserves all the FILL structure.

5.3. Proposition. The nucleus of a (commutative) FILL category is ∗-autonomous full subcategory whose inclusion is ( FILL) structure preserving.

A special case of interest occurs when the tensor is cartesian (i.e. ⊗ = ×). In this case the nucleus has its tensor and cotensor cartesian (recall the involution ensures that if one tensor is cartesian the other must be). As the only ∗-autonomous categories with cartesian tensors are Boolean algebras we may conclude that the nucleus is a Boolean algebra. For each object A in this Boolean algebra, the projections A × A ⟶ A are equal which says A is a subterminal object in the larger category. Thus, the nuclear objects are all subobjects of 1 (this includes ⊥).

Recall that any cartesian closed category can be viewed as a FILL category by the identification ⊗ = × = ⊕. Thus, it is of some interest to wonder what the nucleus of a cartesian closed category might be. By the above remarks the nucleus must consist of subobjects of 1. However, the fact that they are negated forces them to be the whole of 1. Thus, these nuclei are trivial.

The nucleus of a FILL category does not always collapse. For example the category of vector spaces (over some field) is a full multiplicative category with the cotensor and tensor coinciding as the usual tensor on vector spaces. The nucleus is the full subcategory of finite dimensional vector spaces.

5.4. Remark. To anticipate the next section of this paper, we point out that this means that the nucleus of any (⊗–)cartesian linearly distributive category is a MIX category. Of course, this does require the generalization of the argument that the nucleus is ∗- autonomous to the linearly distributive case [CS96]. However, as we shall shortly see, a linearly distributive category is MIX if and only if its nucleus is MIX. Thus, this allows the sweeping observation that all (⊗–)cartesian linearly distributive categories are MIX categories.

6. MIX categories

In this section we fill a gap in the literature, by defining what it means for a category to satisfy the MIX rule. There are some variants here: we shall tend to assume that the tensors are symmetric in this section, although all these results do in fact extend to the nonsymmetric case as well. We shall deal not only with the usual MIX rule

Γ ⊢ Δ Γ′ ⊢ Δ′
Γ, Γ′ ⊢ Δ, Δ′

which is equivalent to the “binary” MIX axiom A, B ⊢ A, B or simply A ⊗ B ⊢ A ⊕ B; we also consider adding the “nullary” MIX axiom ⊢ or equivalently ⊤ ⊢ ⊥. As the binary axiom is equivalent to the axiom ⊥ ⊢ ⊤ (see below), this stronger MIX rule can be given equivalently by Γ ⊢ Γ for any Γ, including Γ empty, or by ⊥ ⊣⊢ ⊤.

6.1. Lemma. In the presence of the cut rule and the standard sequent rules for the units, the MIX rule

Γ ⊢ Δ Γ′ ⊢ Δ′
Γ, Γ′ ⊢ Δ, Δ′

is equivalent to the axiom ⊥ ⊢ ⊤. Proof. To obtain the axiom, consider the derivation

\begin{matrix}⊢ ⊤ & ⊥ ⊢ \\ ⊥ ⊢ ⊤ \end{matrix}

For the converse, consider

\begin{matrix}{Γ ⊢ Δ \atop Γ ⊢ Δ, ⊥} & ⊥ ⊢ ⊤ \\ Γ ⊢ Δ, ⊤ \end{matrix} {Γ′ ⊢ Δ′ \atop ⊤, Γ′ ⊢ Δ′}
Γ, Γ′ ⊢ Δ, Δ′

We shall call a linearly distributive category an isoMIX category if there is an isomorphism between the two tensor units. We shall refer to the binary axiom (or its equivalents) alone as (ordinary) MIX. There is an additional coherence condition needed, however. To motivate that condition, consider the following two derivations of A, B ⊢ A, B from ⊥ ⊢ ⊤, which clearly ought to be equivalent.

\begin{matrix}\begin{matrix}{A ⊢ A \atop A ⊢ A, ⊥} & ⊥ ⊢ ⊤ \\ A ⊢ A, ⊤ \end{matrix} & {B ⊢ B \atop ⊤, B ⊢ B} \\ A, B ⊢ A, B \end{matrix}  = \begin{matrix}\begin{matrix}{B ⊢ B \atop B ⊢ ⊥, B} & ⊥ ⊢ ⊤ \\ B ⊢ ⊤, B \end{matrix} & {A ⊢ A \atop A, ⊤ ⊢ A} \\ A, B ⊢ A, B \end{matrix}

Using the evident component box (labelled m) to represent the (iso)morphism m: ⊥ ⟶ ⊤, these two derivations are represented by the circuits in Figure 12: notice that the equivalence of these circuits amounts to introducing a “switch” rewrite that interchanges the ⊥ and ⊤ thinning links. This then gives us the following definition. 6.2. Definition. A MIX category is a linearly distributive category with a morphism m: ⊥ ⟶ ⊤, making the following diagram commutative.

[figure: A ⊗ B; 1 ⊗ (u_{⊕}^{L})^{−1}; A ⊗ (⊥ ⊕ B); 1 ⊗ (m ⊕ 1); A ⊗ (⊤ ⊕ B); (u_{⊕}^{R})^{−1} ⊗ 1; δ_{L}^{L}; (A ⊕ ⊥) ⊗ B; (A ⊗ ⊤) ⊕ B; (1 ⊕ m) ⊗ 1; u_{⊗}^{R} ⊕ 1; (A ⊕ ⊤) ⊗ B; δ_{R}^{R}; A ⊕ (⊤ ⊗ B); 1 ⊕ u_{⊗}^{L}; A ⊕ B]

[figure: ⊕; ⊗; ⊤; ⊥; m; ⊕; ⊗; ⊤; ⊥; m; =]

Figure 12: Two circuits for binary MIX

In the above definition we have insisted the mix diagram holds for all objects. In fact, it suffices to demand that the diagram commutes for either the unit or counit:

6.3. Lemma. A linearly distributive category is MIX if and only if the above diagram holds for any one of the following cases: A = B = ⊤, A = B = ⊥, A = ⊥ and B = ⊤, or A = ⊤ and B = ⊥.

Proof. This can be seen immediately from the circuits as we may introduce thinnings to “float” the MIX-barbell onto the unit (and/or counit) wires, then perform the switch rewrite on the unit/counit wires, and float the barbell back off. We illustrate this in the case where the switch rewrite is moved onto two unit wires:

[figure: ⊥; ⊤; m; ≡; ⊥; ⊤; m; ≡; ≡; ⊥; ⊥; ⊤; ⊤; m; m; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤; ⊤]

Notice that this proof holds for nonsymmetric linearly distributive categories.

6.4. Remark. An immediate corollary of this is that a linearly distributive category is MIX if and only if its nucleus is. This, as has been noted in Remark 5.4, implies that all (⊗–)cartesian linearly distributive categories are MIX categories.

We can now strengthen the MIX structure to give the stronger notion, by adding the nullary case. It turns out that this doesn’t alter the definition in any other way; in particular the coherence condition for the categorical definition remains the same.

6.5. Definition. An isoMIX category is a MIX category whose “mix” morphism m: ⊥ ⟶^{∼} ⊤ is an isomorphism.

Note that there is nothing “degenerate” or inconsistent in this monoidal context about the axiom ⊤ ⊢ ⊥; indeed many models of linear logic have these two units coincide, and so model this situation. Indeed, the structure of isoMIX that we have defined specializes to the case of a linearly distributive category for which there is a single constant I (a “biunit”) which is simultaneously a unit for the tensor and for the cotensor.

In the next section we shall show that isoMIX categories satisfy the expected coherence theorem. As one essentially has a biunit we expect to be able to drop the thinning links from the circuits. The net criterion would have to be adjusted by dropping the “connectedness” part of the Danos-Regnier criterion. However, this still misses the significance of the coherence diagram of Definition 6.2, and so misses an essential part of the story. Moreover, the presentation in this paper is better than a presentation of isoMIX in terms of “biunits” for a number of reasons. It is more general as it uses an isomorphism instead of the identity. More significantly, it captures the right coherence requirements, and it generalizes to the nonsymmetric and general MIX cases.

However, isoMIX is rather close to having a biunit, and so one might suspect that by forcing the units to be essentially the same, one will also force the MIX condition. We now show that this is indeed the case.

6.6. Lemma. A linearly distributive category in which ⊤ is isomorphic to ⊥ is an isoMIX category.

Proof. The idea is this: we consider the map ⊤⊗⊤ ⟶ ⊥⊕⊥ as illustrated by the circuit in Figure 13. By breaking the unit wires above the MIX-barbell and the counit wires below the barbell we can introduce the composite m^{−1}; m; m^{−1} in two different ways, differing only in having (mirror-image) wirings. These both reduce to the same form, resulting in the desired coherence diagram.

Expansions:

[figure: ⊤; ⊥; m; ⟹; ⊤; ⊥; m^{-1}; ⊥; ⊤; m; ⟹; ⊥; ⊤; m^{-1}]

“Switch”:

[figure: ⊥; ⊤; m; ⟹; ⊥; ⊤; m]

Reductions:

[figure: ^{^{m^{-1}} ⟹^{m}}; ^{^{m^{-1}} ⟹^{m}}; ⊤; ⊥; m; ⟹; ⊥; m^{-1}; ⊤; ⟹; ⊥; ⊤; m; ⊤; m^{-1}; ⊥]

Table 6: Rewrites for isoMIX circuits

[figure: ⊥; ⊤; m; ≡; ⊗; ⊕; m^{-1}; m^{-1}; ⊥; ⊤; m; ≡; ⊗; m^{-1}; m^{-1}; ⊕; ⊤; ⊤; ⊤; ⊤; ⊥; ⊥; ⊥; ⊥; ⊗; m^{-1}; ⊤; ⊤; ⊤; ⊥; ⊥; ⊥; ⊕; ≡; ⊥; ⊤; m; m^{-1}; m^{-1}; ⊤; ⊤; ⊤; ⊤; ⊥; ⊥; ⊥; ⊥; ⊕; ⊗; ≡; ⊥; ⊤; m; ⊗; ⊕; m^{-1}; m^{-1}]

Figure 13: Isomorphic units imply MIX

7. Coherence for MIX

We shall concentrate on isoMIX, as the assumption that m is an isomorphism simplifies some details. To extend the coherence theorems of [BCST] we must extend the circuit diagrams for linearly distributive categories to this context. Of course we add the component m as already illustrated in Figure 12, as well as a component m^{−1} for its inverse in the iso case. In addition we need some new reductions and expansions; the rewrite rules in the isoMIX case are shown in Table 6.

[figure: ⊥; ⊤; m]

It is clear from the expansions that any circuit (representing a sequent derivation in the isoMIX calculus) can be replaced by an equivalent circuit all of whose thinning links are attached to “MIX-barbells” (like the one at left). We can regard these barbells as a “glue” that connects disconnected subcircuits. In the traditional approach to nets satisfying the MIX rule [FR94] the usual net criterion (“acyclic and connected for any setting of the switches”) is relaxed so as not to require connectedness; we have

retained connectedness by the presence of the MIX-barbells. Now, one might then expect that the barbells are not really necessary, and the next proposition shows this is indeed the case. We shall suppose that all circuits under consideration for the moment are in the form of a “skeleton”, viz. a circuit without thinning links, made up of m^{−1} components, non-thinning unit links, (⊥ E) and (⊤ I), and the four tensor and cotensor links, together with a number of MIX-barbells “gluing” parts of the underlying graph together (that is just to say that the thinning links of the barbells are attached to wires in the circuit).

7.1. Proposition. In a symmetric isoMIX category, any two nets with the same skeleton (and so differing only in their “gluings”) are equivalent, that is, they represent the same morphism.

Proof. We prove this by an induction on the size of the graph of the skeleton. Circuits consisting of a single component present no problem, and it is simple to see that the induction step consisting of adjoining a binary link to a single subgraph is also straightforward. The only cases that need special consideration involve linking two subgraphs with a binary (tensor or cotensor) link.

[figure: ⊕]

Consider for example a skeleton consisting of two disconnected subgraphs joined by a (⊕ E) (switching) link, and consider two circuits with this skeleton (but some arbitrary arrangement of barbells), and each having just one barbell joining the two given subgraphs. We want to show these are equivalent. First note that in either circuit, the given subgraphs must each be a subcircuit (i.e. must be sequential). To see this, consider a switch setting that cuts the left wire of the (⊕ E) link: for any setting of the switches in the left subgraph that subgraph must be acyclic (obviously) and connected (since any disconnection in this subgraph could not be connected in the whole graph as there is just the one link out of the subgraph, namely through the barbell). Similarly the right subgraph is a subcircuit. But in this case, the Rewiring Theorem [BCST] tells us that we can rewire each thinning link attached to the barbell linking these subcircuits to any other wire in the subcircuit, in particular, we can take the wiring of one circuit and rewire to produce the second circuit, which then must be equivalent to the first.

Next we consider the case where there are two barbells joining the subgraphs: suppose we have two circuits with the same skeleton as above, and with two barbells linking the given subgraphs. We shall refer to these barbells as b_{1} and b_{2}, to the locations in the left subgraph where the thinning links from b_{1}, b_{2} are attached as l_{1}, l_{2}, and to the locations in the right subgraph where the thinning links from b_{1}, b_{2} are attached as r_{1}, r_{2}. Note that in this case it is no longer necessary that the left and right subgraphs need be sequential. However, it is the case that either r_{1}, r_{2} or l_{1}, l_{2} are connected for any setting of the switches, for if both pairs of attachment points were disconnected for all settings, then indeed the complete graph could not be a circuit. Suppose without loss of generality that l_{1}, l_{2} are connected: then by the Rewiring Theorem we can rewire the thinning link attached at l_{1}, say, to the location r_{2}, thus causing this barbell to lie inside the right subgraph, and so reducing the case to the first case with one barbell linking the subgraphs. In this manner, we can always reduce to this one-barbell case where the problem is done.

The case where there are n barbells joining the subgraphs is handled similarly.

Finally, the case when two (or in general n) subgraphs are linked by a (⊗ E) (nonswitching) link is handled by an argument similar to the two-barbell case above. In effect

[figure: ⊗; ⊥ ⊗ ⊥; ⊥; ⊥; ⊥; ⊥; =; ⊗; ⊥ ⊗ ⊥; ⊥; ⊥; ⊥; ⊥]

Figure 14: Two derivations

the non-switching link plays the role of one barbell. Here we cannot suppose that each subgraph is sequential, but we can rewire the barbells so that all are located within one subgraph or the other, at which point the subgraphs must be sequential, so reducing the problem to the smaller case.

From this we can see how coherence works in the isoMIX context. Given two circuits, we can reduce them to an expanded normal form in which all thinning links come from MIX-barbells. We can eliminate all such barbells from the nets, and then the circuits are equivalent if and only if the expanded normal forms are identical. In effect then, we could present nets in this case without thinning links, and use the “acyclic for any switch setting” criterion for sequentiality (in the commutative case).

7.2. Remark. The preceding argument is actually valid not only for commutative but also for noncommutative tensors. We assumed the tensor and cotensor are symmetric so as to be able to use the (Empire) Rewiring Theorem which simplifies the proof. However, the more general Rewiring Theorem from [BCST] may be used to obtain the same effect in the noncommutative case.

The argument can also be extended to cover the (ordinary) MIX case. In this case a skeleton can contain thinning links, but the proof still goes through to show that all ways of adding MIX-barbells are equivalent for a given skeleton. However, there is the added complication that two skeletons can be equivalent through rewirings that involve the added MIX-barbells.

For example, two equivalent derivations of ⊥ ⊗ ⊥ ⟶ ⊥ are shown in Figure 14. To determine this equivalence however one must add in the missing barbells, and then use the Rewiring Theorem, as shown in Figure 15.

References

[BBPH] Benton B.N., G. Bierman, V. de Paiva, M. Hyland “Term assignment for

[figure: ⊗; ⊥ ⊗ ⊥; ⊥; ⊥; ⊥; ⊥; ⟺; ⊗; ⊥ ⊗ ⊥; ⊥; ⊥; ⊥; ⊥; ⊗; ⊥ ⊗ ⊥; ⊥; ⊥; ⊥; ⊥; ⟺; ⊥; ⊤; m; ⊗; ⊥ ⊗ ⊥; ⊥; ⊥; ⊥; ⊥; ⟺; ⊥; ⊤; m]

Figure 15: Equivalence of the two derivations

intuitionistic linear logic”, in M. Bezem and J.F. Groote, eds, Proceedings of the International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 664 1992, 75–90.

[B92] Blute, R.F. “Linear Logic, Coherence and Dinaturality”, Theoretical Computer Science 115 (1992) 3–42.

[BCS92] Blute, R.F., J.R.B. Cockett, and R.A.G. Seely “ ! and ? : Storage as tensorial strength”, Mathematical Structures in Computer Science 6 (1996) 313–351.

[BCST] Blute R.F., J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble “Natural deduction and coherence for weakly distributive categories”, Journal of Pure and Applied Algebra 113 (1996) 229–296. (Preprint, McGill University, 1992, revised 1994).

[CS91] Cockett, J.R.B. and R.A.G. Seely “Weakly distributive categories”, in M.P. Fourman, P.T. Johnstone, A.M. Pitts, eds., Applications of Categories to Computer Science, London Mathematical Society Lecture Note Series 177 (1992) 45–65.

[CS91j] Cockett, J.R.B. and R.A.G. Seely “Weakly distributive categories”, Journal of Pure and Applied Algebra 114 (1997) 133–173. (Updated version available on

<http://www.math.mcgill.ca/~rags>.)

[CS96] Cockett, J.R.B. and R.A.G. Seely “Linearly distributive functors”, preprint, McGill University, 1996.

[D90] Danos, V. “La logique linéaire appliquée à l’étude de divers processus de normalisation et principalement du λ-calcul”, Doctoral dissertation, Université de Paris, 1990.

[DR89] Danos, V. and L. Regnier “The structure of multiplicatives”, Archive for Mathematical Logic 28 (1989) 181–203.

[FR94] Fleury, A. and C. Retoré “The mix rule”, Mathematical Structures in Computer Science 4 (1994) 273–285.

[Gi87] Girard, J.-Y. “Linear logic”, Theoretical Computer Science 50 (1987) 1–102.

[Gr83] Grishin, V.N. “On a generalization of the Ajdukiewicz–Lambek system”, in Studies in Nonclassical Logics and Formal Systems, Nauka, Moscow, (1983) 315– 343.

[HR89] Higgs, D.A. and K.A. Rowe “Nuclearity in the category of complete semilattices”, Journal of Pure and Applied Algebra 57 (1989) 67–78.

[HP91] Hyland, M. and V. de Paiva “Lineales”, talk given at the Montreal Category Theory Meeting, June 1991.

[HP93] Hyland, M. and V. de Paiva “Full intuitionistic linear logic (Extended Abstract)”, Annals of Pure and Applied Logic 64, 3 (1993) 273–291.

[J90] Jay, C.B. “The structure of free closed categories”, Journal of Pure and Applied Algebra 66 (1990) 271–285.

[Laf95] Lafont, Y. “From proof nets to interaction nets”, in J.-Y. Girard, Y. Lafont, and L. Regnier, eds., Advances in Linear Logic, London Mathematical Society Lecture Note Series 222 (1995) 225–247.

[L69] Lambek, J. “Deductive systems and categories II”, Lecture Notes in Mathematics 87 (Springer-Verlag, Berlin, Heidelberg, New York, 1969).

[L93] Lambek, J. “From categorial grammar to bilinear logic”, in K. Došen and P. Schroeder-Heister, eds., Substructural logics, Studies in Logic and Computation 2, Oxford Science Publications, 1993

[LW92] Lincoln, P. and I. Winkler “Constant-only multiplicative linear logic is NPcomplete”, Theoretical Computer Science 135 (1994) 155–169.

[P65] Prawitz, D. Natural Deduction, Almqvist and Wiksell, Uppsala (1965)

[R88] Rowe, K.A. “Nuclearity”, Canad. Math. Bull. 31 (1988) 227–235.

[Sc91] Schellinx, H. “Some syntactical observations on linear logic”, Journal of Logic and Computation 1 (1991) 537–559.

[Se89] Seely, R.A.G. “Linear logic, ∗-autonomous categories and cofree coalgebras”, in J. Gray and A. Scedrov (eds.), Categories in Computer Science and Logic Contemporary Mathematics 92 (Am. Math. Soc. 1989).

[T94] Trimble, T.H. “Linear logic, bimodules, and full coherence for autonomous categories”, Doctoral dissertation, Rutgers University, 1994.

[Tr91] Troelstra, A. Lectures on Linear Logic, CSLI Lecture Notes 29 (CSLI 1992).

Appendices

A. Circuit expressions

In [BCST] we pointed out that proof circuits were not mere “pretty pictures”, but rather that there was a rigorous term calculus underpinning them. To accommodate the proof systems discussed in this paper we shall have to extend the term calculus for proof circuits (i.e. circuit expressions) introduced in [BCST]. This appendix is not intended to be selfcontained and relies on the notation introduced in [BCST]. The extension involves adding new components to the set listed in [BCST] corresponding to the new links for the new connectives. So for example, for ({− \atop ∘} E) there is no need for any new notation; we just treat this as a new given component, and so have the expression

A, A {− \atop ∘} B : ⟨a, z|[a, z] {− \atop ∘} E[b]|b⟩ : B

There are similar expressions for (∘− E), (⧁ I), (⧀ I).

The trick is to adapt this calculus to handle the scope boxes we are using. For this we shall introduce new binding operators: for example, for ({− \atop ∘} I) we need a binding operator which abstracts variables a:A, b:B from an expression for C, and introduces a new output variable z : A {− \atop ∘} B. So, given a circuit expression A, Γ : ⟨a, w|[a, w]C[b, v]|b, v⟩ : B, Δ, we have a new term introduced by ({− \atop ∘} I) given by

Γ : ⟨w|\underline{(a|[a, w]C[b, v]|b>}[z]|z, v⟩ : A {− \atop ∘} B, Δ

Similarly for the other “hom” terms—using notation based on the sequent rules of Table 2 this gives these circuit expressions for (∘− I), (⧁ E), (⧀ E).

Γ : ⟨w|\overline{(b|[w, b]C[v, a]|a>}[z]|v, z⟩ : Δ, A ∘− B
A ⧁ B, Δ : ⟨z, w|[z]\overline{<b|[b, w]C[a, v]|a)}|v⟩ : Γ
Δ, A ⧀ B : ⟨w, z|[z]\underline{<a|[w, a]C[v, b]|b)}|v⟩ : Γ

The reductions and expansions corresponding to these rewrites (we leave the typing to the reader) are:

\begin{aligned}\underline{(a|C|b>}[z]; [a, z] {− \atop ∘} E[b] & ⇒ & C \\ \overline{(b|C|a>}[z]; [z, b] ∘− E[a] & ⇒ & C \\ [b] ⧁ I[a, z]; [z]\overline{<b|C|a)} & ⇒ & C \\ [a] ⧀ I[z, b]; [z]\underline{<a|C|b)} & ⇒ & C \end{aligned}  \begin{aligned}[z] & ⇒ & \underline{(a|[a, z] {− \atop ∘} E[b]|b>}[z] \\ [z] & ⇒ & \overline{(b|[z, b] ∘− E[a]|a>}[z] \\ [z] & ⇒ & [z]\overline{<b|[b] ⧁ I[a, z]|a)} \\ [z] & ⇒ & [z]\underline{<a|[a] ⧀ I[z, b]|b)} \end{aligned}

In addition, there are equations corresponding to the box (or scope) equivalences of Table 4:

\begin{aligned}C′; \underline{(a|C|b>}[z] & = & \underline{(a|C′; C|b>}[z] \\ \underline{(a|C|b>}[z]; C′ & = & \underline{(a|C; C′|b>}[z] \\ C′; \overline{(b|C|a>}[z] & = & \overline{(b|C′; C|a>}[z] \\ \overline{(b|C|a>}[z]; C′ & = & \overline{(b|C; C′|a>}[z] \end{aligned}  \begin{aligned}C′; [z]\overline{<b|C|a)} & = & [z]\overline{<b|C′; C|a)} \\ [z]\overline{<b|C|a)}; C′ & = & [z]\overline{<b|C; C′|a)} \\ C′; [z]\underline{<a|C|b)} & = & [z]\underline{<a|C′; C|b)} \\ [z]\underline{<a|C|b)}; C′ & = & [z]\underline{<a|C; C′|b)} \end{aligned}

where C, C′ are circuit expressions, a, b ∉ free variables of C′. These equations will only be of interest, of course, when both sides are sequential, in the sense of the next appendix.

B. Sequentialization

One rather crucial aspect of circuits is the matter of determining whether a circuit is a representation of a valid sequent derivation or not. The circuits which represent sequent derivations are called sequential; the process of verifying such validity is called sequentialization.

In [BCST] sequentialization for the tensor–par fragment of noncommutative linear logic was studied in some detail, using essentially the same approach as that given independently by Lafont [Laf95]. It is now straightforward to adapt that approach for bilinear logic. Note that the original proof of Girard’s [Gi87] will not work in the present context, where we allow non-logical axioms (the components C) in the logic [BCST]. However, since our proof of sequentialization for linearly distributive categories allowed non-logical components, we get more-or-less immediately sequentialization for bilinear logic, and for GILL and FILL therefore as well.

Again, this appendix is not intended to be self-contained, but rather just gives the necessary pointers to carry out the appropriate modifications to [BCST]. In Table 7 we show some of the sequentialization steps for these natural deduction links for bilinear logic and GILL; the reader may fill in the rest by duality. For FILL there is an important change to these rules, as pointed out in Remark 1.1. That is, the restriction that Δ be empty in the left hand rewrite in Table 7 means that we ought to redraw this rewrite without Δ.

We shall leave it to the reader to verify that the proof of sequentiality from [BCST] applies to the present context. As we have merely added some new components and some new sequentialization steps for these components, we just have to check that the confluence of the new system still holds. The only technical problems in the proof in [BCST] involved the cut rule; with the natural deduction presentation of bilinear logic the cut rule is unchanged, and the [BCST] proof applies here.

In [BCST] we made some comments about this sequentialization process and the traditional net criterion in the noncommutative case. These apply equally to FILL and to bilinear logic. In particular, it is possible for a non-sequential (in the noncommutative sense) planar circuit to satisfy the traditional net criterion. The example in Figure 16

[figure: {− \atop ∘}; A, Γ ⊢ B, Δ; Δ; ⟹; Γ ⊢ A {− \atop ∘} B, Δ; Δ; A {− \atop ∘} B; A {− \atop ∘} B; Γ; Γ; A; B; {− \atop ∘}; A {− \atop ∘} B; A; B; ⟹; A, A {− \atop ∘} B ⊢ B; A {− \atop ∘} B; A; B]

Table 7: Sequentialization

[figure: ⊕; ⊕; ⊗; ⊕; ⊤; ⊤; ⊗; ⊗; ⊤; ⊥; A ⊕ (⊥ ⊕ B); (A ⊗ ⊤) ⊕ B; ⊕; ⊕; ⊗; ⊕; ⊤; ⊥; (A ⊗ ⊤) ⊕ B; A ⊕ (⊥ ⊕ B); ⟹]

Figure 16: A non-sequential net, and its sequential normal form

illustrates this in a simple case, where we only use the linearly distributive structure of ⊗, ⊕ and their units. With this example, we can actually see the problem: if we reduce this circuit, as shown in Figure 16, the resulting net is sequential. An attempt to sequentialize the original example quickly shows that the problem occurs because of the cut using the formula ⊤ ⊗ ⊤; this cut is not present in the reduced circuit. Similar problems can occur with non-logical axioms (extra components, that is) and with nets with multiple input or output wires.

List of Tables

1 Links for proof circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 2 Sequent rules corresponding to circuit links . . . . . . . . . . . . . . . . . . 92 3 Reductions and expansions for proof circuits . . . . . . . . . . . . . . . . . 95 4 Box scope equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 5 Some unit rewirings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 6 Rewrites for isoMIX circuits . . . . . . . . . . . . . . . . . . . . . . . . . . 122 7 Sequentialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130

List of Figures

1 Orienting scope?—scope expansion . . . . . . . . . . . . . . . . . . . . . . 94 2 Orienting scope?—scope reduction . . . . . . . . . . . . . . . . . . . . . . 94 3 Some examples of proof circuits . . . . . . . . . . . . . . . . . . . . . . . . 97 4 An example of circuit rewrites . . . . . . . . . . . . . . . . . . . . . . . . . 98 5 A valid circuit for the triple dual map . . . . . . . . . . . . . . . . . . . . . 109 6 A^{⊥} rewrites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 7 ⧁ derived links . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 8 ⧁ derived rewrites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 9 Isomorphisms between two negations . . . . . . . . . . . . . . . . . . . . . 115 10 Circuits for nuclear objects . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 11 Circuits for nuclear objects . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 12 Two circuits for binary MIX . . . . . . . . . . . . . . . . . . . . . . . . . . 120 13 Isomorphic units imply MIX . . . . . . . . . . . . . . . . . . . . . . . . . . 123 14 Two derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 15 Equivalence of the two derivations . . . . . . . . . . . . . . . . . . . . . . . 126 16 A non-sequential net, and its sequential normal form . . . . . . . . . . . . 130

Department of Computer Science, University of Calgary, 2500 University Drive, Calgary, AL, T2N 1N4, Canada. and Department of Mathematics, McGill University, 805 Sherbrooke St., Montréal, PQ, H3A 2K6, Canada.

Email: robin@cpsc.ucalgary.ca   rags@math.mcgill.ca

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1997/n5/n5.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi and Postscript format. Details will be e-mailed to new subscribers and are available by WWW/ftp. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and LaTEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at URL http://www.tac.mta.ca/tac/ or by anonymous ftp from ftp.tac.mta.ca in the directory pub/tac/info. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@triples.math.mcgill.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, University of Genoa: carboni@vmimat.mat.unimi.it P. T. Johnstone, University of Cambridge: ptj@pmms.cam.ac.uk G. Max Kelly, University of Sydney: kelly m@maths.su.oz.au Anders Kock, University of Aarhus: kock@mi.aau.dk F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.ruu.nl Susan Niefield, Union College: niefiels@gar.union.edu Robert Paré, Dalhousie University: pare@cs.dal.ca Andrew Pitts, University of Cambridge: ap@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@charlie.math.unc.edu Ross Street, Macquarie University: street@macadam.mpce.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Sydney: walters b@maths.su.oz.au R. J. Wood, Dalhousie University: rjwood@cs.da.ca