Previous: Representing general structures with Up: Chu Spaces from the Next: Conclusion

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 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 and logical connectives , , , and . In the following, 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, . This is interpreted simply as the dual of the Chu space interpreting A.

The operation is interpreted as the Chu space consisting of the representations of the continuous functions from the interpretation of A to the interpretation of B. Recall from section 3 the Chu space representing . Let denote the set of continuous functions from to . Then is defined as the Chu space consisting of the representations of those functions viewed as words of length , where r(f,(a,y)) = = s(f(a),y).

This defines the behavior of on Chu spaces. Its behavior on morphisms is defined so as to give this operation the characteristics of an internal homfunctor. Given continuous functions and , we take to be the continuous function from to defined by , sending the Chu transform (where ) to the composite (where = ). Since Chu transforms are closed under composition hgf is a Chu transform, whence is well-defined.

It remains to show that is continuous. Evidently its adjoint should map to where is the adjoint of h. Instantiating the adjointness condition calls for the equality of (namely t(hgf,(a',y'))) and . The definition of t gives the left hand side as S'(hgf(a'),y') and the right hand side as , but these are equal because h is a Chu transform, and we are done.

Having defined as a functor it is now easy to define , namely as , and , as .

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 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.

Previous: Representing general structures with Up: Chu Spaces from the Next: Conclusion
Vaughan Pratt
1998-03-14