1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Friday September 15, 2:15 pm
P. J. Scott
Newton Institute and University of Ottawa
Traditional completeness theorems for logics relate truth in models to provability. In this work, joint with Richard Blute, the goal is to give genuine mathematical models of proofs themselves, with appropriate representation theorems. Equivalently, we shall find mathematical models yielding full representation theorems for certain free categories (in this case, for free $*$-autonomous categories).
This work has two historical sources: work on full abstraction for programming languages begun by Milner in the 1970's, and the somewhat lesser known, but highly influential work of Lauchli (1968) on abstract realizability. Although we were inspired by recent similar work by Abramsky/Jagadeesan and Hyland/Ong, our models do not use anything like game semantics, but rather ordinary mathematical structures.
We consider continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on a linear version of Functorial Polymorphism, employs "uniform" dinatural transformations which are equivariant with respect to all such actions. 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.
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 linear logics, e.g. to Yetter's Cyclic Linear Logic, using the Shuffle Hopf Algebra.