Linear Logic

Chu spaces and their continuous functions form a *-autonomous category [Bar79], one that is self-dual and symmetric monoidal closed. This places them squarely in the domain of discourse of Girard's linear logic [Bar91,Gir87]. In this section we define the multiplicative fragment of linear logic from the representational viewpoint, in which ${\cal A}{\relbar\mkern-9mu\circ}{\cal B}$ in particular has a strikingly natural definition.

In ordinary logic the logical connectives denote operations on truth values. Linear logic however makes the most sense when understood as a categorical logic, whose connectives are functors rather than mere operations.

The language of multiplicative linear logic consists of propositional variables $P,Q,\ldots$ and logical connectives $A^\bot$, $A{\relbar\mkern-9mu\circ}B$, $A\otimes B$, and $A\invamp B$. In the following, $A,B,\ldots$ denote arbitrary formulas.

In the Chu space interpretation of linear logic, all formulas are interpreted as Chu spaces.

The first operation of linear logic is linear negation, $A^\bot$. This is interpreted simply as the dual ${\cal A}^\bot$ of the Chu space ${\cal A}$ interpreting A.

The operation $A{\relbar\mkern-9mu\circ}B$ is interpreted as the Chu space consisting of the representations of the continuous functions from the interpretation ${\cal A}=(A,r,X)$ of A to the interpretation ${\cal B}=(B,s,Y)$ of B. Recall from section 3 the Chu space ${\cal F}_f=(A,\varphi_f,Y)$ representing $f:{\cal A}\to{\cal B}$. Let ${\cal B}^{{\cal A}}$ denote the set of continuous functions from ${\cal A}$ to ${\cal B}$. Then ${\cal A}{\relbar\mkern-9mu\circ}{\cal B}$ is defined as the Chu space $({\cal B}^{{\cal A}},r,A\times Y)$ consisting of the representations of those functions viewed as words of length $A\times Y$, where r(f,(a,y)) = $\varphi_f(a,y)$ = s(f(a),y).

This defines the behavior of ${\relbar\mkern-9mu\circ}$ on Chu spaces. Its behavior on morphisms is defined so as to give this operation the characteristics of an internal homfunctor. Given continuous functions $f:{\cal A}'\to{\cal A}$ and $h:{\cal B}\to{\cal B}'$, we take $f{\relbar\mkern-9mu\circ}h$ to be the continuous function from ${\cal A}{\relbar\mkern-9mu\circ}{\cal B}$ to ${\cal A}'{\relbar\mkern-9mu\circ}{\cal B}'$ defined by $\lambda g.hgf$, sending the Chu transform $g:{\cal A}\to{\cal B}$ (where ${\cal A}{\relbar\mkern-9mu\circ}{\cal B}=({\cal B}^{{\cal A}},t,A\times Y)$) to the composite $hgf:{\cal A}'{\relbar\mkern-9mu\circ}{\cal B}'$ (where ${\cal A}'{\relbar\mkern-9mu\circ}{\cal B}'$ = $({\cal B}^{\prime{\cal A}},t',A'\times Y')$). Since Chu transforms are closed under composition hgf is a Chu transform, whence $f{\relbar\mkern-9mu\circ}h$ is well-defined.

It remains to show that $f{\relbar\mkern-9mu\circ}h$ is continuous. Evidently its adjoint should map $(a',y')\in A'\times Y'$ to $(f(a'),h^\bot(y'))\in A\times Y$ where $h^\bot:Y'\to Y$ is the adjoint of h. Instantiating the adjointness condition calls for the equality of $t'(\lambda g.hgf(g),(a',y'))$ (namely t(hgf,(a',y'))) and $t(g,(f(a'),h^\bot(y'))$. The definition of t gives the left hand side as S'(hgf(a'),y') and the right hand side as $S(g(f(a')),h^\bot(y'))$, but these are equal because h is a Chu transform, and we are done.

Having defined $A{\relbar\mkern-9mu\circ}B$ as a functor it is now easy to define $A\otimes B$, namely as $(A{\relbar\mkern-9mu\circ}B^\bot)^\bot$, and $A\invamp B$, as $A^\bot{\relbar\mkern-9mu\circ} B$.

In [Pra97] we make a start on the project of proving full completeness of linear logic interpreted over Chu spaces, by showing that for formulas of multiplicative linear logic having at most two occurrences of each variable, cut-free proof-nets of those formulas are in bijective correspondence with the dinatural elements of the corresponding functors. This shows that, up to this case, dinaturality exactly captures proof on the semantic side of the mathematical ledger.

In more recent work this summer with Gordon Plotkin we have shown that dinaturality is not sufficient for formulas with four occurrences. In particular there are at least four dinaturals from $A{\relbar\mkern-9mu\circ}A$ to itself. However by strengthening the naturality condition to logicality, i.e. invariance under logical relations, we believe we can extend full completeness to the whole of MLL.