The paper below is available by anonymous ftp from the
following sites:
triples.math.mcgill.ca, in the directory: pub/blute,
theory.doc.ic.ac.uk, in the directory: papers/Scott.
ftp.csi.uottawa.ca, in the directory: pub/papers/PhilScott
The file is called: lauchli.ps.Z.
Any comments would be greatly appreciated.
Cheers,
Philip Scott
P. S. Of course, you may also contact either of the authors for a
hard copy:
R. F. Blute & P. J. Scott
Dept. of Mathematics
University of Ottawa
585 King Edward
Ottawa, Ont. K1N 6N5
Canada
----------------------------------------------
LINEAR LAUCHLI SEMANTICS
R. F. Blute P. J. Scott
We introduce a linear analogue of Lauchli's semantics for
intuitionistic logic. In fact, our result is a strengthening
of Lauchli's work to the level of proofs, rather than
provability. This is obtained by considering continuous actions
of the additive group of integers on a category of topological
vector spaces. The semantics, based on functorial
polymorphism, consists of dinatural transformations which are
equivariant with respect to all such actions. Such dinatural
transformations are called uniform. To any sequent in
Multiplicative Linear Logic (MLL), we associate a vector space
of ``diadditive'' uniform transformations. We then show that this
space is generated by denotations of cut-free proofs of
the sequent in the theory MLL+MIX. Thus we obtain a full
completeness 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 transformations
which are uniform with respect to actions of the additive group of
integers are also uniform with respect to the actions of arbitrary
cocommutative Hopf algebras. Finally, we discuss several possible
extensions 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 work can also be viewed as a first step towards
developing a theory of logical relations for linear
logic and concurrency.