LINEAR LAUCHLI SEMANTICS

We introduce a linear analogue of Lauchli's semantics for intuitionist ic logic. In fact, our result is a strengthening of Lauchli's work to the level of proofs, rather than provability. This is obtained by cons idering continuous actions of the additive group of integers on a cate gory of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivari ant with respect to all such actions. Such dinatural transformations a re called uniform. To any sequent in Multiplicative Linear Logic (MLL) , we associate a vector space of ''diadditive'' uniform transformation s. We then show that this space is generated by denotations of cut-fre e proofs of the sequent in the theory MLL+MIX. Thus we obtain a full c ompleteness theorem in the sense of Abramsky and Jagadeesan, although our result differs from theirs in the use of dinatural transformations . As corollaries, we show that these dinatural transformations compose , and obtain a conservativity result: diadditive dinatural transformat ions which are uniform with respect to actions of the additive group o f integers are also uniform with respect to the actions of arbitrary c ocommutative Hopf algebras. Finally, we discuss several possible exten sions of this work to noncommutative logic. It is well known that the intuitionistic version of Lauchli's semantics is a special case of the theory of logical relations, due to Plotkin and Statman. Thus, our wo rk can also be viewed as a first step towards developing a theory of l ogical relations for linear logic and concurrency.