Full completeness of the multiplicative linear logic of Chu spaces

Harish Devarajan

Stanford University

Dominic Hughes

Stanford University

Gordon Plotkin

University of Edinburgh

Vaughan Pratt

Stanford University

Abstract

We prove full completeness of multiplicative linear logic (MLL) without MIX under the Chu interpretation. In particular we show that the cut-free proofs of MLL theorems are in a natural bijection with the binary logical transformations of the corresponding operations on the category of Chu spaces on a two-letter alphabet.

This is the online version of the paper of the same title appearing in the LICS’99 proceedings.

1 Introduction

Ordinary completeness of an axiom system reconciles the syntax and semantics of truth by promising a finite syntactic justification for every semantically valid theorem. Full completeness analogously reconciles the syntax and semantics of proof by promising a finite syntactic derivation of every semantically sound constructive proof. The term “full” comes from category theory, which provides the appropriate setting for the interpretation of syntactic proofs by semantic in terms of a full functor from a category of the former (as its morphisms) to a category of the latter. For a sufficiently abstract notion of syntactic proof one can expect in addition that the representation functor be faithful.

The conventional semantic justification for theorems, evolved largely during this century, is truth invariance for all value assignments of the parameters of the theorem, possibly subject to given axioms. More recently analogous semantic notions of abstract constructive proof have begun to appear, in particular natural and dinatural transformations [LS86, BS96] and related notions such as logical transformations [Plo80], game strategies [AJ94, HO93], and uniformity conditions [Loa94]. The naturality condition expresses transformational invariance for all transformations of the parameters of the proof, again possibly subject to given axioms.

The interpretation of natural transformations as constructive proofs is suggested by the the Curry-Howard interpretation of types as propositions. This interpretation is motivated at least in part by the striking phenomenon that every type having at least one such semantic proof corresponds to a theorem when types are read as propositions. For example when A and B are type variables ranging over kindred objects such as sets, or vector spaces, the projection from A × B to A, a natural transformation in the respective category of those objects, can be understood as witnessing the validity of the proposition A ∧ B ⊃ A. The correspondences between conjunction A ∧ B and product A × B, and implication A ⊃ B and the function space A → B, are prominent features of the Curry-Howard isomorphism.

Viewing an object A as consisting of all admissible evidence for the corresponding proposition A brings out the constructive quality of transformations-as-proofs. Our example of the projection from A×B to A can then be understood as a method for constructing evidence a for A from evidence (a, b) for A ∧ B by discarding b.

One application for extending completeness to proofs is to symmetrize better the complementarity of truth and proof by equipping each with a reconciled syntax and semantics. Another is to substitute a calculus tailored to the manipulation of algebraic structures for the usual general-purpose first-order calculus, with the goal of improving our understanding of human algebraic reasoning. Yet another is to enrich automated theorem proving and program verification systems with new techniques complementary to the existing ones.

In this paper we prove full completeness of Multiplicative Linear Logic (MLL) [Gir87] without units in the category Chu of Chu spaces over 2 [Bar79]. In more detail, we exhibit a full functor from the ∗-autonomous category of cut-free proofs of MLL to the ∗-autonomous category of binary logical transformations between MLL formulae interpreted as operations Ob(Chu)^{n} → Ob(Chu), where Ob(Chu) denotes the objects of Chu, and n is the number of variables in a formula.

Elsewhere [Pra97] we demonstrated full completeness for dinatural transformations in Chu of binary MLL formulas, those in which each variable occurs only once with each sign. We also demonstrated the impossibility of increasing the number of occurrences of one variable by exhibiting a spurious dinatural transformation of (A−∘A)−∘(A−∘A), one that corresponded to no linear logic proof.

The contribution of this paper is that strengthening dinaturality to binary logicality eliminates all spurious transformations. The same strengthening has previously proved successful in eliminating spurious transformations in the category of Sets [Plo80, PR98].

This correspondence between linear logic and Chu spaces enhances both subjects. On the one hand the correspondence furnishes Chu spaces with the attractive and well-studied structure of linear logic. On the other, linear logic benefits from having a model that is of interest both in its own right [Bar79, Pav96, Pra98] and for foundations of mathematics and semantics of concurrency. Chu spaces provide a linear counterpart to relational structures as universal mathematical objects, inasmuch as a great many concrete categories arising in mathematical practice emded fully and concretely in Chu(Set, K) for some K [Pra95b]. Moreover the rows and columns of Chu spaces model events and states of concurrent processes with the same even-handedness that Petri nets grant to their places and transitions, but with a richer process-algebraic structure [Pra95a, VGP95]. Given these considerations, the exact match of the logicality semantics of Chu spaces with the proof structure of multiplicative linear logic simultaneously confers a degree of logical tractability on Chu spaces while broadening the applicability of linear logic.

In outline, our proof begins with semisimple (par of tensors) MLL formulas A, and associates a MIX proof net π with every Chu logical transformation η of A. We pull η back along the Lafont-Streicher embedding (LS) of coherence spaces [LS91] to yield a dinatural η̂, then appeal to full completeness for MLL with MIX [Tan97] to obtain π (Section 3.1). Next we show that π determines η not only in the LS image but also beyond, by using logical relations to tie down its behaviour at an arbitrary Chu space via the LS image of its coherence space “simulation” (Section 3.3). To refute MIX we show that, in Chu, information flows between the connected components of switchings of MIX proof nets and deduce that there can be only one component (Section 3.4). We conclude by extending to formulas of higher type by induction on a measure of the number of applications of linear distributivity required to reach semisimple formulas (Section 4).

2 Definitions

2.1 Chu Spaces

A Chu space A = (A, r, X) over a set K is a set A of points, a set X of states, and a function r : A × X → K, called the matrix of A. For each point a the a^{th} row of A is r(a, −) : X → K, and for each state x the x^{th} column of A is r(−, x) : A → K.

A Chu space A is biextensional if it has no repeated columns and no repeated rows. The biextensional collapse of a Chu space is the result of identifying repeated rows and columns.

A Chu transform (f, g) : (A, r, X) → (B, s, Y) is a pair of functions f : A → B and g : Y → X satisfying the adjointness condition s(f(a), y) = r(a, g(y)) for all a in A and y in Y.

The category Chu_{K} has as objects Chu spaces over K and as morphisms Chu transforms composing via (f′, g′)(f, g) = (f′f, gg′).

It will sometimes be convenient to write A and X as A^{+} and A^{−}, and Chu transforms ϕ as (ϕ^{+} , ϕ^{−}). We also adopt the notation a · x for r(a, x) when r can be deduced easily from context.

The dual or perp A^{⊥} of A = (A, r, X) is (X, r˘ , A) where r˘ (x, a) = r(a, x). On morphisms (f, g) : A → B, define (f, g)^{⊥} = (g, f) : B^{⊥} → A^{⊥}. Linear negation is involutive: A^{⊥⊥} = A and (f, v)^{⊥⊥} = (f, v).

The tensor product A ⊗ B of A = (A, r, X) and B = (B, s, Y) is (A × B, t, F) where F ⊂ Y^{A} × X^{B} is the set of all pairs (h, k) of functions h : A → Y, k : B → X for which s(b, h(a)) = r(a, k(b)) for all a ∈ A and b ∈ B, and t : (A × B) × F → K is given by t((a, b), (h, k)) = s(b, h(a)) (= r(a, k(b))).

Given (f, g) : A → B and (f′, g′) : A′ → B′ define (f, g)⊗(f′, g′) : A⊗A′ → B ⊗B′ on points by (a, a′) ↦ (f(a), f′(a′)), and on states by (h : B → Y′, k : B′ → Y) ↦ (g′h′f : A → X′, gk′f′ : A′ → X).

Tensor is commutative and associative up to coherent isomorphism. A−∘B abbreviates (A ⊗ B^{⊥})^{⊥} and A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B abbreviates (A^{⊥} ⊗ B^{⊥})^{⊥}.

The tensor unit 1 is ({⋆}, λak.k, K), a single row consisting of K. Chu transforms 1 → A correspond to points a ∈ A^{+} of A, since the reverse map on states is fully determined. In this paper we treat the axiomatization of MLL without units.

These operations make Chu_{K} a ∗-autonomous category [Bar79]. Our full completeness result is for K = 2 = {0, 1}, and we henceforth abbreviate Chu_{2} to Chu.

2.2 Logical Transformations

An MLL formula is an expression built from propositional variables with symbols for tensor and perp. Such a formula of up to n variables defines an n-ary MLL operation Ob(Chu)^{n} → Ob(Chu), where Ob(Chu) is the collection of objects of Chu, by interpreting syntactic tensor ⊗ and perp (−)^{⊥} by the object part of their namesakes in Chu. More formally, given an MLL formula F on variables P_{1}, …, P_{n} we define the corresponding n-ary MLL operation F : Ob(Chu)^{n} → Ob(Chu) at A A A for (A_{1}, …, A_{n}) by induction as follows.

\begin{aligned}P_{i}(A A A) & = & A_{i} & (F ⊗G)(A A A) & = & F (A A A)⊗G(A A A) \\ P_{i}^{⊥}(A A A) & = & A_{i}^{⊥} & (F^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G)(A A A) & = & F (A A A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G(A A A) \end{aligned}

A transformation τ : F → G between n-ary MLL operations is a family of morphisms τ_{A A A} : F (A A A) → G(A A A) indexed by n-tuples A A A of Chu spaces. We take the constant operation 1 : (A_{1}, …, A_{n}) ↦ 1 to be an n-ary MLL operation, where 1 is the tensor unit in Chu, allowing us to work with elements η_{A A A} : 1 → F (A A A).

In their role as interpretations of MLL proofs, there are far too many transformations for a full completeness result, most transformations being too specific to represent general-purpose constructions. The usual criterion for a canonical choice of transformations is naturality, but this is unavailable for mixed-variance MLL terms such as A−∘A because there is no obvious extension of such operations from objects to morphisms.

Dinatural transformations circumvent the mixedvariance problem by defining a suitable notion of naturality for transformations between “composites” (loosely understood as including A−∘A) of the functors (−)^{⊥}, (−) ⊗ (−) and (−)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (−), of which our MLL operations are the object part. Dinaturality suffices to prove full completeness of MLL, without units but with the MIX rule A ⊗ B ⊢ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, for coherence spaces [Tan97]. For Chu spaces however dinaturality is not strong enough in that it admits certain spurious transformations corresponding to no MLL proof [Pra97]. A further drawback of dinatural transformations is that they do not always compose.

In this paper we eliminate all spurious transformations with the help of a stronger condition, binary logicality, which we shall abbreviate to logicality. We extend MLL operations to act not on morphisms but on binary relations R : A −^{×} B, yielding binary relations F (R) : F (A) −^{×} F (B). Unlike functions, binary relations are closed under converse, which neatly sidesteps the main difficulty with mixed-variance.

Definition 1. A Chu relation R = (R^{+} , R^{−}) : A −^{×} B between Chu spaces A = (A, r, X) and B = (B, s, Y) is a pair of ordinary binary relations R^{+} ⊆ A × B and R^{−} ⊆ X × Y meeting the following adjointness condition: for all a, b, x, y such that aR^{+} b and xR^{−} y, we have a · x = b · y.

In the special case when R^{+} is a function A → B and R^{−} a function Y → X, a Chu relation is exactly a Chu transform. Hence Chu relations generalize Chu transforms.

We need the following notion both to define the action of MLL operations on Chu relations, and to define logical relations.

Definition 2. Let (A, B, R) be a two-sorted relational structure with one binary relation R ⊂ A × B. Take a second structure (A′, B′, R′) of the same similarity type. We call a pair of functions f : A → A′, g : B → B′ a two-sorted homomorphism when for all aRb we have f(a)R′g(b).

We now define how MLL operations act on Chu relations.

Perp. If R = (R^{+} , R^{−}) : A −^{×} B, so that R^{+} ⊆ A^{+} × B^{+} and R^{−} ⊆ A^{−} × B^{−} satisfy adjointness, then R^{⊥} = (R^{−} , R^{+} ) : A^{⊥} −^{×} B^{⊥}, also satisfying adjointness. In the special case where R is a Chu transform from A to B, R^{⊥} will be a Chu transform from B^{⊥} to A^{⊥}.

Tensor. Given R : A −^{×} B and R′ : A′ −^{×} B′, we define R ⊗ R′ : A ⊗ A′ −^{×} B ⊗ B′ by (i) (a, a′)(R ⊗ R′)^{+} (b, b′) iff aR^{+} b and a′R′^{+} b′, and (ii) (f_{1}, f_{2})(R ⊗ R′)^{−} (g_{1}, g_{2}) iff (f_{1}, g_{1}) is a two-sorted homomorphism from R^{+} to R′^{−} and (f_{2}, g_{2}) is a two-sorted homomorphism from R′^{+} to R^{−} . This brings us to the main concept for our result, that of

logical transformation.

Let η : F → G be a transformation between n-ary MLL operations. Then each component η_{A A A} : FA A A → GA A A is a Chu transform, consisting of an adjoint pair of functions η_{A A A}^{+} : F A^{+} → GA^{+} and η_{A A A}^{−} : GA A A^{−} → FA A A^{−} (read FA A A^{+} as (F (A A A))^{+} ). The usual naturality commuting square becomes a pair of squares, one for points, and one for states, which we call the positive and negative logicality squares, the top and bottom faces of the following cube.

[figure: FA A A^{+}; GA A A^{+}; FA A A^{−}; GA A A^{−}; η_{A A A}^{+}; r_{FA A A}; r_{GA A A}; η_{A A A}^{−}; FR R R^{+}; GR R R^{+}; FR R R^{−}; GR R R^{−}; FB B B^{+}; GB B B^{+}; FB B B^{−}; GB B B^{−}; η_{B B B}^{+}; r_{FB B B}; r_{GB B B}; η_{B B B}^{−}]

In the cube A A A = (A_{1}, …, A_{n}) ∈ Chu^{n}, B B B = (B_{1}, …, B_{n}) ∈ Chu^{n}, R R R = R_{1}, …, R_{n} is a tuple of Chu relations R_{i} : A_{i} −^{×} B_{i}, FR R R^{+} abbreviates (F (R R R))^{+} , and r_{C} denotes the matrix of C. The positive logicality square, namely the top face of the cube, consists of a two-sorted homomorphism between F (R R R)^{+} ⊆ F (A A A)^{+} × F (B B B)^{+} and G(R R R)^{+} ⊆ G(A A A)^{+} × G(B B B)^{+} , namely a pair of functions η_{A A A}^{+} : F (A A A)^{+} → G(A A A)^{+} and η_{B B B}^{+} : F (B B B)^{+} → G(B B B)^{+} such that a F (R R R) b implies η_{A A A}(a) G(R R R) η_{B B B}(b) for all a ∈ F (A A A)^{+} and b ∈ F (B B B)^{+} .

Definition 3. A transformation η between n-ary MLL operations F and G is logical when all logicality squares in η are two-sorted homomorphisms.

A less elementary but faster equivalent definition of both the action of MLL operations on relations and of logicality takes for these cubes the morphisms of Chu(Log,2). This is the result of applying the Chu construction [Bar79, App.] to Log, the category of binary relations as objects and two-sorted homomorphisms between them, with dualizer the identity relation 1_{2}. This approach requires a familiarity with the general categorical Chu construction that we have not presumed here.

2.3 Multiplicative Linear Logic

In this section we define a Hilbert-style axiomatization of multiplicative linear logic (MLL) convenient for our main result. The language of MLL consists of finite formulas built up from literals (propositional variables P or P^{⊥}) using connectives tensor A ⊗ B and par A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B. We expand the abbreviations (A ⊗ B)^{⊥} to A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B^{⊥}, (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} to A^{⊥} ⊗ B^{⊥}, A−∘B to A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, A^{⊥⊥} to A, and A ⊗ B ⊗ C to (A ⊗ B) ⊗ C.

We axiomatize MLL with one axiom schema together with rules for associativity, commutativity, and linear or weak distributivity as follows.

System S:

T_{n} (L_{1}^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L_{1}) ⊗ … ⊗ (L_{n}^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L_{n}), n ≥ 1
A (A ⊗ B) ⊗ C ⊢ A ⊗ (B ⊗ C)
\overline{A}  (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C ⊢ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)
C  A ⊗ B ⊢ B ⊗ A
\overline{C}  A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A
D  (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ⊗ C ⊢ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ C)
E  A ⊗ B ⊢ A′ ⊗ B′
\overline{E}  A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ A′^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B′

Rules E and \overline{E} assume A ⊢ A′ and B ⊢ B′, i.e. the other rules may be applied not only to formulas but to their subformulas.

The obvious interpretation of this system is propositional: the axiom is an n-fold conjunction of trivial implications L−∘L between literals P or P^{⊥}, and the rules derive additional theorems in arbitrary MLL formulas A, B, C. (To eliminate explicit ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} from Rule D, substitute A^{⊥} for A and abbreviate the result to (A−∘B) ⊗ C ⊢ A−∘(B ⊗ C).)

We pass from the logical to the transformational interpretation via the Curry-Howard isomorphism, which reinterprets propositions as MLL operations and proofs as procedures for suitably transforming evidence for those propositions. For example the operation P −∘P, as the case n = 1 of the axiom schema T, has a unique proof, namely the identity transformation 1_{P} : P → P as P ranges over all Chu spaces. We then understand the above system as a calculus for deriving new transformations from old.

The transformation produced by each derivation in this system is defined as follows by induction on the length of derivations. We only specify the object part of the MLL operations since we do not use the morphism part.

Axiom schema Tdenotes for each n the n-tuple of identity transformations, with the i-th being 1_{L_{i}} : L_{i} → L_{i} where L_{i} is the i projection from Chu^{n} to Chu when L_{i} = P_{i}, composed with perp when L_{i} = P_{i}^{⊥}.

Rule A maps each point ((a, b), c) of F (A_{1}, …, A_{n}) to point (a, (b, c)) of G(A_{1}, …, A_{n}) for each point of F (A_{1}, …, A_{n}), where F is the n-ary MLL operation formed as per the left-hand side from n-ary MLL operations A, B, C, and G is similarly formed from the righthand side. The adjoint of this map sends each pair (f, g), where f : A → (B ⊗ C)^{⊥}, g : B ⊗ C → A^{⊥}, to f′ : A × B → C^{⊥}, g′ : C → (A ⊗ B)^{⊥} each obtained by transposition (Currying) from f and g respectively. Rule \overline{A}is the evident dual of this.

Rule C maps each point (a, b) of F (A_{1}, …, A_{n}) to point (b, a) of G(A_{1}, …, A_{n}), again for F, G respectively the left and right hand sides of the rule. And again Rule \overline{C} is merely the dual of Rule C.

The meat of the system resides in Rule D, linear distributivity. This is a pair consisting of a forward map sending the pair ((f, g), c) to the Chu transform (λx.(f(x), c), λ(h, k).g(k(c))) (uniquely determined by the types), and a backward map from A^{⊥} ⊗ (B^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C^{⊥}) to (A^{⊥} ⊗ B^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C^{⊥} sending the pair (x, (h, k)) to the Chu transform (λ(f, g).h(g(x), λc.(x, k(c)), where f : X → B, g : Y → A, h : B → Z, k : C → Y throughout. Note the self-duality of Rule D, which therefore needs no dual unlike A, C, and E.

Rule E takes as input transformations σ : A → A′ and τ : B → B′, and combines them by tensoring their outputs together as σ ⊗ τ, defined pointwise on objects of Chu^{n}. Likewise Rule \overline{E} par’s them together.

Theorem 4 (Soundness). If τ is derivable in System S then τ is logical.

2.4 Linkings, Proof nets, and Danos-Regnier

Definition 5. A linking of a formula having n complementary pairs of literal occurrences is a function Λ : 2n → 2n, where 2n = {1, 2, …, 2n}, with the properties that, for 1 ≤ i ≤ 2n, (a) Λ(Λ(i)) = i, and (b) the literals occurring at positions i and Λ(i), counting literal occurrences from the left starting from 1, are the same variable with opposite polarities. We say that the literals at i and Λ(i) are connected by a link, which we view as an edge of an undirected graph.

A proof structure is a pair (A, Λ) where Λ is a linking of formula A.

A proof net is a proof structure (A, Λ) arising as a derivation in System S as follows. At the start of the derivation the instance of axiom Tis made a proof structure with the linking Λ defined for 1 ≤ i ≤ n as Λ(2i − 1) = 2i, Λ(2i) = 2i − 1, thereby pairing up the two literals in P_{i}^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} P_{i}. All subsequent steps A ⊢ B of the proof assign the linking of A to B, with the exception of rules C and \overline{C}, which transform (A, Λ) to (A′, Λ′) by modifying Λ to reflect the new positions of the literal occurrences in the two interchanged formulas while leaving the rest of Λ unchanged.

When all n pairs of P_{i}’s of a theorem are distinct, it is easy to see that the theorem has a unique proof net. However repetitions of P_{i}’s, as in (P −∘P) ⊗ (P −∘P), raise the possibility that a conseqence such as (P ⊗ P)−∘(P ⊗ P) may have more than one proof net. In this example, two matchings are possible, which may be understood as corresponding to the two theorems (P ⊗ Q)−∘(P ⊗ Q) and (P ⊗ Q)−∘(Q ⊗ P), in each of which Q is then renamed to P.

Danos and Regnier [DR89] give the following characterization of proof nets. Form the parse-tree of the theorem, regarded as an undirected graph, with ⊗’s and ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ’s labeling the root and internal vertices, and literals labeling the leaves. Add one edge for every link, between the literals linked by the proof structure. Now define a switching of a proof structure to be a deletion of one of the two edges immediately under each^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} . The main theorem of the Danos-Regnier paper is that for MLL with the MIX rule A ⊗ B ⊢ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, a proof structure is a proof net if and only if its every switching is acyclic. In the absence of the MIX rule the criterion becomes that every switching be acyclic and also connected, that is, a tree.

2.5 Coherence spaces

Coherence spaces were the first and indeed motivating model of linear logic [Gir87]. Define the ∗-autonomous category of coherence spaces and linear maps as follows.

Objects. A coherence space U = (|U|, ⌢ ⌣_{U}) is a reflexive undirected graph: a set |U| of tokens and a reflexive symmetric coherence relation ⌢ ⌣_{U} ⊆ |K| × |U| between tokens. Define strict coherence by u^{⌢}_{U} v iff u ⌢ ⌣_{U} v and u ≠ v, incoherence by u ⌣ ⌢_{U} v iff ¬(u^{⌢}_{U} v), and strict incoherence by u^{⌣}_{U} v iff ¬(u ⌢ ⌣_{U} v).

A clique a in U is a subset a of |U| made of pairwise coherent tokens; an anticlique x in U is a subset x of |U| made of pairwise incoherent tokens. We write U^{•} and U^{∘} for the sets of cliques and anticliques of U respectively.

Morphisms. A linear map l : U → V is a binary relation between tokens l ⊆ |U| × |V | such that for all (u, v), (u′, v′) ∈ l, u ⌢ ⌣_{U} u′ ⇒ v ⌢ ⌣_{V} v′ and v ⌣ ⌢_{V} v′ ⇒ u ⌣ ⌢_{U} u′. Composition is usual relational composition, with the usual identities. A linear map l defines a function [−]l : U^{•} → V^{•} from cliques to cliques and a reverse function l[−] : V^{∘} → U^{∘} from anticliques to anticliques, with

[a]l  = { v ∈ |V | : ∃u ∈ a ((u, v) ∈ l) }
l[x] = { u ∈ |U| : ∃v ∈ x ((u, v) ∈ l) }

Either [−]l or l[−] determine l completely.

Linear negation: U^{⊥} = (|U|, ⌣ ⌢_{U}), the exchange of coherence and incoherence. On maps l^{⊥} : V^{⊥} → U^{⊥} is given by (v, u) ∈ l^{⊥} iff (u, v) ∈ l.

Tensor product: |U ⊗ V | = |U| × |V | with (u, v) ⌢ ⌣_{U⊗V} (u′, v′) iff u ⌢ ⌣_{U} u′ and v ⌢ ⌣_{V} v.

Tensor unit: |I| = {⋆}, with (necessarily) ⋆ ⌢ ⌣_{I} ⋆. Linear maps I → X correspond to cliques of X.

2.5.1 The Lafont-Streicher embedding

Lafont and Streicher [LS91] exhibit a full and faithful functor LS : Coh → Chu. Points are cliques, states are anticliques, and matrix entries are given by intersection: LS(U) = (U^{•}, ⊓ , U^{∘}), where a ⊓ x = |a ∩ x|. (Note that clique and an anticlique can intersect in at most one point.) On linear maps l : U → V, LS(l) = ([−]l, l[−]) : LS(U) → LS(V).

The embedding is weakly tensorial with tensorial strength τ_{UV} : LS(U) ⊗ LS(V) → LS(U ⊗ V) and t : 1 → LS(I) as follows:

\begin{aligned}τ^{+} & : & (a, b) ↦ a × b \\ τ^{−} & : & z ↦ ([−]z, z[−]) \end{aligned} \begin{aligned}t^{+} & : & ⋆ ↦ \{⋆\} \\ t^{−} & : & ∅ ↦ 0, \{⋆\} ↦ 1 \end{aligned}

τ^{−} is an isomorphism because LS is full and faithful. The embedding commutes with involution: LS(U)^{⊥} = LS(U^{⊥}).

2.5.2 Relating LS(Coh) to Coh

Both our semisimple full completeness result and the subsequent extension to higher types pivot on our ability to move freely between Chu and Coh. In this section we show that any semantic proof (logical element) η of a formula F in Chu can be pulled back to a semantic proof η̂ of F in Coh. We first exhibit a map (ˆ−) taking points a of F (LSU) in Chu to cliques â of F (U) in Coh, then define η̂ componentwise by η̂_{U} = η̂_{LSU}.

The Chu space LSU ⊗ LSV has the same states as LS(U ⊗ V), namely all anticliques of U ⊗ V. However LSU ⊗ LSV does not have all cliques of U ⊗ V, only the “rectangular” ones formed as a × b, where a, b are cliques of U, V respectively. The par LSU^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} LSV has the dual defect. The value in Chu of an arbitrary MLL formula F on LSCoh will then be missing both cliques and anticliques of the value of F in Coh. However, sufficiently many cliques and anticliques remain that the latter can be reconstructed as a certain closure of the former, denoted \overline{A}.

Let A = (A, r, X) be a biextensional Chu space, in other words, a Chu space with no repeated rows or columns. Then we can identify every point a of A with the subset {x ∈ X : r(a, x) = 1} of X, and every state x with the subset {a ∈ A : r(a, x) = 1} of A. This allows us to treat A as a set of subsets of X, treat X as a set of subsets of A, and to form unions of points and states, as in the following construction.

Define a set of sets to be consistent when it is non-empty and pairwise disjoint (stronger than necessary, but convenient and sufficient for our purposes).

Definition 6. The consistent closure of a biextensional Chu space A is the biextensional Chu space \overline{A} = (\overline{A}, \overline{r}, \overline{X}) given by

\overline{A} = \{ ⋃ A′ : A′ ⊆ A and A′ is consistent\}
\overline{X} = \{ ⋃ X′ : X′ ⊆ X and X′ is consistent\}

and for all consistent A′ ⊆ A and consistent X′ ⊆ X

\overline{r} ( ⋃ A′, ⋃ X′ ) = ⋁_{a∈A′, x∈X′} r(a, x)

For a non-biextensional Chu space A define \overline{A} to be the consistent closure of the biextensional collapse of A.

Note that \overline{\overline{A}} = \overline{A} and \overline{A^{⊥}} = \overline{A}^{⊥}. If \overline{A} ≅ LSU for some coherence space U then we say that A generates U. The following Lemma states that if A generates U and B generates V, then A ⊗ B (tensor in Chu) generates U ⊗ V (tensor in Coh).

Lemma 7. Let A, B be Chu spaces such that \overline{A} ≅ LSU and \overline{B} ≅ LSV for coherence spaces U, V. Then

\overline{A ⊗ B} ≅ LS(U ⊗ V)

Proof. Write A = (A, r, X), B = (B, s, Y), A⊗B = (A× B, t, F), LSU = (U^{•}, ⊓, U^{∘}) and LSV = (V^{•}, ⊓, V^{∘}). Thus LS(U ⊗ V) =((U ⊗ V)^{•}, ⊓, (U ⊗ V)^{∘}). We define a Chu isomorphism (θ, ϕ) : \overline{A ⊗ B} → LS(U ⊗ V), i.e. an adjoint pair of isomorphisms θ : \overline{A × B} → (U ⊗ V)^{•} and ϕ : (U ⊗ V)^{∘} → \overline{F} between sets:

θ( ⋃ { (a_{i}, b_{i}) : i ∈ I } ) = ⋃_{i∈I} (a_{i} × b_{i})
ϕ(∅) =  ∅
ϕ(z) = ⋃ {f_{α,β} : ⟨α, β⟩ ∈ z}

( for z ≠ ∅) where f_{α,β} = (f_{α,β}^{1} : A → Y, f_{α,β}^{2} : B → X) is given by

f_{α,β}^{1}(a) = \begin{cases}\{β\} & if α ∈ a \\ ∅ & if α ∉ a \end{cases}  f_{α,β}^{2}(b) = \begin{cases}\{α\} & if β ∈ b \\ ∅ & if β ∉ b \end{cases}

The definition of ϕ(z) requires working with tokens α, β. These are available since for a Chu space (A, r, X) to generate a coherence space U, both A and X must contain ∅ (as a row and column of 0s respectively) and all singletons (i.e. tokens) of U.

Proposition 8. Let F be an n-ary MLL formula, U = U_{1}, …, U_{n} for coherence spaces U_{i} ∈ Coh, and LSU = LSU_{1}, …, LSU_{n}. Then

\overline{F (LSU)} ≅ LS(F U),

where F is interpreted on the left as an MLL operation in Chu, and on the right as an MLL operation in Coh.

Proof. Since \overline{A^{⊥}} = \overline{A}^{⊥} for any Chu space A, so we can write A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B in F as (A^{⊥} ⊗ B^{⊥})^{⊥}, then apply Lemma 7 recursively.

For the following definition, note that points of F (LSU) are a subset of the points of \overline{F (LSU)}.

Definition 9. Let F be an n-ary MLL formula, U = U_{1}, …, U_{n} for coherence spaces U_{i} ∈ Coh, and LSU = LSU_{1}, …, LSU_{n}. Given any point a of F (LSU) in Chu, define the clique â of F (U) in Coh, the clique associated with a, as the image of a under the isomorphism of Proposition 8, acting from left to right.

3 Semisimple full completeness

An MLL formula is semisimple if it is of the form .^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{i≤m}( ⨂_{j≤k_{i}} L_{ij}) where L_{ij} are literals. Our route to full completeness for semisimple formulae passes through the category Coh of coherence spaces, via the map (ˆ−) constructed above. The primary attraction of Coh is the existence of full completeness results for MLL with MIX, for example [Tan97], which allow us to assign a MIX proof net to every logical transformation in Chu.

In the Lafont-Streicher image of Coh in Chu, the functional behaviour of the logical transformation corresponds to a tuple of lambda calculus terms associated canonically with its MIX proof net. We argue that the behaviour of the logical transformation outside the Coh image is also governed by the lambda terms, by asserting logical relations to hold between arbitrary Chu spaces and their “simulations” in the Coh image. Thus every logical transformation is characterized by a distinct tuple of lambda terms.

Finally we refute MIX, by showing that any such lambda term must use all of its arguments during computation. Hence the corresponding MIX proof net is connected under all switchings, so is a proof net, and we obtain the desired bijection between proofs of semisimple MLL theorems and logical transformations in Chu.

3.1 MIX proof nets via Coh

In this section we a associate MIX proof net π_{η} with every Chu logical transformation η, by passing into Coh and appealing full completeness for MLL with MIX [Tan97].

Lemma 10. Let F be a semisimple formula. Every logical element η : 1 → F in Chu gives rise to a dinatural transformation η̂: 1 → F in Coh.

Proof. Define η̂_{U} = η̂_{LSU}. We omit the proof that η̂ is dinatural.

Tan [Tan97] has shown that every dinatural transformation of a formula in Coh is the denotation of a unique MIX proof net, a proof structure acyclic under all switchings, though not necessarily connected. Define the MIX proof net π_{η} defined by η to be the MIX proof net denoting η̂ in Coh.

3.2 λ term characterization in LS(Coh)

We show that every logical transformation η in Chu, when restricted to the Coh-image, is determined by a tuple of lambda terms associated cananocally with the MIX proof net π_{η} that was assigned to it via Coh.

Lemma 11. Every MIX proof net of a semisimple formula F = ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{i≤m}(⨂_{j≤k_{i}}L_{ij}) is characterized uniquely by an m-tuple (t^{1}, …, t^{m}) of λ-terms. Each t^{i} is of the form λa_{1} … a_{m−1}.M^{i} where the body M^{i} is a tuple (M_{1}^{i}, …, M_{k_{i}}^{i}) containing no λ abstractions and at most one occurrence of each variable a_{j}, 1 ≤ j ≤ m − 1.

Proof. Let G_{π} be the undirected graph with vertices the clauses F_{i} = ⨂_{j≤k_{i}}L_{ij} of F and edges the links e of π, with e connecting F_{i} and F_{i′} in G_{π} just when e matches a literal of F_{i} with a literal of F_{i′} in π. Since F is semisimple and π is acyclic under all switchings, G_{π} is acyclic.

We first construct t^{m}. Orient the edges of the connected component of the vertex F_{m} so as to point towards F_{m}. This defines a tree which we interpret as the applicative structure of M^{m}. Variable a_{i} corresponds to vertex F_{i} and serves as the function symbol at that vertex, taking as arguments the subtrees below it, with the leaves thus constituting ordinary variables. The k_{m} incoming edges of F^{m} give rise to the k_{m} components M_{j}^{m} of M^{m}.

The remaining t^{i} are obtained similarly, modulo matching a_{l} with F_{l+1} for i ≤ l ≤ m − 1.

Our next Lemma allows us to describe every Chu transformation η : 1 → ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{i≤m}(⨂_{j≤k_{i}}L_{ij}) into a semisimple formula of n variables as an m-tuple of families of functions (η1 ; A⃗, …, ηm ; A⃗) indexed by A⃗ ∈ Chu^{n}.

Lemma 12. Let A_{1}, …, A_{m} be Chu spaces. Every Chu transform f : 1 → A_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} …^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{m} is characterized by an m-tuple of functions (f^{1}, …, f^{m}), where f^{i} : A_{1}^{−} × … × A_{i−1}^{−} × A_{i+1}^{−} × … × A_{m}^{−} → A_{i}^{+}.

Proof. Omitted.

Proposition 13. Let η : 1 → F be a logical element into a semisimple MLL formula of n variables in Chu, and let t = (t^{1}, …, t^{m}) be the tuple of lambda terms representing the MIX proof net π_{η} associated with η. Then η = t in LS(Coh)^{n} ⊂ Chu^{n}. In other words, ηi_{LSU} = t^{i} for all U = U_{1}, …, U_{n} ∈ Coh^{n} and 1 ≤ i ≤ m, where LSU = LS(U_{1}), …, LS(U_{n}) ∈ Chu^{n}.

Proof. Omitted.

3.3 λ-term characterization beyond LS(Coh)

Having characterized logical transformations in the Coh-image by tuples of lambda terms, we show that this uniform behaviour extends to the whole of Chu.

Proposition 14. Let F be a semisimple MLL formula of n propositional variables interpreted in Chu. Then every logical tranformation η : 1 → F is determined by its restriction to the Coh-image, namely the sub-family η_{A A A} indexed by A A A ∈ LS(Coh)^{n}.

Proof. To determine η at arbitrary Chu spaces A A A ∈ Chu^{n} we “simulate” each A = (A, r, X) ∈ A A A by a coherence space \overline{A}, then use logical relations between LS(\overline{A}) in LS(Coh) and A in Chu to pin down the behaviour of η_{A A A}.

The set of tokens of \overline{A} is A + X + r, the disjoint union of the points, the states, and the coordinates of the 1s in the matrix. Coherence is “coherence along rows, incoherence within columns”: a ⌢ ⌣(a, x) and (a, x) ⌢ ⌣(a, y) for all a ∈ A and x, y ∈ X, together with the requisite loops α ⌢ ⌣α. The “row”-clique \overline{a} = \{a\} ∪ \{(a, x) ∈ r : x ∈ X} “simulating” a intersects the “column”-anticlique \overline{x} = \{x\} ∪ \{(a, x) ∈ r : a ∈ A\} “simulating” x exactly when r(a, x) = 1. Hence the matrix ⊓ of LS(\overline{A}) “simulates” the matrix of the original: \overline{a} ⊓ \overline{x} = |\overline{a} ∩ \overline{x}| = r(a, x). We establish this relationship formally as the logical relation R_{A} between LS(\overline{A}) and A given on points by \overline{a} R_{A}^{+}a for every a ∈ A and on states by \overline{x} R_{A}^{−}x for every x ∈ X. R_{A} is logical because \overline{a} ⊓ \overline{x} = r(a, x), the adjointness condition of Definition 2.2.

Let t = λa_{1} … a_{m−1}.M be one of the tuple of λ-terms characterizing η in LS(Coh), and assume for simplicity, and without loss of generality, that the tuple M is a singleton. Recast the type of η : 1 → F to parallel the natural typing of t, so that

η_{A A A} : F_{1} ⊗ … ⊗ F_{m} → B
η_{LS(\overline{A A A})} : G_{1} ⊗ … ⊗ G_{m} → LS(\overline{B})
F_{i} = B_{i1} ⊗ … ⊗ B_{ik_{i}}−∘B_{i}
G_{i} = LS(\overline{B_{i1}}) ⊗ … ⊗ LS(\overline{B_{ik_{i}}})−∘LS(\overline{B_{i}})

for B, B_{i}, B_{ij} ∈ A A A and LS(\overline{A A A}) = (LS(\overline{A_{1}}), …, LS(\overline{A_{n}})). We shall determine

η_{A A A}^{+} : F_{1}^{+} × … × F_{m}^{+} → B^{+},

a component of the tuple characterizing η as per Lemma 12, by showing that

η_{A A A}^{+}(f_{1}, …, f_{m}) = t(f_{1}, …, f_{m})

for all inputs f_{i} ∈ F_{i}^{+}. For each f_{i} define the linear map

f̃_{i} : \overline{B_{i1}} ⊗ … ⊗ \overline{B_{ik_{i}}} → \overline{B_{i}}

between coherence spaces by

\{(b_{i1}, …, b_{ik_{i}})\} × \overline{f_{i}^{+}(b_{i1}, …, b_{ik_{i}})} ⊆ f̃_{i}

for all b_{ij} ∈ B_{ij}^{+} ⊆ |\overline{B_{ij}}|, where for a point a of a Chu space A, \overline{a} is the “row” clique of \overline{A} simulating a as defined above. Let τ_{i} be the tensorial strength

LS(\overline{B_{i1}}) ⊗ … ⊗ LS(\overline{B_{ik_{i}}}) → LS(\overline{B_{i1}} ⊗ … ⊗ \overline{B_{ik_{i}}})

and define \overline{f_{i}} = LS(f̃_{i}) ∘ τ_{i} of type G_{i}, so that \overline{f_{i}}^{+} is a function from (k_{i}-tuples of) “row”-cliques to “row”-cliques. In particular \overline{f_{i}} “simulates” f_{i}, for example

\overline{f_{i}}^{+}(\overline{b_{i1}}, …, \overline{b_{ik_{i}}}) = \overline{f_{i}^{+}(b_{i1}, …, b_{ik_{i}})}  (1)

More formally, \overline{f_{i}}R_{i}^{+}f_{i} under the Chu logical relation R_{i} = R_{B_{i1}} ⊗ … ⊗ R_{B_{ik_{i}}} −∘R_{B_{i}} between G_{i} and F_{i}.

Since R_{i} is a Chu logical relation between G_{i} and F_{i} for each i, by the logicality of η we must have η_{LS(\overline{A A A})}^{+}(\overline{f_{1}}, …, \overline{f_{m}}) R_{B_{i}}^{+} η_{A A A}^{+}(f_{1}, …, f_{m}). Furthermore since η_{LS(\overline{A A A})}^{+} is a λ-term t, by repeated application of (1) we have

η_{LS(\overline{A A A})}^{+}(\overline{f_{1}}, …, \overline{f_{m}}) = t(\overline{f_{1}}, …, \overline{f_{m}})
= \overline{t(f_{1}, …, f_{m})}

Thus

\overline{t(f_{1}, …, f_{m})} R_{B_{i}}^{+} η_{A A A}^{+}(f_{1}, …, f_{m})

and since by construction aR_{B_{i}}^{+}b if and only if a = \overline{b}, we conclude that η_{A A A}^{+}(f_{1}, …, f_{m}) = t(f_{1}, … f_{m}).

Finally, repeat the argument for each of the other lambda terms of the tuple.

3.4 MIX refutation

The final link in the chain to semisimple full completeness is to show that the MIX proof net assigned to a Chu logical element is connected under all switchings, and hence is a proof net. This occurs precisely when any (and hence all) of the lambda terms in the characterizing tuple use all their arguments.

Lemma 15. , Let t = λa_{1} … a_{m−1}.M be a λ-term of the m-tuple characterizing a MIX proof net π of a semisimple formula ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{i≤m}(⨂_{j≤k_{i}} L_{ij}). If each variable a_{i} occurs in M, 1 ≤ i ≤ m − 1, then π is a proof net.

Proof. The graph G_{π} in the construction of t in Lemma 11 is connected if and only if π is a proof net.

Proposition 16. A λ-term of a tuple defining a Chu logical element of a semisimple MLL operation must use all its arguments.

Proof. Without loss of generality assume that the operation has the form A−∘B where B is a literal and A = A_{1} ⊗ … ⊗ A_{n} is a product of pars of literals. The λ-term then has the form λa_{1} … a_{n}.M for some applicative term M in λ-variables a_{1}, …, a_{n}. Let η be the denotation of this λ-term. Set all variables of the formula to the Chu space

J = {00 \atop 01} , so η_{J} is a Chu transform from A(J) to B(J).

Note that J^{⊥} = J.

A(J) is a Chu space with just one nonzero point, i.e. just one point indexing a nonzero row: A_{i} is a par of k_{i} literals, so A_{i}(J) is the par of k_{i} copies of J, a matrix with 2 points, 2^{k_{i}} states, and only one nonzero entry; hence A(J), the tensor product of n such matrices, has 2^{n} points, only one of which is nonzero. B(J) = J since B is a literal.

By continuity of η_{J}, every zero point (the index of an all-zero row) of A(J) must be sent to 0 in B(J). We now argue by logicality that the nonzero point of A(J) must be sent to 1 in B(J). Let N be the 1 × 1 Chu space whose one entry is 1, and take R to be the Chu relation between N and J that relates the point of N to the nonzero point of J and the state of N to the nonzero state of J. Then A(R) relates the point of A(N) = N with the nonzero point of A(J), so any two-sorted homomorphism from A(J) to J must send the nonzero point of A(J) to the nonzero point of B(J), i.e. 1.

But the one nonzero point of A(J) is indexed by the constantly-one n-tuple. So when all arguments to η_{J} are set to 1, and any one argument is then changed to 0, the result of η_{J} changes from 1 to 0. But then η, and hence the λ-term denoting it, depends on all n of its arguments.

Theorem 17 (Semisimple full completeness). Let F be a semisimple MLL formula interpreted in Chu. Then every logical tranformation η : 1 → F is denoted by a unique proof of F.

Proof. Proposition 13 characterizes η as a MIX proof net π_{η} in the Coh-image, and Proposition 14 extends this characterization to the whole of Chu. By Proposition 16, in conjunction with Lemma 15, π_{η} is a proof net.

4 Full Completeness

We prove our main theorem by induction on level of formulas, a measure of distance of theorems to certain semisimple formulas. We first define the notion of level and state key supporting lemmas.

The rules of our axiomatization of MLL either rearrange the formula invertibly (A and C), cater trivially for context (E), or do some real work (D). Our argument hinges on the behavior of this last rule.

For convenience and to make more explicit the choice implicit in linear distributivity (LD), we replace Rule D by an equivalent pair of rules either one of which would suffice on its own.

\begin{aligned}D1 & (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ⊗ C & ⊢ & (A ⊗ C)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B \\ D2 & (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ⊗ C & ⊢ & A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (C ⊗ B) \end{aligned}

A linking of the common antecedent of these rules is permuted by the rules to yield identical linkings of the two LD consequents.

Definition 18. The level of an MLL formula is defined to be maximal subject to the following constraints. The level of a semisimple formula is zero. If a level l formula is derivable from A by associativity or commutativity then A has level l. If a pair of LD consequents of A have level at most l then A has level at most l + 1.

So the level of a formula A is the minimum, over all occurrences within A of a subformula matching Rule D, of one plus the maximum of the level of the corresponding pair of LD consequents A_{1} and A_{2}. Every MLL formula reduces to semisimple formulas after finitely many applications of D, whence level is well-defined.

We shall need the following lemmas.

Lemma 19. If the LD consequents of a transformation of an MLL formula in Chu both represent proof nets, then those proof nets have the same Λ (linking of literals).

We defer the proof of this lemma to after the main theorem.

Lemma 20. If a linking Λ is a proof net for both Rule D consequents of a formula A, then Λ is a proof net for A.

Proof. We omit the straightforward combinatorial argument.

Theorem 21. Every logical element η of an MLL formula A represents a proof.

Proof. We proceed by induction on level. The previous section supplied the basis for the induction. We now assume as our induction hypothesis the case l and prove the case l + 1.

Let A be a formula of level l + 1, and let η be a logical element of A. Apply commutativity and associativity as required to A so that when Rule D is applied to some subformula (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ⊗ C in each of the two possible ways, both consequents A_{1} and A_{2} of A are of level l. The two applications of the rule map η to two transformations, call them η_{1} and η_{2}.

By soundness each η_{i} is a logical element and therefore by the induction hypothesis has a proof net. By Lemma 19 the two proof nets must have the same linking Λ. By Lemma 20 (A, Λ) is a proof net. By soundness (A, Λ) denotes a logical element η′ while (A_{1}, Λ) and (A_{2}, Λ) denote logical elements η′_{1}, η′_{2} respectively. By the induction hypothesis η′_{1} = η_{1} and η′_{2} = η_{2}. But D is injective, so η = η′.

This completes the proof of our main theorem, leaving only Lemma 19 to prove.

Proof. (of Lemma 19) Let η in A have consequents η_{1} and η_{2} representing proof nets in Chu. Form the corresponding arrangement in Coh, consisting of a clique η̂ and consequents η̂_{1} and η̂_{2}. By Lemma 23 η_{i} and η̂_{i} represent the same proof nets for i = 1, 2. By Lemma 24 η̂_{1} and η̂_{2} are the LD consequents of a common clique η̂. By Lemma 22 they have the same linking, whence the same holds for η_{1} and η_{2}.

We have discharged obligation 19 at the expense of three new obligations.

Lemma 22. If the two LD consequents of a clique both realize proof nets then those nets have the same linking.

Proof. Although the rules of System S nontrivially transform the coherence spaces they act on, their constituent tokens, as tuples of tokens of W, are not changed except to reflect permutations of variables. The linking information in a dinatural clique in Coh resides entirely in the individual tokens [Tan97] (as opposed to the coherence relations between the tokens). Under our reformulation of Rule D as D1 and D2, the two LD consequents of a clique undergo the same permutation of atomic tokens within each token of the clique and hence encode the same linking.

Lemma 23. If η is the unique representation in Chu of a proof net (A, Λ), then η̂ represents (A, Λ) in Coh.

Proof. Select any System S derivation of (A, Λ) and interpret it in both Coh and Chu. In the beginning the hat relationship holds between the respective proof representations. By commutativity of hat and derivation (Lemma 24) this relationship is maintained during the proof and hence still holds when A is reached. Since (A, Λ) only has one representation, the transformation in Chu we ended up with must be η, whence the transformation in Coh we arrived at must be η̂.

Lemma 24. The hat map taking the points of the Chu space F (LSW W W) to the coherence space F (W W W) commutes with the action of the rules of System S.

Proof. Since the rules act according to λ-terms it suffices to verify the commutativity for all λ-terms. If the correspondence between Chu spaces F (LSW W W) and coherent spaces F (W W W) were an isomorphism this would be a triviality. However the points of the former embed as a subset of those of the latter, and likewise for states, both for the top level formula and for all subformulas. We therefore need to show that the correspondence is tight enough for the action of the rules to maintain the correspondence despite this difference.

We proceed by induction on the height of λ-terms. We take as our inductive hypothesis that for all MLL formulas F, for all assignments of Chu spaces LSW W W, and corresponding assignments of coherent spaces W W W, to variables of F, and for all bindings of λ-variables to points of F (LSW W W), and correspondingly to points of F (W W W), evaluating a λ-term of height h in each of the two environments produces a corresponding pair of points of respectively F (LSW W W) and F (W W W).

The basis for the induction, λ-terms that are λ-variables, holds by choice of environment. We now assume the case of height h and proceed to height h + 1.

For applications MN, the Chu point denoted by M is a function f between Chu spaces A and B (say) while the corresponding coherence space point denoted by M is a function f̂ from \overline{A} to \overline{B}. Since the correspondence embeds the set A of points of A in \overline{A}, and since N evaluates to a point a in the image of that embedding by the induction hypothesis, f̂(a) must be the corresponding point in \overline{B}, which too will be in the image of the embedding of B in \overline{B}.

A λ-abstraction λx.M, as a point of say A−∘B, will denote a Chu transform f of Chu spaces having corresponding coherence space map f̂. The induction hypothesis ensures that f and f̂agree on A, while the fact that coherence space maps commute with consistent unions ensures that the coherence space map denoted by λx.M (as determined by evaluating M in each environment obtained by setting x to a point of \overline{A}) agrees with f̂on the whole of \overline{A}.

For pairs (M, N) the correspondence is immediate.

References

[AJ94] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59(2):543–574, 1994.

[Bar79] M. Barr. ∗-Autonomous categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[BS96] R.F. Blute and P.J. Scott. Linear Läuchli semantics. Annals of Pure and Applied Logic, 77:101–142, 1996.

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

[Gir87] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[HO93] J.M.E. Hyland and C.-H.L. Ong. Fair games and full completeness for multiplicative linear logic without the mix-rule. Available by ftp from ftp.comlab.ox.ac.uk as fcomplete.ps.gz in /pub/Documents/techpapers/Luke.Ong, 1993.

[Loa94] R. Loader. Linear logic, totality and full completeness. In Proc. 9th Annual IEEE Symp. on Logic in Computer Science, 1994.

[LS86] J. Lambek and P. Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1986.

[LS91] Y. Lafont and T. Streicher. Games semantics for linear logic. In Proc. 6th Annual IEEE Symp. on Logic in Computer Science, pages 43–49, Amsterdam, July 1991.

[Pav96] D. Pavlović. Chu I: Cofree equivalences, dualities and ∗-autonomous categories. Math. Structures in Comp. Sci., 6(5), 1996.

[Plo80] G.D. Plotkin. Lambda definability in the full type hierarchy. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press, 1980.

[PR98] R. Paré and L. Román. Dinatural numbers. J. Pure and Applied Algebra, 128:33–92, 1998.

[Pra95a] V.R. Pratt. Chu spaces and their interpretation as concurrent objects. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 392–405. Springer-Verlag, 1995.

[Pra95b] V.R. Pratt. The Stone gamut: A coordinatization of mathematics. In Logic in Computer Science, pages 444–454. IEEE Computer Society, June 1995.

[Pra97] V.R. Pratt. Towards full completeness of the linear logic of chu spaces. In Electronic Notes in Theoretical Computer Science, volume 6, Pittsburgh, 1997. URL: http://www.elsevier.nl/locate/entcs/volume6.html, 18 pages.

[Pra98] V.R. Pratt. Chu spaces as a semantic bridge between linear logic and mathematics. Submitted to a technical journal, available as http://boole.stanford.edu/pub/bridge.ps.gz, 1998.

[Tan97] A. Tan. Full completeness for models of linear logic. PhD thesis, King’s College, University of Cambridge, October 1997.

[VGP95] R. Van Glabbeek and G. Plotkin. Configuration structures. In Logic in Computer Science, pages 199–209. IEEE Computer Society, June 1995.